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 ⊢ 𝑉 = ( Base ‘ 𝑊 )
clmpm1dir.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
clmpm1dir.a ⊢ + = ( +g ‘ 𝑊 )
Assertion clmsub4 ( ( 𝑊 ∈ ℂMod ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( 𝐴 + 𝐵 ) + ( - 1 · ( 𝐶 + 𝐷 ) ) ) = ( ( 𝐴 + ( - 1 · 𝐶 ) ) + ( 𝐵 + ( - 1 · 𝐷 ) ) ) )

Proof

Step Hyp Ref Expression
1 clmpm1dir.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 clmpm1dir.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
3 clmpm1dir.a ⊢ + = ( +g ‘ 𝑊 )
4 simpl ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → 𝑊 ∈ ℂMod )
5 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
6 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
7 5 6 clmneg1 ⊢ ( 𝑊 ∈ ℂMod → - 1 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
8 7 adantr ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → - 1 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
9 simpl ⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) → 𝐶 ∈ 𝑉 )
10 9 adantl ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → 𝐶 ∈ 𝑉 )
11 simpr ⊢ ( ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) → 𝐷 ∈ 𝑉 )
12 11 adantl ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → 𝐷 ∈ 𝑉 )
13 1 5 2 6 3 clmvsdi ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( - 1 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( - 1 · ( 𝐶 + 𝐷 ) ) = ( ( - 1 · 𝐶 ) + ( - 1 · 𝐷 ) ) )
14 4 8 10 12 13 syl13anc ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( - 1 · ( 𝐶 + 𝐷 ) ) = ( ( - 1 · 𝐶 ) + ( - 1 · 𝐷 ) ) )
15 14 3adant2 ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( - 1 · ( 𝐶 + 𝐷 ) ) = ( ( - 1 · 𝐶 ) + ( - 1 · 𝐷 ) ) )
16 15 oveq2d ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( 𝐴 + 𝐵 ) + ( - 1 · ( 𝐶 + 𝐷 ) ) ) = ( ( 𝐴 + 𝐵 ) + ( ( - 1 · 𝐶 ) + ( - 1 · 𝐷 ) ) ) )
17 clmabl ⊢ ( 𝑊 ∈ ℂMod → 𝑊 ∈ Abel )
18 ablcmn ⊢ ( 𝑊 ∈ Abel → 𝑊 ∈ CMnd )
19 17 18 syl ⊢ ( 𝑊 ∈ ℂMod → 𝑊 ∈ CMnd )
20 19 3ad2ant1 ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → 𝑊 ∈ CMnd )
21 simp2 ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) )
22 simpl ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐶 ∈ 𝑉 ) → 𝑊 ∈ ℂMod )
23 7 adantr ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐶 ∈ 𝑉 ) → - 1 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
24 simpr ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐶 ∈ 𝑉 ) → 𝐶 ∈ 𝑉 )
25 1 5 2 6 clmvscl ⊢ ( ( 𝑊 ∈ ℂMod ∧ - 1 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐶 ∈ 𝑉 ) → ( - 1 · 𝐶 ) ∈ 𝑉 )
26 22 23 24 25 syl3anc ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐶 ∈ 𝑉 ) → ( - 1 · 𝐶 ) ∈ 𝑉 )
27 simpl ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐷 ∈ 𝑉 ) → 𝑊 ∈ ℂMod )
28 7 adantr ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐷 ∈ 𝑉 ) → - 1 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
29 simpr ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐷 ∈ 𝑉 ) → 𝐷 ∈ 𝑉 )
30 1 5 2 6 clmvscl ⊢ ( ( 𝑊 ∈ ℂMod ∧ - 1 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐷 ∈ 𝑉 ) → ( - 1 · 𝐷 ) ∈ 𝑉 )
31 27 28 29 30 syl3anc ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐷 ∈ 𝑉 ) → ( - 1 · 𝐷 ) ∈ 𝑉 )
32 26 31 anim12dan ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( - 1 · 𝐶 ) ∈ 𝑉 ∧ ( - 1 · 𝐷 ) ∈ 𝑉 ) )
33 32 3adant2 ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( - 1 · 𝐶 ) ∈ 𝑉 ∧ ( - 1 · 𝐷 ) ∈ 𝑉 ) )
34 1 3 cmn4 ⊢ ( ( 𝑊 ∈ CMnd ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( ( - 1 · 𝐶 ) ∈ 𝑉 ∧ ( - 1 · 𝐷 ) ∈ 𝑉 ) ) → ( ( 𝐴 + 𝐵 ) + ( ( - 1 · 𝐶 ) + ( - 1 · 𝐷 ) ) ) = ( ( 𝐴 + ( - 1 · 𝐶 ) ) + ( 𝐵 + ( - 1 · 𝐷 ) ) ) )
35 20 21 33 34 syl3anc ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( 𝐴 + 𝐵 ) + ( ( - 1 · 𝐶 ) + ( - 1 · 𝐷 ) ) ) = ( ( 𝐴 + ( - 1 · 𝐶 ) ) + ( 𝐵 + ( - 1 · 𝐷 ) ) ) )
36 16 35 eqtrd ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( 𝐴 + 𝐵 ) + ( - 1 · ( 𝐶 + 𝐷 ) ) ) = ( ( 𝐴 + ( - 1 · 𝐶 ) ) + ( 𝐵 + ( - 1 · 𝐷 ) ) ) )