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	$⊢ \underset{˙}{+} = +_{W}$
	lmodnegadd.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	lmodnegadd.n	$⊢ N = {inv}_{g} (W)$
	lmodnegadd.r	$⊢ R = Scalar (W)$
	lmodnegadd.k	$⊢ K = {Base}_{R}$
	lmodnegadd.i	$⊢ I = {inv}_{g} (R)$
	lmodnegadd.w	$⊢ φ \to W \in LMod$
	lmodnegadd.a	$⊢ φ \to A \in K$
	lmodnegadd.b	$⊢ φ \to B \in K$
	lmodnegadd.x	$⊢ φ \to X \in V$
	lmodnegadd.y	$⊢ φ \to Y \in V$
Assertion	lmodnegadd	$⊢ φ \to N ((A \underset{˙}{\cdot} X) \underset{˙}{+} (B \underset{˙}{\cdot} Y)) = (I (A) \underset{˙}{\cdot} X) \underset{˙}{+} (I (B) \underset{˙}{\cdot} Y)$

Proof

Step	Hyp	Ref	Expression
1		lmodnegadd.v	$⊢ V = {Base}_{W}$
2		lmodnegadd.p	$⊢ \underset{˙}{+} = +_{W}$
3		lmodnegadd.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
4		lmodnegadd.n	$⊢ N = {inv}_{g} (W)$
5		lmodnegadd.r	$⊢ R = Scalar (W)$
6		lmodnegadd.k	$⊢ K = {Base}_{R}$
7		lmodnegadd.i	$⊢ I = {inv}_{g} (R)$
8		lmodnegadd.w	$⊢ φ \to W \in LMod$
9		lmodnegadd.a	$⊢ φ \to A \in K$
10		lmodnegadd.b	$⊢ φ \to B \in K$
11		lmodnegadd.x	$⊢ φ \to X \in V$
12		lmodnegadd.y	$⊢ φ \to Y \in V$
13		lmodabl	$⊢ W \in LMod \to W \in Abel$
14	8 13	syl	$⊢ φ \to W \in Abel$
15	1 5 3 6	lmodvscl	$⊢ (W \in LMod \land A \in K \land X \in V) \to A \underset{˙}{\cdot} X \in V$
16	8 9 11 15	syl3anc	$⊢ φ \to A \underset{˙}{\cdot} X \in V$
17	1 5 3 6	lmodvscl	$⊢ (W \in LMod \land B \in K \land Y \in V) \to B \underset{˙}{\cdot} Y \in V$
18	8 10 12 17	syl3anc	$⊢ φ \to B \underset{˙}{\cdot} Y \in V$
19	1 2 4	ablinvadd	$⊢ (W \in Abel \land A \underset{˙}{\cdot} X \in V \land B \underset{˙}{\cdot} Y \in V) \to N ((A \underset{˙}{\cdot} X) \underset{˙}{+} (B \underset{˙}{\cdot} Y)) = N (A \underset{˙}{\cdot} X) \underset{˙}{+} N (B \underset{˙}{\cdot} Y)$
20	14 16 18 19	syl3anc	$⊢ φ \to N ((A \underset{˙}{\cdot} X) \underset{˙}{+} (B \underset{˙}{\cdot} Y)) = N (A \underset{˙}{\cdot} X) \underset{˙}{+} N (B \underset{˙}{\cdot} Y)$
21	1 5 3 4 6 7 8 11 9	lmodvsneg	$⊢ φ \to N (A \underset{˙}{\cdot} X) = I (A) \underset{˙}{\cdot} X$
22	1 5 3 4 6 7 8 12 10	lmodvsneg	$⊢ φ \to N (B \underset{˙}{\cdot} Y) = I (B) \underset{˙}{\cdot} Y$
23	21 22	oveq12d	$⊢ φ \to N (A \underset{˙}{\cdot} X) \underset{˙}{+} N (B \underset{˙}{\cdot} Y) = (I (A) \underset{˙}{\cdot} X) \underset{˙}{+} (I (B) \underset{˙}{\cdot} Y)$
24	20 23	eqtrd	$⊢ φ \to N ((A \underset{˙}{\cdot} X) \underset{˙}{+} (B \underset{˙}{\cdot} Y)) = (I (A) \underset{˙}{\cdot} X) \underset{˙}{+} (I (B) \underset{˙}{\cdot} Y)$

Metamath Proof Explorer

Theorem lmodnegadd

Proof