lmod1lem4

		Ref	Expression
	Hypothesis	lmod1.m	$⊢ M = \{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩, ⟨Scalar (ndx), R⟩\} \cup \{⟨\cdot_{ndx}, (x \in {Base}_{R}, y \in \{I\} ⟼ y)⟩\}$
	Assertion	lmod1lem4	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to (q \cdot_{Scalar (M)} r) \cdot_{M} I = q \cdot_{M} (r \cdot_{M} I)$

Proof

Step	Hyp	Ref	Expression
1		lmod1.m	$⊢ M = \{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩, ⟨Scalar (ndx), R⟩\} \cup \{⟨\cdot_{ndx}, (x \in {Base}_{R}, y \in \{I\} ⟼ y)⟩\}$
2		fvex	$⊢ {Base}_{R} \in V$
3		snex	$⊢ \{I\} \in V$
4	2 3	pm3.2i	$⊢ ({Base}_{R} \in V \land \{I\} \in V)$
5	4	a1i	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to ({Base}_{R} \in V \land \{I\} \in V)$
6		mpoexga	$⊢ ({Base}_{R} \in V \land \{I\} \in V) \to (x \in {Base}_{R}, y \in \{I\} ⟼ y) \in V$
7	1	lmodvsca	$⊢ (x \in {Base}_{R}, y \in \{I\} ⟼ y) \in V \to (x \in {Base}_{R}, y \in \{I\} ⟼ y) = \cdot_{M}$
8	5 6 7	3syl	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to (x \in {Base}_{R}, y \in \{I\} ⟼ y) = \cdot_{M}$
9	8	eqcomd	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to \cdot_{M} = (x \in {Base}_{R}, y \in \{I\} ⟼ y)$
10		simprr	$⊢ (((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \land (x = q \land y = I)) \to y = I$
11		simprl	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to q \in {Base}_{R}$
12		snidg	$⊢ I \in V \to I \in \{I\}$
13	12	ad2antrr	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to I \in \{I\}$
14	9 10 11 13 13	ovmpod	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to q \cdot_{M} I = I$
15		simprr	$⊢ (((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \land (x = r \land y = I)) \to y = I$
16		simprr	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to r \in {Base}_{R}$
17	9 15 16 13 13	ovmpod	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to r \cdot_{M} I = I$
18	17	oveq2d	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to q \cdot_{M} (r \cdot_{M} I) = q \cdot_{M} I$
19		simprr	$⊢ (((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \land (x = q \cdot_{Scalar (M)} r \land y = I)) \to y = I$
20		simplr	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to R \in Ring$
21	1	lmodsca	$⊢ R \in Ring \to R = Scalar (M)$
22	21	fveq2d	$⊢ R \in Ring \to \cdot_{R} = \cdot_{Scalar (M)}$
23	20 22	syl	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to \cdot_{R} = \cdot_{Scalar (M)}$
24	23	eqcomd	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to \cdot_{Scalar (M)} = \cdot_{R}$
25	24	oveqd	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to q \cdot_{Scalar (M)} r = q \cdot_{R} r$
26		eqid	$⊢ {Base}_{R} = {Base}_{R}$
27		eqid	$⊢ \cdot_{R} = \cdot_{R}$
28	26 27	ringcl	$⊢ (R \in Ring \land q \in {Base}_{R} \land r \in {Base}_{R}) \to q \cdot_{R} r \in {Base}_{R}$
29	20 11 16 28	syl3anc	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to q \cdot_{R} r \in {Base}_{R}$
30	25 29	eqeltrd	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to q \cdot_{Scalar (M)} r \in {Base}_{R}$
31	9 19 30 13 13	ovmpod	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to (q \cdot_{Scalar (M)} r) \cdot_{M} I = I$
32	14 18 31	3eqtr4rd	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to (q \cdot_{Scalar (M)} r) \cdot_{M} I = q \cdot_{M} (r \cdot_{M} I)$

Metamath Proof Explorer

Theorem lmod1lem4

Proof