This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → ( 𝑁 ‘ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) ) = ( ( ( 𝐼 ‘ 𝐴 ) · 𝑋 ) + ( ( 𝐼 ‘ 𝐵 ) · 𝑌 ) ) )