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