lmod1

Description: The (smallest) structure representing azero module over an arbitrary ring. (Contributed by AV, 29-Apr-2019)

		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	lmod1	$⊢ (I \in V \land R \in Ring) \to M \in LMod$

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		eqid	$⊢ \{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\} = \{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\}$
3	2	grp1	$⊢ I \in V \to \{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\} \in Grp$
4		fvex	$⊢ {Base}_{\{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\}} \in V$
5		snex	$⊢ \{I\} \in V$
6	2	grpbase	$⊢ \{I\} \in V \to \{I\} = {Base}_{\{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\}}$
7	5 6	ax-mp	$⊢ \{I\} = {Base}_{\{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\}}$
8	7	opeq2i	$⊢ ⟨{Base}_{ndx}, \{I\}⟩ = ⟨{Base}_{ndx}, {Base}_{\{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\}}⟩$
9		tpeq1	$⊢ ⟨{Base}_{ndx}, \{I\}⟩ = ⟨{Base}_{ndx}, {Base}_{\{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\}}⟩ \to \{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩, ⟨Scalar (ndx), R⟩\} = \{⟨{Base}_{ndx}, {Base}_{\{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\}}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩, ⟨Scalar (ndx), R⟩\}$
10	8 9	ax-mp	$⊢ \{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩, ⟨Scalar (ndx), R⟩\} = \{⟨{Base}_{ndx}, {Base}_{\{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\}}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩, ⟨Scalar (ndx), R⟩\}$
11	10	uneq1i	$⊢ \{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩, ⟨Scalar (ndx), R⟩\} \cup \{⟨\cdot_{ndx}, (x \in {Base}_{R}, y \in \{I\} ⟼ y)⟩\} = \{⟨{Base}_{ndx}, {Base}_{\{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\}}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩, ⟨Scalar (ndx), R⟩\} \cup \{⟨\cdot_{ndx}, (x \in {Base}_{R}, y \in \{I\} ⟼ y)⟩\}$
12	1 11	eqtri	$⊢ M = \{⟨{Base}_{ndx}, {Base}_{\{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\}}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩, ⟨Scalar (ndx), R⟩\} \cup \{⟨\cdot_{ndx}, (x \in {Base}_{R}, y \in \{I\} ⟼ y)⟩\}$
13	12	lmodbase	$⊢ {Base}_{\{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\}} \in V \to {Base}_{\{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\}} = {Base}_{M}$
14	4 13	ax-mp	$⊢ {Base}_{\{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\}} = {Base}_{M}$
15	14	eqcomi	$⊢ {Base}_{M} = {Base}_{\{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\}}$
16		fvex	$⊢ +_{\{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\}} \in V$
17		snex	$⊢ \{⟨⟨I, I⟩, I⟩\} \in V$
18	2	grpplusg	$⊢ \{⟨⟨I, I⟩, I⟩\} \in V \to \{⟨⟨I, I⟩, I⟩\} = +_{\{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\}}$
19	17 18	ax-mp	$⊢ \{⟨⟨I, I⟩, I⟩\} = +_{\{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\}}$
20	19	opeq2i	$⊢ ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩ = ⟨+_{ndx}, +_{\{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\}}⟩$
21		tpeq2	$⊢ ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩ = ⟨+_{ndx}, +_{\{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\}}⟩ \to \{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩, ⟨Scalar (ndx), R⟩\} = \{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, +_{\{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\}}⟩, ⟨Scalar (ndx), R⟩\}$
22	20 21	ax-mp	$⊢ \{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩, ⟨Scalar (ndx), R⟩\} = \{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, +_{\{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\}}⟩, ⟨Scalar (ndx), R⟩\}$
23	22	uneq1i	$⊢ \{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩, ⟨Scalar (ndx), R⟩\} \cup \{⟨\cdot_{ndx}, (x \in {Base}_{R}, y \in \{I\} ⟼ y)⟩\} = \{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, +_{\{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\}}⟩, ⟨Scalar (ndx), R⟩\} \cup \{⟨\cdot_{ndx}, (x \in {Base}_{R}, y \in \{I\} ⟼ y)⟩\}$
24	1 23	eqtri	$⊢ M = \{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, +_{\{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\}}⟩, ⟨Scalar (ndx), R⟩\} \cup \{⟨\cdot_{ndx}, (x \in {Base}_{R}, y \in \{I\} ⟼ y)⟩\}$
25	24	lmodplusg	$⊢ +_{\{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\}} \in V \to +_{\{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\}} = +_{M}$
26	16 25	ax-mp	$⊢ +_{\{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\}} = +_{M}$
27	26	eqcomi	$⊢ +_{M} = +_{\{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\}}$
28	15 27	grpprop	$⊢ M \in Grp \leftrightarrow \{⟨{Base}_{ndx}, \{I\}⟩, ⟨+_{ndx}, \{⟨⟨I, I⟩, I⟩\}⟩\} \in Grp$
29	3 28	sylibr	$⊢ I \in V \to M \in Grp$
30	29	adantr	$⊢ (I \in V \land R \in Ring) \to M \in Grp$
31	1	lmodsca	$⊢ R \in Ring \to R = Scalar (M)$
32	31	eqcomd	$⊢ R \in Ring \to Scalar (M) = R$
33	32	adantl	$⊢ (I \in V \land R \in Ring) \to Scalar (M) = R$
34		simpr	$⊢ (I \in V \land R \in Ring) \to R \in Ring$
35	33 34	eqeltrd	$⊢ (I \in V \land R \in Ring) \to Scalar (M) \in Ring$
36	33	fveq2d	$⊢ (I \in V \land R \in Ring) \to {Base}_{Scalar (M)} = {Base}_{R}$
37	36	eleq2d	$⊢ (I \in V \land R \in Ring) \to (q \in {Base}_{Scalar (M)} \leftrightarrow q \in {Base}_{R})$
38	36	eleq2d	$⊢ (I \in V \land R \in Ring) \to (r \in {Base}_{Scalar (M)} \leftrightarrow r \in {Base}_{R})$
39	37 38	anbi12d	$⊢ (I \in V \land R \in Ring) \to ((q \in {Base}_{Scalar (M)} \land r \in {Base}_{Scalar (M)}) \leftrightarrow (q \in {Base}_{R} \land r \in {Base}_{R}))$
40		simpll	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to I \in V$
41		simplr	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to R \in Ring$
42		simprr	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to r \in {Base}_{R}$
43	40 41 42	3jca	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to (I \in V \land R \in Ring \land r \in {Base}_{R})$
44	1	lmod1lem1	$⊢ (I \in V \land R \in Ring \land r \in {Base}_{R}) \to r \cdot_{M} I \in \{I\}$
45	43 44	syl	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to r \cdot_{M} I \in \{I\}$
46	1	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)$
47	43 46	syl	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to r \cdot_{M} (I +_{M} I) = (r \cdot_{M} I) +_{M} (r \cdot_{M} I)$
48	1	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)$
49	45 47 48	3jca	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to (r \cdot_{M} I \in \{I\} \land r \cdot_{M} (I +_{M} I) = (r \cdot_{M} I) +_{M} (r \cdot_{M} I) \land (q +_{Scalar (M)} r) \cdot_{M} I = (q \cdot_{M} I) +_{M} (r \cdot_{M} I))$
50	1	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)$
51	1	lmod1lem5	$⊢ (I \in V \land R \in Ring) \to 1_{Scalar (M)} \cdot_{M} I = I$
52	51	adantr	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to 1_{Scalar (M)} \cdot_{M} I = I$
53	49 50 52	jca32	$⊢ ((I \in V \land R \in Ring) \land (q \in {Base}_{R} \land r \in {Base}_{R})) \to ((r \cdot_{M} I \in \{I\} \land r \cdot_{M} (I +_{M} I) = (r \cdot_{M} I) +_{M} (r \cdot_{M} I) \land (q +_{Scalar (M)} r) \cdot_{M} I = (q \cdot_{M} I) +_{M} (r \cdot_{M} I)) \land ((q \cdot_{Scalar (M)} r) \cdot_{M} I = q \cdot_{M} (r \cdot_{M} I) \land 1_{Scalar (M)} \cdot_{M} I = I))$
54	53	ex	$⊢ (I \in V \land R \in Ring) \to ((q \in {Base}_{R} \land r \in {Base}_{R}) \to ((r \cdot_{M} I \in \{I\} \land r \cdot_{M} (I +_{M} I) = (r \cdot_{M} I) +_{M} (r \cdot_{M} I) \land (q +_{Scalar (M)} r) \cdot_{M} I = (q \cdot_{M} I) +_{M} (r \cdot_{M} I)) \land ((q \cdot_{Scalar (M)} r) \cdot_{M} I = q \cdot_{M} (r \cdot_{M} I) \land 1_{Scalar (M)} \cdot_{M} I = I)))$
55	39 54	sylbid	$⊢ (I \in V \land R \in Ring) \to ((q \in {Base}_{Scalar (M)} \land r \in {Base}_{Scalar (M)}) \to ((r \cdot_{M} I \in \{I\} \land r \cdot_{M} (I +_{M} I) = (r \cdot_{M} I) +_{M} (r \cdot_{M} I) \land (q +_{Scalar (M)} r) \cdot_{M} I = (q \cdot_{M} I) +_{M} (r \cdot_{M} I)) \land ((q \cdot_{Scalar (M)} r) \cdot_{M} I = q \cdot_{M} (r \cdot_{M} I) \land 1_{Scalar (M)} \cdot_{M} I = I)))$
56	55	ralrimivv	$⊢ (I \in V \land R \in Ring) \to \forall q \in {Base}_{Scalar (M)} \forall r \in {Base}_{Scalar (M)} ((r \cdot_{M} I \in \{I\} \land r \cdot_{M} (I +_{M} I) = (r \cdot_{M} I) +_{M} (r \cdot_{M} I) \land (q +_{Scalar (M)} r) \cdot_{M} I = (q \cdot_{M} I) +_{M} (r \cdot_{M} I)) \land ((q \cdot_{Scalar (M)} r) \cdot_{M} I = q \cdot_{M} (r \cdot_{M} I) \land 1_{Scalar (M)} \cdot_{M} I = I))$
57		oveq2	$⊢ x = I \to w +_{M} x = w +_{M} I$
58	57	oveq2d	$⊢ x = I \to r \cdot_{M} (w +_{M} x) = r \cdot_{M} (w +_{M} I)$
59		oveq2	$⊢ x = I \to r \cdot_{M} x = r \cdot_{M} I$
60	59	oveq2d	$⊢ x = I \to (r \cdot_{M} w) +_{M} (r \cdot_{M} x) = (r \cdot_{M} w) +_{M} (r \cdot_{M} I)$
61	58 60	eqeq12d	$⊢ x = I \to (r \cdot_{M} (w +_{M} x) = (r \cdot_{M} w) +_{M} (r \cdot_{M} x) \leftrightarrow r \cdot_{M} (w +_{M} I) = (r \cdot_{M} w) +_{M} (r \cdot_{M} I))$
62	61	3anbi2d	$⊢ x = I \to ((r \cdot_{M} w \in \{I\} \land r \cdot_{M} (w +_{M} x) = (r \cdot_{M} w) +_{M} (r \cdot_{M} x) \land (q +_{Scalar (M)} r) \cdot_{M} w = (q \cdot_{M} w) +_{M} (r \cdot_{M} w)) \leftrightarrow (r \cdot_{M} w \in \{I\} \land r \cdot_{M} (w +_{M} I) = (r \cdot_{M} w) +_{M} (r \cdot_{M} I) \land (q +_{Scalar (M)} r) \cdot_{M} w = (q \cdot_{M} w) +_{M} (r \cdot_{M} w)))$
63	62	anbi1d	$⊢ x = I \to (((r \cdot_{M} w \in \{I\} \land r \cdot_{M} (w +_{M} x) = (r \cdot_{M} w) +_{M} (r \cdot_{M} x) \land (q +_{Scalar (M)} r) \cdot_{M} w = (q \cdot_{M} w) +_{M} (r \cdot_{M} w)) \land ((q \cdot_{Scalar (M)} r) \cdot_{M} w = q \cdot_{M} (r \cdot_{M} w) \land 1_{Scalar (M)} \cdot_{M} w = w)) \leftrightarrow ((r \cdot_{M} w \in \{I\} \land r \cdot_{M} (w +_{M} I) = (r \cdot_{M} w) +_{M} (r \cdot_{M} I) \land (q +_{Scalar (M)} r) \cdot_{M} w = (q \cdot_{M} w) +_{M} (r \cdot_{M} w)) \land ((q \cdot_{Scalar (M)} r) \cdot_{M} w = q \cdot_{M} (r \cdot_{M} w) \land 1_{Scalar (M)} \cdot_{M} w = w)))$
64	63	ralbidv	$⊢ x = I \to (\forall w \in \{I\} ((r \cdot_{M} w \in \{I\} \land r \cdot_{M} (w +_{M} x) = (r \cdot_{M} w) +_{M} (r \cdot_{M} x) \land (q +_{Scalar (M)} r) \cdot_{M} w = (q \cdot_{M} w) +_{M} (r \cdot_{M} w)) \land ((q \cdot_{Scalar (M)} r) \cdot_{M} w = q \cdot_{M} (r \cdot_{M} w) \land 1_{Scalar (M)} \cdot_{M} w = w)) \leftrightarrow \forall w \in \{I\} ((r \cdot_{M} w \in \{I\} \land r \cdot_{M} (w +_{M} I) = (r \cdot_{M} w) +_{M} (r \cdot_{M} I) \land (q +_{Scalar (M)} r) \cdot_{M} w = (q \cdot_{M} w) +_{M} (r \cdot_{M} w)) \land ((q \cdot_{Scalar (M)} r) \cdot_{M} w = q \cdot_{M} (r \cdot_{M} w) \land 1_{Scalar (M)} \cdot_{M} w = w)))$
65	64	ralsng	$⊢ I \in V \to (\forall x \in \{I\} \forall w \in \{I\} ((r \cdot_{M} w \in \{I\} \land r \cdot_{M} (w +_{M} x) = (r \cdot_{M} w) +_{M} (r \cdot_{M} x) \land (q +_{Scalar (M)} r) \cdot_{M} w = (q \cdot_{M} w) +_{M} (r \cdot_{M} w)) \land ((q \cdot_{Scalar (M)} r) \cdot_{M} w = q \cdot_{M} (r \cdot_{M} w) \land 1_{Scalar (M)} \cdot_{M} w = w)) \leftrightarrow \forall w \in \{I\} ((r \cdot_{M} w \in \{I\} \land r \cdot_{M} (w +_{M} I) = (r \cdot_{M} w) +_{M} (r \cdot_{M} I) \land (q +_{Scalar (M)} r) \cdot_{M} w = (q \cdot_{M} w) +_{M} (r \cdot_{M} w)) \land ((q \cdot_{Scalar (M)} r) \cdot_{M} w = q \cdot_{M} (r \cdot_{M} w) \land 1_{Scalar (M)} \cdot_{M} w = w)))$
66	65	adantr	$⊢ (I \in V \land R \in Ring) \to (\forall x \in \{I\} \forall w \in \{I\} ((r \cdot_{M} w \in \{I\} \land r \cdot_{M} (w +_{M} x) = (r \cdot_{M} w) +_{M} (r \cdot_{M} x) \land (q +_{Scalar (M)} r) \cdot_{M} w = (q \cdot_{M} w) +_{M} (r \cdot_{M} w)) \land ((q \cdot_{Scalar (M)} r) \cdot_{M} w = q \cdot_{M} (r \cdot_{M} w) \land 1_{Scalar (M)} \cdot_{M} w = w)) \leftrightarrow \forall w \in \{I\} ((r \cdot_{M} w \in \{I\} \land r \cdot_{M} (w +_{M} I) = (r \cdot_{M} w) +_{M} (r \cdot_{M} I) \land (q +_{Scalar (M)} r) \cdot_{M} w = (q \cdot_{M} w) +_{M} (r \cdot_{M} w)) \land ((q \cdot_{Scalar (M)} r) \cdot_{M} w = q \cdot_{M} (r \cdot_{M} w) \land 1_{Scalar (M)} \cdot_{M} w = w)))$
67		oveq2	$⊢ w = I \to r \cdot_{M} w = r \cdot_{M} I$
68	67	eleq1d	$⊢ w = I \to (r \cdot_{M} w \in \{I\} \leftrightarrow r \cdot_{M} I \in \{I\})$
69		oveq1	$⊢ w = I \to w +_{M} I = I +_{M} I$
70	69	oveq2d	$⊢ w = I \to r \cdot_{M} (w +_{M} I) = r \cdot_{M} (I +_{M} I)$
71	67	oveq1d	$⊢ w = I \to (r \cdot_{M} w) +_{M} (r \cdot_{M} I) = (r \cdot_{M} I) +_{M} (r \cdot_{M} I)$
72	70 71	eqeq12d	$⊢ w = I \to (r \cdot_{M} (w +_{M} I) = (r \cdot_{M} w) +_{M} (r \cdot_{M} I) \leftrightarrow r \cdot_{M} (I +_{M} I) = (r \cdot_{M} I) +_{M} (r \cdot_{M} I))$
73		oveq2	$⊢ w = I \to (q +_{Scalar (M)} r) \cdot_{M} w = (q +_{Scalar (M)} r) \cdot_{M} I$
74		oveq2	$⊢ w = I \to q \cdot_{M} w = q \cdot_{M} I$
75	74 67	oveq12d	$⊢ w = I \to (q \cdot_{M} w) +_{M} (r \cdot_{M} w) = (q \cdot_{M} I) +_{M} (r \cdot_{M} I)$
76	73 75	eqeq12d	$⊢ w = I \to ((q +_{Scalar (M)} r) \cdot_{M} w = (q \cdot_{M} w) +_{M} (r \cdot_{M} w) \leftrightarrow (q +_{Scalar (M)} r) \cdot_{M} I = (q \cdot_{M} I) +_{M} (r \cdot_{M} I))$
77	68 72 76	3anbi123d	$⊢ w = I \to ((r \cdot_{M} w \in \{I\} \land r \cdot_{M} (w +_{M} I) = (r \cdot_{M} w) +_{M} (r \cdot_{M} I) \land (q +_{Scalar (M)} r) \cdot_{M} w = (q \cdot_{M} w) +_{M} (r \cdot_{M} w)) \leftrightarrow (r \cdot_{M} I \in \{I\} \land r \cdot_{M} (I +_{M} I) = (r \cdot_{M} I) +_{M} (r \cdot_{M} I) \land (q +_{Scalar (M)} r) \cdot_{M} I = (q \cdot_{M} I) +_{M} (r \cdot_{M} I)))$
78		oveq2	$⊢ w = I \to (q \cdot_{Scalar (M)} r) \cdot_{M} w = (q \cdot_{Scalar (M)} r) \cdot_{M} I$
79	67	oveq2d	$⊢ w = I \to q \cdot_{M} (r \cdot_{M} w) = q \cdot_{M} (r \cdot_{M} I)$
80	78 79	eqeq12d	$⊢ w = I \to ((q \cdot_{Scalar (M)} r) \cdot_{M} w = q \cdot_{M} (r \cdot_{M} w) \leftrightarrow (q \cdot_{Scalar (M)} r) \cdot_{M} I = q \cdot_{M} (r \cdot_{M} I))$
81		oveq2	$⊢ w = I \to 1_{Scalar (M)} \cdot_{M} w = 1_{Scalar (M)} \cdot_{M} I$
82		id	$⊢ w = I \to w = I$
83	81 82	eqeq12d	$⊢ w = I \to (1_{Scalar (M)} \cdot_{M} w = w \leftrightarrow 1_{Scalar (M)} \cdot_{M} I = I)$
84	80 83	anbi12d	$⊢ w = I \to (((q \cdot_{Scalar (M)} r) \cdot_{M} w = q \cdot_{M} (r \cdot_{M} w) \land 1_{Scalar (M)} \cdot_{M} w = w) \leftrightarrow ((q \cdot_{Scalar (M)} r) \cdot_{M} I = q \cdot_{M} (r \cdot_{M} I) \land 1_{Scalar (M)} \cdot_{M} I = I))$
85	77 84	anbi12d	$⊢ w = I \to (((r \cdot_{M} w \in \{I\} \land r \cdot_{M} (w +_{M} I) = (r \cdot_{M} w) +_{M} (r \cdot_{M} I) \land (q +_{Scalar (M)} r) \cdot_{M} w = (q \cdot_{M} w) +_{M} (r \cdot_{M} w)) \land ((q \cdot_{Scalar (M)} r) \cdot_{M} w = q \cdot_{M} (r \cdot_{M} w) \land 1_{Scalar (M)} \cdot_{M} w = w)) \leftrightarrow ((r \cdot_{M} I \in \{I\} \land r \cdot_{M} (I +_{M} I) = (r \cdot_{M} I) +_{M} (r \cdot_{M} I) \land (q +_{Scalar (M)} r) \cdot_{M} I = (q \cdot_{M} I) +_{M} (r \cdot_{M} I)) \land ((q \cdot_{Scalar (M)} r) \cdot_{M} I = q \cdot_{M} (r \cdot_{M} I) \land 1_{Scalar (M)} \cdot_{M} I = I)))$
86	85	ralsng	$⊢ I \in V \to (\forall w \in \{I\} ((r \cdot_{M} w \in \{I\} \land r \cdot_{M} (w +_{M} I) = (r \cdot_{M} w) +_{M} (r \cdot_{M} I) \land (q +_{Scalar (M)} r) \cdot_{M} w = (q \cdot_{M} w) +_{M} (r \cdot_{M} w)) \land ((q \cdot_{Scalar (M)} r) \cdot_{M} w = q \cdot_{M} (r \cdot_{M} w) \land 1_{Scalar (M)} \cdot_{M} w = w)) \leftrightarrow ((r \cdot_{M} I \in \{I\} \land r \cdot_{M} (I +_{M} I) = (r \cdot_{M} I) +_{M} (r \cdot_{M} I) \land (q +_{Scalar (M)} r) \cdot_{M} I = (q \cdot_{M} I) +_{M} (r \cdot_{M} I)) \land ((q \cdot_{Scalar (M)} r) \cdot_{M} I = q \cdot_{M} (r \cdot_{M} I) \land 1_{Scalar (M)} \cdot_{M} I = I)))$
87	86	adantr	$⊢ (I \in V \land R \in Ring) \to (\forall w \in \{I\} ((r \cdot_{M} w \in \{I\} \land r \cdot_{M} (w +_{M} I) = (r \cdot_{M} w) +_{M} (r \cdot_{M} I) \land (q +_{Scalar (M)} r) \cdot_{M} w = (q \cdot_{M} w) +_{M} (r \cdot_{M} w)) \land ((q \cdot_{Scalar (M)} r) \cdot_{M} w = q \cdot_{M} (r \cdot_{M} w) \land 1_{Scalar (M)} \cdot_{M} w = w)) \leftrightarrow ((r \cdot_{M} I \in \{I\} \land r \cdot_{M} (I +_{M} I) = (r \cdot_{M} I) +_{M} (r \cdot_{M} I) \land (q +_{Scalar (M)} r) \cdot_{M} I = (q \cdot_{M} I) +_{M} (r \cdot_{M} I)) \land ((q \cdot_{Scalar (M)} r) \cdot_{M} I = q \cdot_{M} (r \cdot_{M} I) \land 1_{Scalar (M)} \cdot_{M} I = I)))$
88	66 87	bitrd	$⊢ (I \in V \land R \in Ring) \to (\forall x \in \{I\} \forall w \in \{I\} ((r \cdot_{M} w \in \{I\} \land r \cdot_{M} (w +_{M} x) = (r \cdot_{M} w) +_{M} (r \cdot_{M} x) \land (q +_{Scalar (M)} r) \cdot_{M} w = (q \cdot_{M} w) +_{M} (r \cdot_{M} w)) \land ((q \cdot_{Scalar (M)} r) \cdot_{M} w = q \cdot_{M} (r \cdot_{M} w) \land 1_{Scalar (M)} \cdot_{M} w = w)) \leftrightarrow ((r \cdot_{M} I \in \{I\} \land r \cdot_{M} (I +_{M} I) = (r \cdot_{M} I) +_{M} (r \cdot_{M} I) \land (q +_{Scalar (M)} r) \cdot_{M} I = (q \cdot_{M} I) +_{M} (r \cdot_{M} I)) \land ((q \cdot_{Scalar (M)} r) \cdot_{M} I = q \cdot_{M} (r \cdot_{M} I) \land 1_{Scalar (M)} \cdot_{M} I = I)))$
89	88	2ralbidv	$⊢ (I \in V \land R \in Ring) \to (\forall q \in {Base}_{Scalar (M)} \forall r \in {Base}_{Scalar (M)} \forall x \in \{I\} \forall w \in \{I\} ((r \cdot_{M} w \in \{I\} \land r \cdot_{M} (w +_{M} x) = (r \cdot_{M} w) +_{M} (r \cdot_{M} x) \land (q +_{Scalar (M)} r) \cdot_{M} w = (q \cdot_{M} w) +_{M} (r \cdot_{M} w)) \land ((q \cdot_{Scalar (M)} r) \cdot_{M} w = q \cdot_{M} (r \cdot_{M} w) \land 1_{Scalar (M)} \cdot_{M} w = w)) \leftrightarrow \forall q \in {Base}_{Scalar (M)} \forall r \in {Base}_{Scalar (M)} ((r \cdot_{M} I \in \{I\} \land r \cdot_{M} (I +_{M} I) = (r \cdot_{M} I) +_{M} (r \cdot_{M} I) \land (q +_{Scalar (M)} r) \cdot_{M} I = (q \cdot_{M} I) +_{M} (r \cdot_{M} I)) \land ((q \cdot_{Scalar (M)} r) \cdot_{M} I = q \cdot_{M} (r \cdot_{M} I) \land 1_{Scalar (M)} \cdot_{M} I = I)))$
90	56 89	mpbird	$⊢ (I \in V \land R \in Ring) \to \forall q \in {Base}_{Scalar (M)} \forall r \in {Base}_{Scalar (M)} \forall x \in \{I\} \forall w \in \{I\} ((r \cdot_{M} w \in \{I\} \land r \cdot_{M} (w +_{M} x) = (r \cdot_{M} w) +_{M} (r \cdot_{M} x) \land (q +_{Scalar (M)} r) \cdot_{M} w = (q \cdot_{M} w) +_{M} (r \cdot_{M} w)) \land ((q \cdot_{Scalar (M)} r) \cdot_{M} w = q \cdot_{M} (r \cdot_{M} w) \land 1_{Scalar (M)} \cdot_{M} w = w))$
91	1	lmodbase	$⊢ \{I\} \in V \to \{I\} = {Base}_{M}$
92	5 91	ax-mp	$⊢ \{I\} = {Base}_{M}$
93		eqid	$⊢ +_{M} = +_{M}$
94		eqid	$⊢ \cdot_{M} = \cdot_{M}$
95		eqid	$⊢ Scalar (M) = Scalar (M)$
96		eqid	$⊢ {Base}_{Scalar (M)} = {Base}_{Scalar (M)}$
97		eqid	$⊢ +_{Scalar (M)} = +_{Scalar (M)}$
98		eqid	$⊢ \cdot_{Scalar (M)} = \cdot_{Scalar (M)}$
99		eqid	$⊢ 1_{Scalar (M)} = 1_{Scalar (M)}$
100	92 93 94 95 96 97 98 99	islmod	$⊢ M \in LMod \leftrightarrow (M \in Grp \land Scalar (M) \in Ring \land \forall q \in {Base}_{Scalar (M)} \forall r \in {Base}_{Scalar (M)} \forall x \in \{I\} \forall w \in \{I\} ((r \cdot_{M} w \in \{I\} \land r \cdot_{M} (w +_{M} x) = (r \cdot_{M} w) +_{M} (r \cdot_{M} x) \land (q +_{Scalar (M)} r) \cdot_{M} w = (q \cdot_{M} w) +_{M} (r \cdot_{M} w)) \land ((q \cdot_{Scalar (M)} r) \cdot_{M} w = q \cdot_{M} (r \cdot_{M} w) \land 1_{Scalar (M)} \cdot_{M} w = w)))$
101	30 35 90 100	syl3anbrc	$⊢ (I \in V \land R \in Ring) \to M \in LMod$

Metamath Proof Explorer

Theorem lmod1

Proof