Metamath Proof Explorer


Theorem clmvsubval2

Description: Value of vector subtraction on a subcomplex module. (Contributed by Mario Carneiro, 19-Nov-2013) (Revised by AV, 7-Oct-2021)

Ref Expression
Hypotheses clmvsubval.v V = Base W
clmvsubval.p + ˙ = + W
clmvsubval.m - ˙ = - W
clmvsubval.f F = Scalar W
clmvsubval.s · ˙ = W
Assertion clmvsubval2 W CMod A V B V A - ˙ B = -1 · ˙ B + ˙ A

Proof

Step Hyp Ref Expression
1 clmvsubval.v V = Base W
2 clmvsubval.p + ˙ = + W
3 clmvsubval.m - ˙ = - W
4 clmvsubval.f F = Scalar W
5 clmvsubval.s · ˙ = W
6 1 2 3 4 5 clmvsubval W CMod A V B V A - ˙ B = A + ˙ -1 · ˙ B
7 clmabl W CMod W Abel
8 7 3ad2ant1 W CMod A V B V W Abel
9 simp2 W CMod A V B V A V
10 simpl W CMod B V W CMod
11 eqid Base F = Base F
12 4 11 clmneg1 W CMod 1 Base F
13 12 adantr W CMod B V 1 Base F
14 simpr W CMod B V B V
15 1 4 5 11 clmvscl W CMod 1 Base F B V -1 · ˙ B V
16 10 13 14 15 syl3anc W CMod B V -1 · ˙ B V
17 16 3adant2 W CMod A V B V -1 · ˙ B V
18 1 2 ablcom W Abel A V -1 · ˙ B V A + ˙ -1 · ˙ B = -1 · ˙ B + ˙ A
19 8 9 17 18 syl3anc W CMod A V B V A + ˙ -1 · ˙ B = -1 · ˙ B + ˙ A
20 6 19 eqtrd W CMod A V B V A - ˙ B = -1 · ˙ B + ˙ A