equal
deleted
inserted
replaced
116 lemma (in vectorspace) diff_mult_distrib2: |
116 lemma (in vectorspace) diff_mult_distrib2: |
117 "x \<in> V \<Longrightarrow> (a - b) \<cdot> x = a \<cdot> x - (b \<cdot> x)" |
117 "x \<in> V \<Longrightarrow> (a - b) \<cdot> x = a \<cdot> x - (b \<cdot> x)" |
118 proof - |
118 proof - |
119 assume x: "x \<in> V" |
119 assume x: "x \<in> V" |
120 have " (a - b) \<cdot> x = (a + - b) \<cdot> x" |
120 have " (a - b) \<cdot> x = (a + - b) \<cdot> x" |
121 by (simp add: diff_def) |
121 by (simp add: diff_minus) |
122 also from x have "\<dots> = a \<cdot> x + (- b) \<cdot> x" |
122 also from x have "\<dots> = a \<cdot> x + (- b) \<cdot> x" |
123 by (rule add_mult_distrib2) |
123 by (rule add_mult_distrib2) |
124 also from x have "\<dots> = a \<cdot> x + - (b \<cdot> x)" |
124 also from x have "\<dots> = a \<cdot> x + - (b \<cdot> x)" |
125 by (simp add: negate_eq1 mult_assoc2) |
125 by (simp add: negate_eq1 mult_assoc2) |
126 also from x have "\<dots> = a \<cdot> x - (b \<cdot> x)" |
126 also from x have "\<dots> = a \<cdot> x - (b \<cdot> x)" |