equal
deleted
inserted
replaced
33 lemma linearform_neg [intro??]: |
33 lemma linearform_neg [intro??]: |
34 "[| is_vectorspace V; is_linearform V f; x:V|] |
34 "[| is_vectorspace V; is_linearform V f; x:V|] |
35 ==> f (- x) = - f x"; |
35 ==> f (- x) = - f x"; |
36 proof -; |
36 proof -; |
37 assume "is_linearform V f" "is_vectorspace V" "x:V"; |
37 assume "is_linearform V f" "is_vectorspace V" "x:V"; |
38 have "f (- x) = f ((- 1r) (*) x)"; by (simp! add: negate_eq1); |
38 have "f (- x) = f ((- (#1::real)) (*) x)"; by (simp! add: negate_eq1); |
39 also; have "... = (- 1r) * (f x)"; by (rule linearform_mult); |
39 also; have "... = (- #1) * (f x)"; by (rule linearform_mult); |
40 also; have "... = - (f x)"; by (simp!); |
40 also; have "... = - (f x)"; by (simp!); |
41 finally; show ?thesis; .; |
41 finally; show ?thesis; .; |
42 qed; |
42 qed; |
43 |
43 |
44 lemma linearform_diff [intro??]: |
44 lemma linearform_diff [intro??]: |
54 qed; |
54 qed; |
55 |
55 |
56 text{* Every linear form yields $0$ for the $\zero$ vector.*}; |
56 text{* Every linear form yields $0$ for the $\zero$ vector.*}; |
57 |
57 |
58 lemma linearform_zero [intro??, simp]: |
58 lemma linearform_zero [intro??, simp]: |
59 "[| is_vectorspace V; is_linearform V f |] ==> f 00 = 0r"; |
59 "[| is_vectorspace V; is_linearform V f |] ==> f 00 = (#0::real)"; |
60 proof -; |
60 proof -; |
61 assume "is_vectorspace V" "is_linearform V f"; |
61 assume "is_vectorspace V" "is_linearform V f"; |
62 have "f 00 = f (00 - 00)"; by (simp!); |
62 have "f 00 = f (00 - 00)"; by (simp!); |
63 also; have "... = f 00 - f 00"; |
63 also; have "... = f 00 - f 00"; |
64 by (rule linearform_diff) (simp!)+; |
64 by (rule linearform_diff) (simp!)+; |
65 also; have "... = 0r"; by simp; |
65 also; have "... = (#0::real)"; by simp; |
66 finally; show "f 00 = 0r"; .; |
66 finally; show "f 00 = (#0::real)"; .; |
67 qed; |
67 qed; |
68 |
68 |
69 end; |
69 end; |