equal
deleted
inserted
replaced
450 then have "?P (c*s z + y)" unfolding thz Py det_row_mul[of i] det_row_add[of i] |
450 then have "?P (c*s z + y)" unfolding thz Py det_row_mul[of i] det_row_add[of i] |
451 by simp } |
451 by simp } |
452 |
452 |
453 ultimately show ?thesis |
453 ultimately show ?thesis |
454 apply - |
454 apply - |
455 apply (rule span_induct_alt[of ?P ?S, OF P0, folded smult_conv_scaleR]) |
455 apply (rule span_induct_alt[of ?P ?S, OF P0, folded scalar_mult_eq_scaleR]) |
456 apply blast |
456 apply blast |
457 apply (rule x) |
457 apply (rule x) |
458 done |
458 done |
459 qed |
459 qed |
460 |
460 |
744 have thr: "- row i A \<in> span {row j A| j. j \<noteq> i}" |
744 have thr: "- row i A \<in> span {row j A| j. j \<noteq> i}" |
745 unfolding thr0 |
745 unfolding thr0 |
746 apply (rule span_setsum) |
746 apply (rule span_setsum) |
747 apply simp |
747 apply simp |
748 apply (rule ballI) |
748 apply (rule ballI) |
749 apply (rule span_mul [where 'a="real^'n", folded smult_conv_scaleR])+ |
749 apply (rule span_mul [where 'a="real^'n", folded scalar_mult_eq_scaleR])+ |
750 apply (rule span_superset) |
750 apply (rule span_superset) |
751 apply auto |
751 apply auto |
752 done |
752 done |
753 let ?B = "(\<chi> k. if k = i then 0 else row k A) :: real ^'n^'n" |
753 let ?B = "(\<chi> k. if k = i then 0 else row k A) :: real ^'n^'n" |
754 have thrb: "row i ?B = 0" using iU by (vector row_def) |
754 have thrb: "row i ?B = 0" using iU by (vector row_def) |
780 then have thd1: "det (\<chi> i. row i A) = det A" by simp |
780 then have thd1: "det (\<chi> i. row i A) = det A" by simp |
781 have thd0: "det (\<chi> i. if i = k then row k A + (\<Sum>i \<in> ?Uk. x $ i *s row i A) else row i A) = det A" |
781 have thd0: "det (\<chi> i. if i = k then row k A + (\<Sum>i \<in> ?Uk. x $ i *s row i A) else row i A) = det A" |
782 apply (rule det_row_span) |
782 apply (rule det_row_span) |
783 apply (rule span_setsum[OF fUk]) |
783 apply (rule span_setsum[OF fUk]) |
784 apply (rule ballI) |
784 apply (rule ballI) |
785 apply (rule span_mul [where 'a="real^'n", folded smult_conv_scaleR])+ |
785 apply (rule span_mul [where 'a="real^'n", folded scalar_mult_eq_scaleR])+ |
786 apply (rule span_superset) |
786 apply (rule span_superset) |
787 apply auto |
787 apply auto |
788 done |
788 done |
789 show "?lhs = x$k * det A" |
789 show "?lhs = x$k * det A" |
790 apply (subst U) |
790 apply (subst U) |
877 {fix i j |
877 {fix i j |
878 let ?A = "transpose ?mf ** ?mf" |
878 let ?A = "transpose ?mf ** ?mf" |
879 have th0: "\<And>b (x::'a::comm_ring_1). (if b then 1 else 0)*x = (if b then x else 0)" |
879 have th0: "\<And>b (x::'a::comm_ring_1). (if b then 1 else 0)*x = (if b then x else 0)" |
880 "\<And>b (x::'a::comm_ring_1). x*(if b then 1 else 0) = (if b then x else 0)" |
880 "\<And>b (x::'a::comm_ring_1). x*(if b then 1 else 0) = (if b then x else 0)" |
881 by simp_all |
881 by simp_all |
882 from fd[rule_format, of "cart_basis i" "cart_basis j", unfolded matrix_works[OF lf, symmetric] dot_matrix_vector_mul] |
882 from fd[rule_format, of "axis i 1" "axis j 1", unfolded matrix_works[OF lf, symmetric] dot_matrix_vector_mul] |
883 have "?A$i$j = ?m1 $ i $ j" |
883 have "?A$i$j = ?m1 $ i $ j" |
884 by (simp add: inner_vec_def matrix_matrix_mult_def columnvector_def rowvector_def cart_basis_def th0 setsum_delta[OF fU] mat_def)} |
884 by (simp add: inner_vec_def matrix_matrix_mult_def columnvector_def rowvector_def |
|
885 th0 setsum_delta[OF fU] mat_def axis_def) } |
885 hence "orthogonal_matrix ?mf" unfolding orthogonal_matrix by vector |
886 hence "orthogonal_matrix ?mf" unfolding orthogonal_matrix by vector |
886 with lf have ?rhs by blast} |
887 with lf have ?rhs by blast} |
887 moreover |
888 moreover |
888 {assume lf: "linear f" and om: "orthogonal_matrix ?mf" |
889 {assume lf: "linear f" and om: "orthogonal_matrix ?mf" |
889 from lf om have ?lhs |
890 from lf om have ?lhs |
929 note th0 = this |
930 note th0 = this |
930 have "f v \<bullet> f w = c^2 * (v \<bullet> w)" |
931 have "f v \<bullet> f w = c^2 * (v \<bullet> w)" |
931 unfolding dot_norm_neg dist_norm[symmetric] |
932 unfolding dot_norm_neg dist_norm[symmetric] |
932 unfolding th0 fd[rule_format] by (simp add: power2_eq_square field_simps)} |
933 unfolding th0 fd[rule_format] by (simp add: power2_eq_square field_simps)} |
933 note fc = this |
934 note fc = this |
934 show ?thesis unfolding linear_def vector_eq[where 'a="real^'n"] smult_conv_scaleR by (simp add: inner_add fc field_simps) |
935 show ?thesis |
|
936 unfolding linear_def vector_eq[where 'a="real^'n"] scalar_mult_eq_scaleR |
|
937 by (simp add: inner_add fc field_simps) |
935 qed |
938 qed |
936 |
939 |
937 lemma isometry_linear: |
940 lemma isometry_linear: |
938 "f (0:: real^'n) = (0:: real^'n) \<Longrightarrow> \<forall>x y. dist(f x) (f y) = dist x y |
941 "f (0:: real^'n) = (0:: real^'n) \<Longrightarrow> \<forall>x y. dist(f x) (f y) = dist x y |
939 \<Longrightarrow> linear f" |
942 \<Longrightarrow> linear f" |
979 apply (subst H(2)) |
982 apply (subst H(2)) |
980 apply (subst H(3)) |
983 apply (subst H(3)) |
981 apply (subst H(4)) |
984 apply (subst H(4)) |
982 using H(5-9) |
985 using H(5-9) |
983 apply (simp add: norm_eq norm_eq_1) |
986 apply (simp add: norm_eq norm_eq_1) |
984 apply (simp add: inner_diff smult_conv_scaleR) unfolding * |
987 apply (simp add: inner_diff scalar_mult_eq_scaleR) unfolding * |
985 by (simp add: field_simps) } |
988 by (simp add: field_simps) } |
986 note th0 = this |
989 note th0 = this |
987 let ?g = "\<lambda>x. if x = 0 then 0 else norm x *\<^sub>R f (inverse (norm x) *\<^sub>R x)" |
990 let ?g = "\<lambda>x. if x = 0 then 0 else norm x *\<^sub>R f (inverse (norm x) *\<^sub>R x)" |
988 {fix x:: "real ^'n" assume nx: "norm x = 1" |
991 {fix x:: "real ^'n" assume nx: "norm x = 1" |
989 have "?g x = f x" using nx by auto} |
992 have "?g x = f x" using nx by auto} |