lmod1lem2

		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	lmod1lem2	$⊢ (I \in V \land R \in Ring \land r \in {Base}_{R}) \to r \cdot_{M} (I +_{M} I) = (r \cdot_{M} I) +_{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		mpoexga	$⊢ ({Base}_{R} \in V \land \{I\} \in V) \to (x \in {Base}_{R}, y \in \{I\} ⟼ y) \in V$
6	4 5	mp1i	$⊢ (I \in V \land R \in Ring \land r \in {Base}_{R}) \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	6 7	syl	$⊢ (I \in V \land R \in Ring \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 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 r \in {Base}_{R}) \land (x = r \land y = I)) \to y = I$
11		simp3	$⊢ (I \in V \land R \in Ring \land r \in {Base}_{R}) \to r \in {Base}_{R}$
12		snidg	$⊢ I \in V \to I \in \{I\}$
13	12	3ad2ant1	$⊢ (I \in V \land R \in Ring \land r \in {Base}_{R}) \to I \in \{I\}$
14	9 10 11 13 13	ovmpod	$⊢ (I \in V \land R \in Ring \land r \in {Base}_{R}) \to r \cdot_{M} I = I$
15		snex	$⊢ \{⟨⟨I, I⟩, I⟩\} \in V$
16	1	lmodplusg	$⊢ \{⟨⟨I, I⟩, I⟩\} \in V \to \{⟨⟨I, I⟩, I⟩\} = +_{M}$
17	15 16	mp1i	$⊢ (I \in V \land R \in Ring \land r \in {Base}_{R}) \to \{⟨⟨I, I⟩, I⟩\} = +_{M}$
18	17	eqcomd	$⊢ (I \in V \land R \in Ring \land r \in {Base}_{R}) \to +_{M} = \{⟨⟨I, I⟩, I⟩\}$
19	18	oveqd	$⊢ (I \in V \land R \in Ring \land r \in {Base}_{R}) \to I +_{M} I = I \{⟨⟨I, I⟩, I⟩\} I$
20		df-ov	$⊢ I \{⟨⟨I, I⟩, I⟩\} I = \{⟨⟨I, I⟩, I⟩\} (⟨I, I⟩)$
21		opex	$⊢ ⟨I, I⟩ \in V$
22		simp1	$⊢ (I \in V \land R \in Ring \land r \in {Base}_{R}) \to I \in V$
23		fvsng	$⊢ (⟨I, I⟩ \in V \land I \in V) \to \{⟨⟨I, I⟩, I⟩\} (⟨I, I⟩) = I$
24	21 22 23	sylancr	$⊢ (I \in V \land R \in Ring \land r \in {Base}_{R}) \to \{⟨⟨I, I⟩, I⟩\} (⟨I, I⟩) = I$
25	20 24	syl5eq	$⊢ (I \in V \land R \in Ring \land r \in {Base}_{R}) \to I \{⟨⟨I, I⟩, I⟩\} I = I$
26	19 25	eqtrd	$⊢ (I \in V \land R \in Ring \land r \in {Base}_{R}) \to I +_{M} I = I$
27	26	oveq2d	$⊢ (I \in V \land R \in Ring \land r \in {Base}_{R}) \to r \cdot_{M} (I +_{M} I) = r \cdot_{M} I$
28	3	a1i	$⊢ (I \in V \land R \in Ring \land r \in {Base}_{R}) \to \{I\} \in V$
29	2 28 5	sylancr	$⊢ (I \in V \land R \in Ring \land r \in {Base}_{R}) \to (x \in {Base}_{R}, y \in \{I\} ⟼ y) \in V$
30	29 7	syl	$⊢ (I \in V \land R \in Ring \land r \in {Base}_{R}) \to (x \in {Base}_{R}, y \in \{I\} ⟼ y) = \cdot_{M}$
31	30	eqcomd	$⊢ (I \in V \land R \in Ring \land r \in {Base}_{R}) \to \cdot_{M} = (x \in {Base}_{R}, y \in \{I\} ⟼ y)$
32	31 10 11 13 13	ovmpod	$⊢ (I \in V \land R \in Ring \land r \in {Base}_{R}) \to r \cdot_{M} I = I$
33	32 32	oveq12d	$⊢ (I \in V \land R \in Ring \land r \in {Base}_{R}) \to (r \cdot_{M} I) +_{M} (r \cdot_{M} I) = I +_{M} I$
34	33 26	eqtrd	$⊢ (I \in V \land R \in Ring \land r \in {Base}_{R}) \to (r \cdot_{M} I) +_{M} (r \cdot_{M} I) = I$
35	14 27 34	3eqtr4d	$⊢ (I \in V \land R \in Ring \land r \in {Base}_{R}) \to r \cdot_{M} (I +_{M} I) = (r \cdot_{M} I) +_{M} (r \cdot_{M} I)$

Metamath Proof Explorer

Theorem lmod1lem2

Proof