lmod1lem3

		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	lmod1lem3	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to (q +_{Scalar (M)} r) \cdot_{M} I = (q \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		eqidd	$⊢ ((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) = (x \in {Base}_{R}, y \in \{I\} ⟼ y)$
3		simprr	$⊢ (((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \land (x = q +_{Scalar (M)} r \land y = I)) \to y = I$
4		simplr	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to R \in Ring$
5	1	lmodsca	$⊢ R \in Ring \to R = Scalar (M)$
6	5	fveq2d	$⊢ R \in Ring \to +_{R} = +_{Scalar (M)}$
7	4 6	syl	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to +_{R} = +_{Scalar (M)}$
8	7	eqcomd	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to +_{Scalar (M)} = +_{R}$
9	8	oveqd	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to q +_{Scalar (M)} r = q +_{R} r$
10		simprl	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to q \in {Base}_{R}$
11		simprr	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to r \in {Base}_{R}$
12		eqid	$⊢ {Base}_{R} = {Base}_{R}$
13		eqid	$⊢ +_{R} = +_{R}$
14	12 13	ringacl	$⊢ (R \in Ring \land q \in {Base}_{R} \land r \in {Base}_{R}) \to q +_{R} r \in {Base}_{R}$
15	4 10 11 14	syl3anc	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to q +_{R} r \in {Base}_{R}$
16	9 15	eqeltrd	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to q +_{Scalar (M)} r \in {Base}_{R}$
17		snidg	$⊢ I \in V \to I \in \{I\}$
18	17	adantr	$⊢ (I \in V \land R \in Ring) \to I \in \{I\}$
19	18	adantr	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to I \in \{I\}$
20		simpl	$⊢ (I \in V \land R \in Ring) \to I \in V$
21	20	adantr	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to I \in V$
22	2 3 16 19 21	ovmpod	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to (q +_{Scalar (M)} r) (x \in {Base}_{R}, y \in \{I\} ⟼ y) I = I$
23		fvex	$⊢ {Base}_{R} \in V$
24		snex	$⊢ \{I\} \in V$
25	23 24	pm3.2i	$⊢ ({Base}_{R} \in V \land \{I\} \in V)$
26		mpoexga	$⊢ ({Base}_{R} \in V \land \{I\} \in V) \to (x \in {Base}_{R}, y \in \{I\} ⟼ y) \in V$
27	25 26	mp1i	$⊢ ((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) \in V$
28	1	lmodvsca	$⊢ (x \in {Base}_{R}, y \in \{I\} ⟼ y) \in V \to (x \in {Base}_{R}, y \in \{I\} ⟼ y) = \cdot_{M}$
29	27 28	syl	$⊢ ((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}$
30	29	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)$
31	30	oveqd	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to (q +_{Scalar (M)} r) \cdot_{M} I = (q +_{Scalar (M)} r) (x \in {Base}_{R}, y \in \{I\} ⟼ y) I$
32		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$
33	30 32 10 19 19	ovmpod	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to q \cdot_{M} I = I$
34		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$
35	30 34 11 19 19	ovmpod	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to r \cdot_{M} I = I$
36	33 35	oveq12d	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to (q \cdot_{M} I) +_{M} (r \cdot_{M} I) = I +_{M} I$
37		snex	$⊢ \{⟨⟨I, I⟩, I⟩\} \in V$
38	1	lmodplusg	$⊢ \{⟨⟨I, I⟩, I⟩\} \in V \to \{⟨⟨I, I⟩, I⟩\} = +_{M}$
39	37 38	mp1i	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to \{⟨⟨I, I⟩, I⟩\} = +_{M}$
40	39	eqcomd	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to +_{M} = \{⟨⟨I, I⟩, I⟩\}$
41	40	oveqd	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to I +_{M} I = I \{⟨⟨I, I⟩, I⟩\} I$
42		df-ov	$⊢ I \{⟨⟨I, I⟩, I⟩\} I = \{⟨⟨I, I⟩, I⟩\} (⟨I, I⟩)$
43		opex	$⊢ ⟨I, I⟩ \in V$
44	20 43	jctil	$⊢ (I \in V \land R \in Ring) \to (⟨I, I⟩ \in V \land I \in V)$
45	44	adantr	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to (⟨I, I⟩ \in V \land I \in V)$
46		fvsng	$⊢ (⟨I, I⟩ \in V \land I \in V) \to \{⟨⟨I, I⟩, I⟩\} (⟨I, I⟩) = I$
47	45 46	syl	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to \{⟨⟨I, I⟩, I⟩\} (⟨I, I⟩) = I$
48	42 47	syl5eq	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to I \{⟨⟨I, I⟩, I⟩\} I = I$
49	36 41 48	3eqtrd	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to (q \cdot_{M} I) +_{M} (r \cdot_{M} I) = I$
50	22 31 49	3eqtr4d	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to (q +_{Scalar (M)} r) \cdot_{M} I = (q \cdot_{M} I) +_{M} (r \cdot_{M} I)$

Metamath Proof Explorer

Theorem lmod1lem3

Proof