Metamath Proof Explorer

Theorem clmpm1dir

Description: Subtractive distributive law for the scalar product of a subcomplex module. (Contributed by NM, 31-Jul-2007) (Revised by AV, 21-Sep-2021)

Ref Expression
Hypotheses clmpm1dir.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
clmpm1dir.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
clmpm1dir.a ⊢ + = ( +g ‘ 𝑊 )
clmpm1dir.k ⊢ 𝐾 = ( Base ‘ ( Scalar ‘ 𝑊 ) )
Assertion clmpm1dir ( ( 𝑊 ∈ ℂMod ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 − 𝐵 ) · 𝐶 ) = ( ( 𝐴 · 𝐶 ) + ( - 1 · ( 𝐵 · 𝐶 ) ) ) )

Proof

Step Hyp Ref Expression
1 clmpm1dir.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 clmpm1dir.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
3 clmpm1dir.a ⊢ + = ( +g ‘ 𝑊 )
4 clmpm1dir.k ⊢ 𝐾 = ( Base ‘ ( Scalar ‘ 𝑊 ) )
5 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
6 eqid ⊢ ( -g ‘ 𝑊 ) = ( -g ‘ 𝑊 )
7 simpl ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐶 ∈ 𝑉 ) ) → 𝑊 ∈ ℂMod )
8 simpr1 ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐴 ∈ 𝐾 )
9 simpr2 ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐵 ∈ 𝐾 )
10 simpr3 ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐶 ∈ 𝑉 )
11 1 2 5 4 6 7 8 9 10 clmsubdir ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 − 𝐵 ) · 𝐶 ) = ( ( 𝐴 · 𝐶 ) ( -g ‘ 𝑊 ) ( 𝐵 · 𝐶 ) ) )
12 1 5 2 4 clmvscl ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐴 · 𝐶 ) ∈ 𝑉 )
13 7 8 10 12 syl3anc ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐴 · 𝐶 ) ∈ 𝑉 )
14 1 5 2 4 clmvscl ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐵 ∈ 𝐾 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐵 · 𝐶 ) ∈ 𝑉 )
15 7 9 10 14 syl3anc ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐵 · 𝐶 ) ∈ 𝑉 )
16 eqid ⊢ ( invg ‘ 𝑊 ) = ( invg ‘ 𝑊 )
17 1 3 16 6 grpsubval ⊢ ( ( ( 𝐴 · 𝐶 ) ∈ 𝑉 ∧ ( 𝐵 · 𝐶 ) ∈ 𝑉 ) → ( ( 𝐴 · 𝐶 ) ( -g ‘ 𝑊 ) ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 · 𝐶 ) + ( ( invg ‘ 𝑊 ) ‘ ( 𝐵 · 𝐶 ) ) ) )
18 13 15 17 syl2anc ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 · 𝐶 ) ( -g ‘ 𝑊 ) ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 · 𝐶 ) + ( ( invg ‘ 𝑊 ) ‘ ( 𝐵 · 𝐶 ) ) ) )
19 1 16 5 2 clmvneg1 ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝐵 · 𝐶 ) ∈ 𝑉 ) → ( - 1 · ( 𝐵 · 𝐶 ) ) = ( ( invg ‘ 𝑊 ) ‘ ( 𝐵 · 𝐶 ) ) )
20 19 eqcomd ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝐵 · 𝐶 ) ∈ 𝑉 ) → ( ( invg ‘ 𝑊 ) ‘ ( 𝐵 · 𝐶 ) ) = ( - 1 · ( 𝐵 · 𝐶 ) ) )
21 7 15 20 syl2anc ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( invg ‘ 𝑊 ) ‘ ( 𝐵 · 𝐶 ) ) = ( - 1 · ( 𝐵 · 𝐶 ) ) )
22 21 oveq2d ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 · 𝐶 ) + ( ( invg ‘ 𝑊 ) ‘ ( 𝐵 · 𝐶 ) ) ) = ( ( 𝐴 · 𝐶 ) + ( - 1 · ( 𝐵 · 𝐶 ) ) ) )
23 11 18 22 3eqtrd ⊢ ( ( 𝑊 ∈ ℂMod ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 − 𝐵 ) · 𝐶 ) = ( ( 𝐴 · 𝐶 ) + ( - 1 · ( 𝐵 · 𝐶 ) ) ) )