Metamath Proof Explorer

Theorem clmvsubval

Description: Value of vector subtraction in terms of addition in a subcomplex module. Analogue of lmodvsubval2 . (Contributed by NM, 31-Mar-2014) (Revised by AV, 7-Oct-2021)

Ref Expression
Hypotheses clmvsubval.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
clmvsubval.p ⊢ + = ( +g ‘ 𝑊 )
clmvsubval.m ⊢ − = ( -g ‘ 𝑊 )
clmvsubval.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
clmvsubval.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
Assertion clmvsubval ( ( 𝑊 ∈ ℂ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 clmlmod ⊢ ( 𝑊 ∈ ℂMod → 𝑊 ∈ LMod )
7 eqid ⊢ ( invg ‘ 𝐹 ) = ( invg ‘ 𝐹 )
8 eqid ⊢ ( 1r ‘ 𝐹 ) = ( 1r ‘ 𝐹 )
9 1 2 3 4 5 7 8 lmodvsubval2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 − 𝐵 ) = ( 𝐴 + ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) · 𝐵 ) ) )
10 6 9 syl3an1 ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 − 𝐵 ) = ( 𝐴 + ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) · 𝐵 ) ) )
11 4 clm1 ⊢ ( 𝑊 ∈ ℂMod → 1 = ( 1r ‘ 𝐹 ) )
12 11 eqcomd ⊢ ( 𝑊 ∈ ℂMod → ( 1r ‘ 𝐹 ) = 1 )
13 12 fveq2d ⊢ ( 𝑊 ∈ ℂMod → ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) = ( ( invg ‘ 𝐹 ) ‘ 1 ) )
14 4 clmring ⊢ ( 𝑊 ∈ ℂMod → 𝐹 ∈ Ring )
15 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
16 15 8 ringidcl ⊢ ( 𝐹 ∈ Ring → ( 1r ‘ 𝐹 ) ∈ ( Base ‘ 𝐹 ) )
17 14 16 syl ⊢ ( 𝑊 ∈ ℂMod → ( 1r ‘ 𝐹 ) ∈ ( Base ‘ 𝐹 ) )
18 11 17 eqeltrd ⊢ ( 𝑊 ∈ ℂMod → 1 ∈ ( Base ‘ 𝐹 ) )
19 4 15 clmneg ⊢ ( ( 𝑊 ∈ ℂMod ∧ 1 ∈ ( Base ‘ 𝐹 ) ) → - 1 = ( ( invg ‘ 𝐹 ) ‘ 1 ) )
20 18 19 mpdan ⊢ ( 𝑊 ∈ ℂMod → - 1 = ( ( invg ‘ 𝐹 ) ‘ 1 ) )
21 13 20 eqtr4d ⊢ ( 𝑊 ∈ ℂMod → ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) = - 1 )
22 21 3ad2ant1 ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) = - 1 )
23 22 oveq1d ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) · 𝐵 ) = ( - 1 · 𝐵 ) )
24 23 oveq2d ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 + ( ( ( invg ‘ 𝐹 ) ‘ ( 1r ‘ 𝐹 ) ) · 𝐵 ) ) = ( 𝐴 + ( - 1 · 𝐵 ) ) )
25 10 24 eqtrd ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 − 𝐵 ) = ( 𝐴 + ( - 1 · 𝐵 ) ) )