Theorem lmod1

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

	Ref	Expression
Hypothesis	lmod1.m	$$⊢M=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\left\{I\right\}⟩,⟨{+}_{\mathrm{ndx}},\left\{⟨⟨I,I⟩,I⟩\right\}⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),R⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\left(x\in {\mathrm{Base}}_R,y\in \left\{I\right\}⟼y\right)⟩\right\}$$
Assertion	lmod1	$$⊢\left(I\in V\wedge R\in \mathrm{Ring}\right)\to M\in \mathrm{LMod}$$

Proof

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