Metamath Proof Explorer

Theorem clmsub4

Description: Rearrangement of 4 terms in a mixed vector addition and subtraction. (Contributed by NM, 5-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 clmsub4 
|- ( ( W e. CMod /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( A .+ B ) .+ ( -u 1 .x. ( C .+ D ) ) ) = ( ( A .+ ( -u 1 .x. C ) ) .+ ( B .+ ( -u 1 .x. D ) ) ) )

Proof

Step Hyp Ref Expression
1 clmpm1dir.v 
 |-  V = ( Base ` W )
2 clmpm1dir.s 
 |-  .x. = ( .s ` W )
3 clmpm1dir.a 
 |-  .+ = ( +g ` W )
4 simpl 
 |-  ( ( W e. CMod /\ ( C e. V /\ D 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 adantr 
 |-  ( ( W e. CMod /\ ( C e. V /\ D e. V ) ) -> -u 1 e. ( Base ` ( Scalar ` W ) ) )
9 simpl 
 |-  ( ( C e. V /\ D e. V ) -> C e. V )
10 9 adantl 
 |-  ( ( W e. CMod /\ ( C e. V /\ D e. V ) ) -> C e. V )
11 simpr 
 |-  ( ( C e. V /\ D e. V ) -> D e. V )
12 11 adantl 
 |-  ( ( W e. CMod /\ ( C e. V /\ D e. V ) ) -> D e. V )
13 1 5 2 6 3 clmvsdi 
 |-  ( ( W e. CMod /\ ( -u 1 e. ( Base ` ( Scalar ` W ) ) /\ C e. V /\ D e. V ) ) -> ( -u 1 .x. ( C .+ D ) ) = ( ( -u 1 .x. C ) .+ ( -u 1 .x. D ) ) )
14 4 8 10 12 13 syl13anc 
 |-  ( ( W e. CMod /\ ( C e. V /\ D e. V ) ) -> ( -u 1 .x. ( C .+ D ) ) = ( ( -u 1 .x. C ) .+ ( -u 1 .x. D ) ) )
15 14 3adant2 
 |-  ( ( W e. CMod /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( -u 1 .x. ( C .+ D ) ) = ( ( -u 1 .x. C ) .+ ( -u 1 .x. D ) ) )
16 15 oveq2d 
 |-  ( ( W e. CMod /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( A .+ B ) .+ ( -u 1 .x. ( C .+ D ) ) ) = ( ( A .+ B ) .+ ( ( -u 1 .x. C ) .+ ( -u 1 .x. D ) ) ) )
17 clmabl 
 |-  ( W e. CMod -> W e. Abel )
18 ablcmn 
 |-  ( W e. Abel -> W e. CMnd )
19 17 18 syl 
 |-  ( W e. CMod -> W e. CMnd )
20 19 3ad2ant1 
 |-  ( ( W e. CMod /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> W e. CMnd )
21 simp2 
 |-  ( ( W e. CMod /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( A e. V /\ B e. V ) )
22 simpl 
 |-  ( ( W e. CMod /\ C e. V ) -> W e. CMod )
23 7 adantr 
 |-  ( ( W e. CMod /\ C e. V ) -> -u 1 e. ( Base ` ( Scalar ` W ) ) )
24 simpr 
 |-  ( ( W e. CMod /\ C e. V ) -> C e. V )
25 1 5 2 6 clmvscl 
 |-  ( ( W e. CMod /\ -u 1 e. ( Base ` ( Scalar ` W ) ) /\ C e. V ) -> ( -u 1 .x. C ) e. V )
26 22 23 24 25 syl3anc 
 |-  ( ( W e. CMod /\ C e. V ) -> ( -u 1 .x. C ) e. V )
27 simpl 
 |-  ( ( W e. CMod /\ D e. V ) -> W e. CMod )
28 7 adantr 
 |-  ( ( W e. CMod /\ D e. V ) -> -u 1 e. ( Base ` ( Scalar ` W ) ) )
29 simpr 
 |-  ( ( W e. CMod /\ D e. V ) -> D e. V )
30 1 5 2 6 clmvscl 
 |-  ( ( W e. CMod /\ -u 1 e. ( Base ` ( Scalar ` W ) ) /\ D e. V ) -> ( -u 1 .x. D ) e. V )
31 27 28 29 30 syl3anc 
 |-  ( ( W e. CMod /\ D e. V ) -> ( -u 1 .x. D ) e. V )
32 26 31 anim12dan 
 |-  ( ( W e. CMod /\ ( C e. V /\ D e. V ) ) -> ( ( -u 1 .x. C ) e. V /\ ( -u 1 .x. D ) e. V ) )
33 32 3adant2 
 |-  ( ( W e. CMod /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( -u 1 .x. C ) e. V /\ ( -u 1 .x. D ) e. V ) )
34 1 3 cmn4 
 |-  ( ( W e. CMnd /\ ( A e. V /\ B e. V ) /\ ( ( -u 1 .x. C ) e. V /\ ( -u 1 .x. D ) e. V ) ) -> ( ( A .+ B ) .+ ( ( -u 1 .x. C ) .+ ( -u 1 .x. D ) ) ) = ( ( A .+ ( -u 1 .x. C ) ) .+ ( B .+ ( -u 1 .x. D ) ) ) )
35 20 21 33 34 syl3anc 
 |-  ( ( W e. CMod /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( A .+ B ) .+ ( ( -u 1 .x. C ) .+ ( -u 1 .x. D ) ) ) = ( ( A .+ ( -u 1 .x. C ) ) .+ ( B .+ ( -u 1 .x. D ) ) ) )
36 16 35 eqtrd 
 |-  ( ( W e. CMod /\ ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( ( A .+ B ) .+ ( -u 1 .x. ( C .+ D ) ) ) = ( ( A .+ ( -u 1 .x. C ) ) .+ ( B .+ ( -u 1 .x. D ) ) ) )