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