lmodvsneg

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

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

Proof

Step	Hyp	Ref	Expression
1		lmodvsneg.b	$⊢ B = {Base}_{W}$
2		lmodvsneg.f	$⊢ F = Scalar (W)$
3		lmodvsneg.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
4		lmodvsneg.n	$⊢ N = {inv}_{g} (W)$
5		lmodvsneg.k	$⊢ K = {Base}_{F}$
6		lmodvsneg.m	$⊢ M = {inv}_{g} (F)$
7		lmodvsneg.w	$⊢ φ \to W \in LMod$
8		lmodvsneg.x	$⊢ φ \to X \in B$
9		lmodvsneg.r	$⊢ φ \to R \in K$
10	2	lmodring	$⊢ W \in LMod \to F \in Ring$
11	7 10	syl	$⊢ φ \to F \in Ring$
12		ringgrp	$⊢ F \in Ring \to F \in Grp$
13	11 12	syl	$⊢ φ \to F \in Grp$
14		eqid	$⊢ 1_{F} = 1_{F}$
15	5 14	ringidcl	$⊢ F \in Ring \to 1_{F} \in K$
16	11 15	syl	$⊢ φ \to 1_{F} \in K$
17	5 6	grpinvcl	$⊢ (F \in Grp \land 1_{F} \in K) \to M (1_{F}) \in K$
18	13 16 17	syl2anc	$⊢ φ \to M (1_{F}) \in K$
19		eqid	$⊢ \cdot_{F} = \cdot_{F}$
20	1 2 3 5 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 18 9 8 20	syl13anc	$⊢ φ \to (M (1_{F}) \cdot_{F} R) \underset{˙}{\cdot} X = M (1_{F}) \underset{˙}{\cdot} (R \underset{˙}{\cdot} X)$
22	5 19 14 6 11 9	ringnegl	$⊢ φ \to M (1_{F}) \cdot_{F} R = M (R)$
23	22	oveq1d	$⊢ φ \to (M (1_{F}) \cdot_{F} R) \underset{˙}{\cdot} X = M (R) \underset{˙}{\cdot} X$
24	1 2 3 5	lmodvscl	$⊢ (W \in LMod \land R \in K \land X \in B) \to R \underset{˙}{\cdot} X \in B$
25	7 9 8 24	syl3anc	$⊢ φ \to R \underset{˙}{\cdot} X \in B$
26	1 4 2 3 14 6	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)$
27	7 25 26	syl2anc	$⊢ φ \to M (1_{F}) \underset{˙}{\cdot} (R \underset{˙}{\cdot} X) = N (R \underset{˙}{\cdot} X)$
28	21 23 27	3eqtr3rd	$⊢ φ \to N (R \underset{˙}{\cdot} X) = M (R) \underset{˙}{\cdot} X$

Metamath Proof Explorer

Theorem lmodvsneg

Proof