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

Proof

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