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 ⊢ 𝑉 = ( Base ‘ 𝑊 )
clmvsubval.p ⊢ + = ( +g ‘ 𝑊 )
clmvsubval.m ⊢ − = ( -g ‘ 𝑊 )
clmvsubval.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
clmvsubval.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
Assertion clmvsubval2 ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 − 𝐵 ) = ( ( - 1 · 𝐵 ) + 𝐴 ) )

Proof

Step Hyp Ref Expression
1 clmvsubval.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 clmvsubval.p ⊢ + = ( +g ‘ 𝑊 )
3 clmvsubval.m ⊢ − = ( -g ‘ 𝑊 )
4 clmvsubval.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
5 clmvsubval.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
6 1 2 3 4 5 clmvsubval ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 − 𝐵 ) = ( 𝐴 + ( - 1 · 𝐵 ) ) )
7 clmabl ⊢ ( 𝑊 ∈ ℂMod → 𝑊 ∈ Abel )
8 7 3ad2ant1 ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝑊 ∈ Abel )
9 simp2 ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 )
10 simpl ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉 ) → 𝑊 ∈ ℂMod )
11 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
12 4 11 clmneg1 ⊢ ( 𝑊 ∈ ℂMod → - 1 ∈ ( Base ‘ 𝐹 ) )
13 12 adantr ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉 ) → - 1 ∈ ( Base ‘ 𝐹 ) )
14 simpr ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉 ) → 𝐵 ∈ 𝑉 )
15 1 4 5 11 clmvscl ⊢ ( ( 𝑊 ∈ ℂMod ∧ - 1 ∈ ( Base ‘ 𝐹 ) ∧ 𝐵 ∈ 𝑉 ) → ( - 1 · 𝐵 ) ∈ 𝑉 )
16 10 13 14 15 syl3anc ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝑉 ) → ( - 1 · 𝐵 ) ∈ 𝑉 )
17 16 3adant2 ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( - 1 · 𝐵 ) ∈ 𝑉 )
18 1 2 ablcom ⊢ ( ( 𝑊 ∈ Abel ∧ 𝐴 ∈ 𝑉 ∧ ( - 1 · 𝐵 ) ∈ 𝑉 ) → ( 𝐴 + ( - 1 · 𝐵 ) ) = ( ( - 1 · 𝐵 ) + 𝐴 ) )
19 8 9 17 18 syl3anc ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 + ( - 1 · 𝐵 ) ) = ( ( - 1 · 𝐵 ) + 𝐴 ) )
20 6 19 eqtrd ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 − 𝐵 ) = ( ( - 1 · 𝐵 ) + 𝐴 ) )