lmodvsinv

Description: Multiplication of a vector by a negated scalar. (Contributed by Stefan O'Rear, 28-Feb-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lmodvsinv.b	$⊢ B = {Base}_{W}$
2		lmodvsinv.f	$⊢ F = Scalar (W)$
3		lmodvsinv.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
4		lmodvsinv.n	$⊢ N = {inv}_{g} (W)$
5		lmodvsinv.m	$⊢ M = {inv}_{g} (F)$
6		lmodvsinv.k	$⊢ K = {Base}_{F}$
7		simp1	$⊢ (W \in LMod \land R \in K \land X \in B) \to W \in LMod$
8	2	lmodring	$⊢ W \in LMod \to F \in Ring$
9	8	3ad2ant1	$⊢ (W \in LMod \land R \in K \land X \in B) \to F \in Ring$
10		ringgrp	$⊢ F \in Ring \to F \in Grp$
11	9 10	syl	$⊢ (W \in LMod \land R \in K \land X \in B) \to F \in Grp$
12		eqid	$⊢ 1_{F} = 1_{F}$
13	6 12	ringidcl	$⊢ F \in Ring \to 1_{F} \in K$
14	9 13	syl	$⊢ (W \in LMod \land R \in K \land X \in B) \to 1_{F} \in K$
15	6 5	grpinvcl	$⊢ (F \in Grp \land 1_{F} \in K) \to M (1_{F}) \in K$
16	11 14 15	syl2anc	$⊢ (W \in LMod \land R \in K \land X \in B) \to M (1_{F}) \in K$
17		simp2	$⊢ (W \in LMod \land R \in K \land X \in B) \to R \in K$
18		simp3	$⊢ (W \in LMod \land R \in K \land X \in B) \to X \in B$
19		eqid	$⊢ \cdot_{F} = \cdot_{F}$
20	1 2 3 6 19	lmodvsass	$⊢ (W \in LMod \land (M (1_{F}) \in K \land R \in K \land X \in B)) \to (M (1_{F}) \cdot_{F} R) \underset{˙}{\cdot} X = M (1_{F}) \underset{˙}{\cdot} (R \underset{˙}{\cdot} X)$
21	7 16 17 18 20	syl13anc	$⊢ (W \in LMod \land R \in K \land X \in B) \to (M (1_{F}) \cdot_{F} R) \underset{˙}{\cdot} X = M (1_{F}) \underset{˙}{\cdot} (R \underset{˙}{\cdot} X)$
22	6 19 12 5 9 17	ringnegl	$⊢ (W \in LMod \land R \in K \land X \in B) \to M (1_{F}) \cdot_{F} R = M (R)$
23	22	oveq1d	$⊢ (W \in LMod \land R \in K \land X \in B) \to (M (1_{F}) \cdot_{F} R) \underset{˙}{\cdot} X = M (R) \underset{˙}{\cdot} X$
24	1 2 3 6	lmodvscl	$⊢ (W \in LMod \land R \in K \land X \in B) \to R \underset{˙}{\cdot} X \in B$
25	1 4 2 3 12 5	lmodvneg1	$⊢ (W \in LMod \land R \underset{˙}{\cdot} X \in B) \to M (1_{F}) \underset{˙}{\cdot} (R \underset{˙}{\cdot} X) = N (R \underset{˙}{\cdot} X)$
26	7 24 25	syl2anc	$⊢ (W \in LMod \land R \in K \land X \in B) \to M (1_{F}) \underset{˙}{\cdot} (R \underset{˙}{\cdot} X) = N (R \underset{˙}{\cdot} X)$
27	21 23 26	3eqtr3d	$⊢ (W \in LMod \land R \in K \land X \in B) \to M (R) \underset{˙}{\cdot} X = N (R \underset{˙}{\cdot} X)$

Metamath Proof Explorer

Theorem lmodvsinv

Proof