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 
|- .+ = ( +g ` W )
clmvsubval.m 
|- .- = ( -g ` W )
clmvsubval.f 
|- F = ( Scalar ` W )
clmvsubval.s 
|- .x. = ( .s ` W )
Assertion clmvsubval2 
|- ( ( W e. CMod /\ A e. V /\ B e. V ) -> ( A .- B ) = ( ( -u 1 .x. B ) .+ A ) )

Proof

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