lmodvsinv2

Description: Multiplying a negated vector by a scalar. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Hypotheses	lmodvsinv2.b	$⊢ B = {Base}_{W}$
	lmodvsinv2.f	$⊢ F = Scalar (W)$
	lmodvsinv2.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	lmodvsinv2.n	$⊢ N = {inv}_{g} (W)$
	lmodvsinv2.k	$⊢ K = {Base}_{F}$
Assertion	lmodvsinv2	$⊢ (W \in LMod \land R \in K \land X \in B) \to R \underset{˙}{\cdot} N (X) = N (R \underset{˙}{\cdot} X)$

Proof

Step	Hyp	Ref	Expression
1		lmodvsinv2.b	$⊢ B = {Base}_{W}$
2		lmodvsinv2.f	$⊢ F = Scalar (W)$
3		lmodvsinv2.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
4		lmodvsinv2.n	$⊢ N = {inv}_{g} (W)$
5		lmodvsinv2.k	$⊢ K = {Base}_{F}$
6		simp1	$⊢ (W \in LMod \land R \in K \land X \in B) \to W \in LMod$
7		lmodgrp	$⊢ W \in LMod \to W \in Grp$
8	6 7	syl	$⊢ (W \in LMod \land R \in K \land X \in B) \to W \in Grp$
9		simp3	$⊢ (W \in LMod \land R \in K \land X \in B) \to X \in B$
10		eqid	$⊢ +_{W} = +_{W}$
11		eqid	$⊢ 0_{W} = 0_{W}$
12	1 10 11 4	grprinv	$⊢ (W \in Grp \land X \in B) \to X +_{W} N (X) = 0_{W}$
13	8 9 12	syl2anc	$⊢ (W \in LMod \land R \in K \land X \in B) \to X +_{W} N (X) = 0_{W}$
14	13	oveq2d	$⊢ (W \in LMod \land R \in K \land X \in B) \to R \underset{˙}{\cdot} (X +_{W} N (X)) = R \underset{˙}{\cdot} 0_{W}$
15		simp2	$⊢ (W \in LMod \land R \in K \land X \in B) \to R \in K$
16	1 4	grpinvcl	$⊢ (W \in Grp \land X \in B) \to N (X) \in B$
17	8 9 16	syl2anc	$⊢ (W \in LMod \land R \in K \land X \in B) \to N (X) \in B$
18	1 10 2 3 5	lmodvsdi	$⊢ (W \in LMod \land (R \in K \land X \in B \land N (X) \in B)) \to R \underset{˙}{\cdot} (X +_{W} N (X)) = (R \underset{˙}{\cdot} X) +_{W} (R \underset{˙}{\cdot} N (X))$
19	6 15 9 17 18	syl13anc	$⊢ (W \in LMod \land R \in K \land X \in B) \to R \underset{˙}{\cdot} (X +_{W} N (X)) = (R \underset{˙}{\cdot} X) +_{W} (R \underset{˙}{\cdot} N (X))$
20	2 3 5 11	lmodvs0	$⊢ (W \in LMod \land R \in K) \to R \underset{˙}{\cdot} 0_{W} = 0_{W}$
21	6 15 20	syl2anc	$⊢ (W \in LMod \land R \in K \land X \in B) \to R \underset{˙}{\cdot} 0_{W} = 0_{W}$
22	14 19 21	3eqtr3d	$⊢ (W \in LMod \land R \in K \land X \in B) \to (R \underset{˙}{\cdot} X) +_{W} (R \underset{˙}{\cdot} N (X)) = 0_{W}$
23	1 2 3 5	lmodvscl	$⊢ (W \in LMod \land R \in K \land X \in B) \to R \underset{˙}{\cdot} X \in B$
24	1 2 3 5	lmodvscl	$⊢ (W \in LMod \land R \in K \land N (X) \in B) \to R \underset{˙}{\cdot} N (X) \in B$
25	6 15 17 24	syl3anc	$⊢ (W \in LMod \land R \in K \land X \in B) \to R \underset{˙}{\cdot} N (X) \in B$
26	1 10 11 4	grpinvid1	$⊢ (W \in Grp \land R \underset{˙}{\cdot} X \in B \land R \underset{˙}{\cdot} N (X) \in B) \to (N (R \underset{˙}{\cdot} X) = R \underset{˙}{\cdot} N (X) \leftrightarrow (R \underset{˙}{\cdot} X) +_{W} (R \underset{˙}{\cdot} N (X)) = 0_{W})$
27	8 23 25 26	syl3anc	$⊢ (W \in LMod \land R \in K \land X \in B) \to (N (R \underset{˙}{\cdot} X) = R \underset{˙}{\cdot} N (X) \leftrightarrow (R \underset{˙}{\cdot} X) +_{W} (R \underset{˙}{\cdot} N (X)) = 0_{W})$
28	22 27	mpbird	$⊢ (W \in LMod \land R \in K \land X \in B) \to N (R \underset{˙}{\cdot} X) = R \underset{˙}{\cdot} N (X)$
29	28	eqcomd	$⊢ (W \in LMod \land R \in K \land X \in B) \to R \underset{˙}{\cdot} N (X) = N (R \underset{˙}{\cdot} X)$

Metamath Proof Explorer

Theorem lmodvsinv2

Proof