Theorem lmodnegadd

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

	Ref	Expression
Hypotheses	lmodnegadd.v	|- V = ( Base ` W )
	lmodnegadd.p	|- .+ = ( +g ` W )
	lmodnegadd.t	|- .x. = ( .s ` W )
	lmodnegadd.n	|- N = ( invg ` W )
	lmodnegadd.r	|- R = ( Scalar ` W )
	lmodnegadd.k	|- K = ( Base ` R )
	lmodnegadd.i	|- I = ( invg ` R )
	lmodnegadd.w	|- ( ph -> W e. LMod )
	lmodnegadd.a	|- ( ph -> A e. K )
	lmodnegadd.b	|- ( ph -> B e. K )
	lmodnegadd.x	|- ( ph -> X e. V )
	lmodnegadd.y	|- ( ph -> Y e. V )
Assertion	lmodnegadd	|- ( ph -> ( N ` ( ( A .x. X ) .+ ( B .x. Y ) ) ) = ( ( ( I ` A ) .x. X ) .+ ( ( I ` B ) .x. Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		lmodnegadd.v	|- V = ( Base ` W )
2		lmodnegadd.p	|- .+ = ( +g ` W )
3		lmodnegadd.t	|- .x. = ( .s ` W )
4		lmodnegadd.n	|- N = ( invg ` W )
5		lmodnegadd.r	|- R = ( Scalar ` W )
6		lmodnegadd.k	|- K = ( Base ` R )
7		lmodnegadd.i	|- I = ( invg ` R )
8		lmodnegadd.w	|- ( ph -> W e. LMod )
9		lmodnegadd.a	|- ( ph -> A e. K )
10		lmodnegadd.b	|- ( ph -> B e. K )
11		lmodnegadd.x	|- ( ph -> X e. V )
12		lmodnegadd.y	|- ( ph -> Y e. V )
13		lmodabl	|- ( W e. LMod -> W e. Abel )
14	8 13	syl	|- ( ph -> W e. Abel )
15	1 5 3 6	lmodvscl	|- ( ( W e. LMod /\ A e. K /\ X e. V ) -> ( A .x. X ) e. V )
16	8 9 11 15	syl3anc	|- ( ph -> ( A .x. X ) e. V )
17	1 5 3 6	lmodvscl	|- ( ( W e. LMod /\ B e. K /\ Y e. V ) -> ( B .x. Y ) e. V )
18	8 10 12 17	syl3anc	|- ( ph -> ( B .x. Y ) e. V )
19	1 2 4	ablinvadd	|- ( ( W e. Abel /\ ( A .x. X ) e. V /\ ( B .x. Y ) e. V ) -> ( N ` ( ( A .x. X ) .+ ( B .x. Y ) ) ) = ( ( N ` ( A .x. X ) ) .+ ( N ` ( B .x. Y ) ) ) )
20	14 16 18 19	syl3anc	|- ( ph -> ( N ` ( ( A .x. X ) .+ ( B .x. Y ) ) ) = ( ( N ` ( A .x. X ) ) .+ ( N ` ( B .x. Y ) ) ) )
21	1 5 3 4 6 7 8 11 9	lmodvsneg	|- ( ph -> ( N ` ( A .x. X ) ) = ( ( I ` A ) .x. X ) )
22	1 5 3 4 6 7 8 12 10	lmodvsneg	|- ( ph -> ( N ` ( B .x. Y ) ) = ( ( I ` B ) .x. Y ) )
23	21 22	oveq12d	|- ( ph -> ( ( N ` ( A .x. X ) ) .+ ( N ` ( B .x. Y ) ) ) = ( ( ( I ` A ) .x. X ) .+ ( ( I ` B ) .x. Y ) ) )
24	20 23	eqtrd	|- ( ph -> ( N ` ( ( A .x. X ) .+ ( B .x. Y ) ) ) = ( ( ( I ` A ) .x. X ) .+ ( ( I ` B ) .x. Y ) ) )