Metamath Proof Explorer


Theorem lmodnegadd

Description: Distribute negation through addition of scalar products. (Contributed by NM, 9-Apr-2015)

Ref Expression
Hypotheses lmodnegadd.v 𝑉 = ( Base ‘ 𝑊 )
lmodnegadd.p + = ( +g𝑊 )
lmodnegadd.t · = ( ·𝑠𝑊 )
lmodnegadd.n 𝑁 = ( invg𝑊 )
lmodnegadd.r 𝑅 = ( Scalar ‘ 𝑊 )
lmodnegadd.k 𝐾 = ( Base ‘ 𝑅 )
lmodnegadd.i 𝐼 = ( invg𝑅 )
lmodnegadd.w ( 𝜑𝑊 ∈ LMod )
lmodnegadd.a ( 𝜑𝐴𝐾 )
lmodnegadd.b ( 𝜑𝐵𝐾 )
lmodnegadd.x ( 𝜑𝑋𝑉 )
lmodnegadd.y ( 𝜑𝑌𝑉 )
Assertion lmodnegadd ( 𝜑 → ( 𝑁 ‘ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) ) = ( ( ( 𝐼𝐴 ) · 𝑋 ) + ( ( 𝐼𝐵 ) · 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 lmodnegadd.v 𝑉 = ( Base ‘ 𝑊 )
2 lmodnegadd.p + = ( +g𝑊 )
3 lmodnegadd.t · = ( ·𝑠𝑊 )
4 lmodnegadd.n 𝑁 = ( invg𝑊 )
5 lmodnegadd.r 𝑅 = ( Scalar ‘ 𝑊 )
6 lmodnegadd.k 𝐾 = ( Base ‘ 𝑅 )
7 lmodnegadd.i 𝐼 = ( invg𝑅 )
8 lmodnegadd.w ( 𝜑𝑊 ∈ LMod )
9 lmodnegadd.a ( 𝜑𝐴𝐾 )
10 lmodnegadd.b ( 𝜑𝐵𝐾 )
11 lmodnegadd.x ( 𝜑𝑋𝑉 )
12 lmodnegadd.y ( 𝜑𝑌𝑉 )
13 lmodabl ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
14 8 13 syl ( 𝜑𝑊 ∈ Abel )
15 1 5 3 6 lmodvscl ( ( 𝑊 ∈ LMod ∧ 𝐴𝐾𝑋𝑉 ) → ( 𝐴 · 𝑋 ) ∈ 𝑉 )
16 8 9 11 15 syl3anc ( 𝜑 → ( 𝐴 · 𝑋 ) ∈ 𝑉 )
17 1 5 3 6 lmodvscl ( ( 𝑊 ∈ LMod ∧ 𝐵𝐾𝑌𝑉 ) → ( 𝐵 · 𝑌 ) ∈ 𝑉 )
18 8 10 12 17 syl3anc ( 𝜑 → ( 𝐵 · 𝑌 ) ∈ 𝑉 )
19 1 2 4 ablinvadd ( ( 𝑊 ∈ Abel ∧ ( 𝐴 · 𝑋 ) ∈ 𝑉 ∧ ( 𝐵 · 𝑌 ) ∈ 𝑉 ) → ( 𝑁 ‘ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) ) = ( ( 𝑁 ‘ ( 𝐴 · 𝑋 ) ) + ( 𝑁 ‘ ( 𝐵 · 𝑌 ) ) ) )
20 14 16 18 19 syl3anc ( 𝜑 → ( 𝑁 ‘ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) ) = ( ( 𝑁 ‘ ( 𝐴 · 𝑋 ) ) + ( 𝑁 ‘ ( 𝐵 · 𝑌 ) ) ) )
21 1 5 3 4 6 7 8 11 9 lmodvsneg ( 𝜑 → ( 𝑁 ‘ ( 𝐴 · 𝑋 ) ) = ( ( 𝐼𝐴 ) · 𝑋 ) )
22 1 5 3 4 6 7 8 12 10 lmodvsneg ( 𝜑 → ( 𝑁 ‘ ( 𝐵 · 𝑌 ) ) = ( ( 𝐼𝐵 ) · 𝑌 ) )
23 21 22 oveq12d ( 𝜑 → ( ( 𝑁 ‘ ( 𝐴 · 𝑋 ) ) + ( 𝑁 ‘ ( 𝐵 · 𝑌 ) ) ) = ( ( ( 𝐼𝐴 ) · 𝑋 ) + ( ( 𝐼𝐵 ) · 𝑌 ) ) )
24 20 23 eqtrd ( 𝜑 → ( 𝑁 ‘ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) ) = ( ( ( 𝐼𝐴 ) · 𝑋 ) + ( ( 𝐼𝐵 ) · 𝑌 ) ) )