This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clmnegsubdi2

Description: Distribution of negative over vector subtraction. (Contributed by NM, 6-Aug-2007) (Revised by AV, 29-Sep-2021)

Ref Expression
Hypotheses clmpm1dir.v 
|- V = ( Base ` W )
clmpm1dir.s 
|- .x. = ( .s ` W )
clmpm1dir.a 
|- .+ = ( +g ` W )
Assertion clmnegsubdi2 
|- ( ( W e. CMod /\ A e. V /\ B e. V ) -> ( -u 1 .x. ( A .+ ( -u 1 .x. B ) ) ) = ( B .+ ( -u 1 .x. A ) ) )

Proof

Step Hyp Ref Expression
1 clmpm1dir.v 
 |-  V = ( Base ` W )
2 clmpm1dir.s 
 |-  .x. = ( .s ` W )
3 clmpm1dir.a 
 |-  .+ = ( +g ` W )
4 simp1 
 |-  ( ( W e. CMod /\ A e. V /\ B e. V ) -> W e. CMod )
5 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
6 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
7 5 6 clmneg1 
 |-  ( W e. CMod -> -u 1 e. ( Base ` ( Scalar ` W ) ) )
8 7 3ad2ant1 
 |-  ( ( W e. CMod /\ A e. V /\ B e. V ) -> -u 1 e. ( Base ` ( Scalar ` W ) ) )
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 7 adantr 
 |-  ( ( W e. CMod /\ B e. V ) -> -u 1 e. ( Base ` ( Scalar ` W ) ) )
12 simpr 
 |-  ( ( W e. CMod /\ B e. V ) -> B e. V )
13 1 5 2 6 clmvscl 
 |-  ( ( W e. CMod /\ -u 1 e. ( Base ` ( Scalar ` W ) ) /\ B e. V ) -> ( -u 1 .x. B ) e. V )
14 10 11 12 13 syl3anc 
 |-  ( ( W e. CMod /\ B e. V ) -> ( -u 1 .x. B ) e. V )
15 14 3adant2 
 |-  ( ( W e. CMod /\ A e. V /\ B e. V ) -> ( -u 1 .x. B ) e. V )
16 1 5 2 6 3 clmvsdi 
 |-  ( ( W e. CMod /\ ( -u 1 e. ( Base ` ( Scalar ` W ) ) /\ A e. V /\ ( -u 1 .x. B ) e. V ) ) -> ( -u 1 .x. ( A .+ ( -u 1 .x. B ) ) ) = ( ( -u 1 .x. A ) .+ ( -u 1 .x. ( -u 1 .x. B ) ) ) )
17 4 8 9 15 16 syl13anc 
 |-  ( ( W e. CMod /\ A e. V /\ B e. V ) -> ( -u 1 .x. ( A .+ ( -u 1 .x. B ) ) ) = ( ( -u 1 .x. A ) .+ ( -u 1 .x. ( -u 1 .x. B ) ) ) )
18 1 2 3 clmnegneg 
 |-  ( ( W e. CMod /\ B e. V ) -> ( -u 1 .x. ( -u 1 .x. B ) ) = B )
19 18 3adant2 
 |-  ( ( W e. CMod /\ A e. V /\ B e. V ) -> ( -u 1 .x. ( -u 1 .x. B ) ) = B )
20 19 oveq2d 
 |-  ( ( W e. CMod /\ A e. V /\ B e. V ) -> ( ( -u 1 .x. A ) .+ ( -u 1 .x. ( -u 1 .x. B ) ) ) = ( ( -u 1 .x. A ) .+ B ) )
21 clmabl 
 |-  ( W e. CMod -> W e. Abel )
22 21 3ad2ant1 
 |-  ( ( W e. CMod /\ A e. V /\ B e. V ) -> W e. Abel )
23 simpl 
 |-  ( ( W e. CMod /\ A e. V ) -> W e. CMod )
24 7 adantr 
 |-  ( ( W e. CMod /\ A e. V ) -> -u 1 e. ( Base ` ( Scalar ` W ) ) )
25 simpr 
 |-  ( ( W e. CMod /\ A e. V ) -> A e. V )
26 1 5 2 6 clmvscl 
 |-  ( ( W e. CMod /\ -u 1 e. ( Base ` ( Scalar ` W ) ) /\ A e. V ) -> ( -u 1 .x. A ) e. V )
27 23 24 25 26 syl3anc 
 |-  ( ( W e. CMod /\ A e. V ) -> ( -u 1 .x. A ) e. V )
28 27 3adant3 
 |-  ( ( W e. CMod /\ A e. V /\ B e. V ) -> ( -u 1 .x. A ) e. V )
29 simp3 
 |-  ( ( W e. CMod /\ A e. V /\ B e. V ) -> B e. V )
30 1 3 ablcom 
 |-  ( ( W e. Abel /\ ( -u 1 .x. A ) e. V /\ B e. V ) -> ( ( -u 1 .x. A ) .+ B ) = ( B .+ ( -u 1 .x. A ) ) )
31 22 28 29 30 syl3anc 
 |-  ( ( W e. CMod /\ A e. V /\ B e. V ) -> ( ( -u 1 .x. A ) .+ B ) = ( B .+ ( -u 1 .x. A ) ) )
32 17 20 31 3eqtrd 
 |-  ( ( W e. CMod /\ A e. V /\ B e. V ) -> ( -u 1 .x. ( A .+ ( -u 1 .x. B ) ) ) = ( B .+ ( -u 1 .x. A ) ) )