Theorem islmod

Description: The predicate "is a left module". (Contributed by NM, 4-Nov-2013) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	islmod.v	$$⊢V={\mathrm{Base}}_W$$
	islmod.a	$$⊢\underset{\dot{}}{+}={+}_W$$
	islmod.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	islmod.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	islmod.k	$$⊢K={\mathrm{Base}}_F$$
	islmod.p	$$⊢\underset{\dot{}}{⨣}={+}_F$$
	islmod.t	$$⊢\underset{\dot{}}{\times }={\cdot }_F$$
	islmod.u	$$⊢\underset{\dot{}}{1}=1_F$$
Assertion	islmod	$$⊢W\in \mathrm{LMod}\leftrightarrow \left(W\in \mathrm{Grp}\wedge F\in \mathrm{Ring}\wedge \forall q\in K\forall r\in K\forall x\in V\forall w\in V\left(\left(r\underset{\dot{}}{·}w\in V\wedge r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}x\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}x\right)\wedge \left(q\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(q\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=q\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}w=w\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		islmod.v	$$⊢V={\mathrm{Base}}_W$$
2		islmod.a	$$⊢\underset{\dot{}}{+}={+}_W$$
3		islmod.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
4		islmod.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
5		islmod.k	$$⊢K={\mathrm{Base}}_F$$
6		islmod.p	$$⊢\underset{\dot{}}{⨣}={+}_F$$
7		islmod.t	$$⊢\underset{\dot{}}{\times }={\cdot }_F$$
8		islmod.u	$$⊢\underset{\dot{}}{1}=1_F$$
9		fveq2	$$⊢g=W\to {\mathrm{Base}}_g={\mathrm{Base}}_W$$
10	9 1	syl6eqr	$$⊢g=W\to {\mathrm{Base}}_g=V$$
11		fveq2	$$⊢g=W\to {+}_g={+}_W$$
12	11 2	syl6eqr	$$⊢g=W\to {+}_g=\underset{\dot{}}{+}$$
13		fveq2	$$⊢g=W\to \mathrm{Scalar}\left(g\right)=\mathrm{Scalar}\left(W\right)$$
14	13 4	syl6eqr	$$⊢g=W\to \mathrm{Scalar}\left(g\right)=F$$
15		fveq2	$$⊢g=W\to {\cdot }_g={\cdot }_W$$
16	15 3	syl6eqr	$$⊢g=W\to {\cdot }_g=\underset{\dot{}}{·}$$
17	16	sbceq1d	$$⊢g=W\to \left(\underset{\dot{}}{[}{\cdot }_g/s\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)\leftrightarrow \underset{\dot{}}{[}\underset{\dot{}}{·}/s\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)\right)$$
18	14 17	sbceqbid	$$⊢g=W\to \left(\underset{\dot{}}{[}\mathrm{Scalar}\left(g\right)/f\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_g/s\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)\leftrightarrow \underset{\dot{}}{[}F/f\underset{\dot{}}{]}\underset{\dot{}}{[}\underset{\dot{}}{·}/s\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)\right)$$
19	12 18	sbceqbid	$$⊢g=W\to \left(\underset{\dot{}}{[}{+}_g/a\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Scalar}\left(g\right)/f\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_g/s\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)\leftrightarrow \underset{\dot{}}{[}\underset{\dot{}}{+}/a\underset{\dot{}}{]}\underset{\dot{}}{[}F/f\underset{\dot{}}{]}\underset{\dot{}}{[}\underset{\dot{}}{·}/s\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)\right)$$
20	10 19	sbceqbid	$$⊢g=W\to \left(\underset{\dot{}}{[}{\mathrm{Base}}_g/v\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_g/a\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Scalar}\left(g\right)/f\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_g/s\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)\leftrightarrow \underset{\dot{}}{[}V/v\underset{\dot{}}{]}\underset{\dot{}}{[}\underset{\dot{}}{+}/a\underset{\dot{}}{]}\underset{\dot{}}{[}F/f\underset{\dot{}}{]}\underset{\dot{}}{[}\underset{\dot{}}{·}/s\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)\right)$$
21	1	fvexi	$$⊢V\in \mathrm{V}$$
22	2	fvexi	$$⊢\underset{\dot{}}{+}\in \mathrm{V}$$
23	4	fvexi	$$⊢F\in \mathrm{V}$$
24		simp3	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to f=F$$
25	24	fveq2d	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to {\mathrm{Base}}_f={\mathrm{Base}}_F$$
26	25 5	syl6eqr	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to {\mathrm{Base}}_f=K$$
27	24	fveq2d	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to {+}_f={+}_F$$
28	27 6	syl6eqr	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to {+}_f=\underset{\dot{}}{⨣}$$
29	24	fveq2d	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to {\cdot }_f={\cdot }_F$$
30	29 7	syl6eqr	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to {\cdot }_f=\underset{\dot{}}{\times }$$
31	30	sbceq1d	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to \left(\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)\leftrightarrow \underset{\dot{}}{[}\underset{\dot{}}{\times }/t\underset{\dot{}}{]}\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)\right)$$
32	7	fvexi	$$⊢\underset{\dot{}}{\times }\in \mathrm{V}$$
33		oveq	$$⊢t=\underset{\dot{}}{\times }\to qtr=q\underset{\dot{}}{\times }r$$
34	33	oveq1d	$$⊢t=\underset{\dot{}}{\times }\to \left(qtr\right)sw=\left(q\underset{\dot{}}{\times }r\right)sw$$
35	34	eqeq1d	$$⊢t=\underset{\dot{}}{\times }\to \left(\left(qtr\right)sw=qs\left(rsw\right)\leftrightarrow \left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\right)$$
36	35	anbi1d	$$⊢t=\underset{\dot{}}{\times }\to \left(\left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\leftrightarrow \left(\left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)$$
37	36	anbi2d	$$⊢t=\underset{\dot{}}{\times }\to \left(\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\leftrightarrow \left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)$$
38	37	2ralbidv	$$⊢t=\underset{\dot{}}{\times }\to \left(\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\leftrightarrow \forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)$$
39	38	2ralbidv	$$⊢t=\underset{\dot{}}{\times }\to \left(\forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\leftrightarrow \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)$$
40	39	anbi2d	$$⊢t=\underset{\dot{}}{\times }\to \left(\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)\leftrightarrow \left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)\right)$$
41	32 40	sbcie	$$⊢\underset{\dot{}}{[}\underset{\dot{}}{\times }/t\underset{\dot{}}{]}\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)\leftrightarrow \left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)$$
42	24	eleq1d	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to \left(f\in \mathrm{Ring}\leftrightarrow F\in \mathrm{Ring}\right)$$
43		simp1	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to v=V$$
44	43	eleq2d	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to \left(rsw\in v\leftrightarrow rsw\in V\right)$$
45		simp2	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to a=\underset{\dot{}}{+}$$
46	45	oveqd	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to wax=w\underset{\dot{}}{+}x$$
47	46	oveq2d	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to rs\left(wax\right)=rs\left(w\underset{\dot{}}{+}x\right)$$
48	45	oveqd	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to \left(rsw\right)a\left(rsx\right)=\left(rsw\right)\underset{\dot{}}{+}\left(rsx\right)$$
49	47 48	eqeq12d	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to \left(rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\leftrightarrow rs\left(w\underset{\dot{}}{+}x\right)=\left(rsw\right)\underset{\dot{}}{+}\left(rsx\right)\right)$$
50	45	oveqd	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to \left(qsw\right)a\left(rsw\right)=\left(qsw\right)\underset{\dot{}}{+}\left(rsw\right)$$
51	50	eqeq2d	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to \left(\left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\leftrightarrow \left(qpr\right)sw=\left(qsw\right)\underset{\dot{}}{+}\left(rsw\right)\right)$$
52	44 49 51	3anbi123d	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to \left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\leftrightarrow \left(rsw\in V\wedge rs\left(w\underset{\dot{}}{+}x\right)=\left(rsw\right)\underset{\dot{}}{+}\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)\underset{\dot{}}{+}\left(rsw\right)\right)\right)$$
53	24	fveq2d	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to 1_f=1_F$$
54	53 8	syl6eqr	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to 1_f=\underset{\dot{}}{1}$$
55	54	oveq1d	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to 1_{f}sw=\underset{\dot{}}{1}sw$$
56	55	eqeq1d	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to \left(1_{f}sw=w\leftrightarrow \underset{\dot{}}{1}sw=w\right)$$
57	56	anbi2d	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to \left(\left(\left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\leftrightarrow \left(\left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\wedge \underset{\dot{}}{1}sw=w\right)\right)$$
58	52 57	anbi12d	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to \left(\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\leftrightarrow \left(\left(rsw\in V\wedge rs\left(w\underset{\dot{}}{+}x\right)=\left(rsw\right)\underset{\dot{}}{+}\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)\underset{\dot{}}{+}\left(rsw\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\wedge \underset{\dot{}}{1}sw=w\right)\right)\right)$$
59	43 58	raleqbidv	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to \left(\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\leftrightarrow \forall w\in V\left(\left(rsw\in V\wedge rs\left(w\underset{\dot{}}{+}x\right)=\left(rsw\right)\underset{\dot{}}{+}\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)\underset{\dot{}}{+}\left(rsw\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\wedge \underset{\dot{}}{1}sw=w\right)\right)\right)$$
60	43 59	raleqbidv	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to \left(\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\leftrightarrow \forall x\in V\forall w\in V\left(\left(rsw\in V\wedge rs\left(w\underset{\dot{}}{+}x\right)=\left(rsw\right)\underset{\dot{}}{+}\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)\underset{\dot{}}{+}\left(rsw\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\wedge \underset{\dot{}}{1}sw=w\right)\right)\right)$$
61	60	2ralbidv	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to \left(\forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\leftrightarrow \forall q\in k\forall r\in k\forall x\in V\forall w\in V\left(\left(rsw\in V\wedge rs\left(w\underset{\dot{}}{+}x\right)=\left(rsw\right)\underset{\dot{}}{+}\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)\underset{\dot{}}{+}\left(rsw\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\wedge \underset{\dot{}}{1}sw=w\right)\right)\right)$$
62	42 61	anbi12d	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to \left(\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)\leftrightarrow \left(F\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in V\forall w\in V\left(\left(rsw\in V\wedge rs\left(w\underset{\dot{}}{+}x\right)=\left(rsw\right)\underset{\dot{}}{+}\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)\underset{\dot{}}{+}\left(rsw\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\wedge \underset{\dot{}}{1}sw=w\right)\right)\right)\right)$$
63	41 62	syl5bb	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to \left(\underset{\dot{}}{[}\underset{\dot{}}{\times }/t\underset{\dot{}}{]}\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)\leftrightarrow \left(F\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in V\forall w\in V\left(\left(rsw\in V\wedge rs\left(w\underset{\dot{}}{+}x\right)=\left(rsw\right)\underset{\dot{}}{+}\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)\underset{\dot{}}{+}\left(rsw\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\wedge \underset{\dot{}}{1}sw=w\right)\right)\right)\right)$$
64	31 63	bitrd	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to \left(\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)\leftrightarrow \left(F\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in V\forall w\in V\left(\left(rsw\in V\wedge rs\left(w\underset{\dot{}}{+}x\right)=\left(rsw\right)\underset{\dot{}}{+}\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)\underset{\dot{}}{+}\left(rsw\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\wedge \underset{\dot{}}{1}sw=w\right)\right)\right)\right)$$
65	28 64	sbceqbid	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to \left(\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)\leftrightarrow \underset{\dot{}}{[}\underset{\dot{}}{⨣}/p\underset{\dot{}}{]}\left(F\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in V\forall w\in V\left(\left(rsw\in V\wedge rs\left(w\underset{\dot{}}{+}x\right)=\left(rsw\right)\underset{\dot{}}{+}\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)\underset{\dot{}}{+}\left(rsw\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\wedge \underset{\dot{}}{1}sw=w\right)\right)\right)\right)$$
66	26 65	sbceqbid	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to \left(\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)\leftrightarrow \underset{\dot{}}{[}K/k\underset{\dot{}}{]}\underset{\dot{}}{[}\underset{\dot{}}{⨣}/p\underset{\dot{}}{]}\left(F\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in V\forall w\in V\left(\left(rsw\in V\wedge rs\left(w\underset{\dot{}}{+}x\right)=\left(rsw\right)\underset{\dot{}}{+}\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)\underset{\dot{}}{+}\left(rsw\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\wedge \underset{\dot{}}{1}sw=w\right)\right)\right)\right)$$
67	66	sbcbidv	$$⊢\left(v=V\wedge a=\underset{\dot{}}{+}\wedge f=F\right)\to \left(\underset{\dot{}}{[}\underset{\dot{}}{·}/s\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)\leftrightarrow \underset{\dot{}}{[}\underset{\dot{}}{·}/s\underset{\dot{}}{]}\underset{\dot{}}{[}K/k\underset{\dot{}}{]}\underset{\dot{}}{[}\underset{\dot{}}{⨣}/p\underset{\dot{}}{]}\left(F\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in V\forall w\in V\left(\left(rsw\in V\wedge rs\left(w\underset{\dot{}}{+}x\right)=\left(rsw\right)\underset{\dot{}}{+}\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)\underset{\dot{}}{+}\left(rsw\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\wedge \underset{\dot{}}{1}sw=w\right)\right)\right)\right)$$
68	21 22 23 67	sbc3ie	$$⊢\underset{\dot{}}{[}V/v\underset{\dot{}}{]}\underset{\dot{}}{[}\underset{\dot{}}{+}/a\underset{\dot{}}{]}\underset{\dot{}}{[}F/f\underset{\dot{}}{]}\underset{\dot{}}{[}\underset{\dot{}}{·}/s\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)\leftrightarrow \underset{\dot{}}{[}\underset{\dot{}}{·}/s\underset{\dot{}}{]}\underset{\dot{}}{[}K/k\underset{\dot{}}{]}\underset{\dot{}}{[}\underset{\dot{}}{⨣}/p\underset{\dot{}}{]}\left(F\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in V\forall w\in V\left(\left(rsw\in V\wedge rs\left(w\underset{\dot{}}{+}x\right)=\left(rsw\right)\underset{\dot{}}{+}\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)\underset{\dot{}}{+}\left(rsw\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\wedge \underset{\dot{}}{1}sw=w\right)\right)\right)$$
69	3	fvexi	$$⊢\underset{\dot{}}{·}\in \mathrm{V}$$
70	5	fvexi	$$⊢K\in \mathrm{V}$$
71	6	fvexi	$$⊢\underset{\dot{}}{⨣}\in \mathrm{V}$$
72		simp2	$$⊢\left(s=\underset{\dot{}}{·}\wedge k=K\wedge p=\underset{\dot{}}{⨣}\right)\to k=K$$
73		simp1	$$⊢\left(s=\underset{\dot{}}{·}\wedge k=K\wedge p=\underset{\dot{}}{⨣}\right)\to s=\underset{\dot{}}{·}$$
74	73	oveqd	$$⊢\left(s=\underset{\dot{}}{·}\wedge k=K\wedge p=\underset{\dot{}}{⨣}\right)\to rsw=r\underset{\dot{}}{·}w$$
75	74	eleq1d	$$⊢\left(s=\underset{\dot{}}{·}\wedge k=K\wedge p=\underset{\dot{}}{⨣}\right)\to \left(rsw\in V\leftrightarrow r\underset{\dot{}}{·}w\in V\right)$$
76	73	oveqd	$$⊢\left(s=\underset{\dot{}}{·}\wedge k=K\wedge p=\underset{\dot{}}{⨣}\right)\to rs\left(w\underset{\dot{}}{+}x\right)=r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}x\right)$$
77	73	oveqd	$$⊢\left(s=\underset{\dot{}}{·}\wedge k=K\wedge p=\underset{\dot{}}{⨣}\right)\to rsx=r\underset{\dot{}}{·}x$$
78	74 77	oveq12d	$$⊢\left(s=\underset{\dot{}}{·}\wedge k=K\wedge p=\underset{\dot{}}{⨣}\right)\to \left(rsw\right)\underset{\dot{}}{+}\left(rsx\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}x\right)$$
79	76 78	eqeq12d	$$⊢\left(s=\underset{\dot{}}{·}\wedge k=K\wedge p=\underset{\dot{}}{⨣}\right)\to \left(rs\left(w\underset{\dot{}}{+}x\right)=\left(rsw\right)\underset{\dot{}}{+}\left(rsx\right)\leftrightarrow r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}x\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}x\right)\right)$$
80		simp3	$$⊢\left(s=\underset{\dot{}}{·}\wedge k=K\wedge p=\underset{\dot{}}{⨣}\right)\to p=\underset{\dot{}}{⨣}$$
81	80	oveqd	$$⊢\left(s=\underset{\dot{}}{·}\wedge k=K\wedge p=\underset{\dot{}}{⨣}\right)\to qpr=q\underset{\dot{}}{⨣}r$$
82	81	oveq1d	$$⊢\left(s=\underset{\dot{}}{·}\wedge k=K\wedge p=\underset{\dot{}}{⨣}\right)\to \left(qpr\right)sw=\left(q\underset{\dot{}}{⨣}r\right)sw$$
83	73	oveqd	$$⊢\left(s=\underset{\dot{}}{·}\wedge k=K\wedge p=\underset{\dot{}}{⨣}\right)\to \left(q\underset{\dot{}}{⨣}r\right)sw=\left(q\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w$$
84	82 83	eqtrd	$$⊢\left(s=\underset{\dot{}}{·}\wedge k=K\wedge p=\underset{\dot{}}{⨣}\right)\to \left(qpr\right)sw=\left(q\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w$$
85	73	oveqd	$$⊢\left(s=\underset{\dot{}}{·}\wedge k=K\wedge p=\underset{\dot{}}{⨣}\right)\to qsw=q\underset{\dot{}}{·}w$$
86	85 74	oveq12d	$$⊢\left(s=\underset{\dot{}}{·}\wedge k=K\wedge p=\underset{\dot{}}{⨣}\right)\to \left(qsw\right)\underset{\dot{}}{+}\left(rsw\right)=\left(q\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)$$
87	84 86	eqeq12d	$$⊢\left(s=\underset{\dot{}}{·}\wedge k=K\wedge p=\underset{\dot{}}{⨣}\right)\to \left(\left(qpr\right)sw=\left(qsw\right)\underset{\dot{}}{+}\left(rsw\right)\leftrightarrow \left(q\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(q\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)\right)$$
88	75 79 87	3anbi123d	$$⊢\left(s=\underset{\dot{}}{·}\wedge k=K\wedge p=\underset{\dot{}}{⨣}\right)\to \left(\left(rsw\in V\wedge rs\left(w\underset{\dot{}}{+}x\right)=\left(rsw\right)\underset{\dot{}}{+}\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)\underset{\dot{}}{+}\left(rsw\right)\right)\leftrightarrow \left(r\underset{\dot{}}{·}w\in V\wedge r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}x\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}x\right)\wedge \left(q\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(q\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)\right)\right)$$
89	73	oveqd	$$⊢\left(s=\underset{\dot{}}{·}\wedge k=K\wedge p=\underset{\dot{}}{⨣}\right)\to \left(q\underset{\dot{}}{\times }r\right)sw=\left(q\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w$$
90	74	oveq2d	$$⊢\left(s=\underset{\dot{}}{·}\wedge k=K\wedge p=\underset{\dot{}}{⨣}\right)\to qs\left(rsw\right)=qs\left(r\underset{\dot{}}{·}w\right)$$
91	73	oveqd	$$⊢\left(s=\underset{\dot{}}{·}\wedge k=K\wedge p=\underset{\dot{}}{⨣}\right)\to qs\left(r\underset{\dot{}}{·}w\right)=q\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)$$
92	90 91	eqtrd	$$⊢\left(s=\underset{\dot{}}{·}\wedge k=K\wedge p=\underset{\dot{}}{⨣}\right)\to qs\left(rsw\right)=q\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)$$
93	89 92	eqeq12d	$$⊢\left(s=\underset{\dot{}}{·}\wedge k=K\wedge p=\underset{\dot{}}{⨣}\right)\to \left(\left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\leftrightarrow \left(q\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=q\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)\right)$$
94	73	oveqd	$$⊢\left(s=\underset{\dot{}}{·}\wedge k=K\wedge p=\underset{\dot{}}{⨣}\right)\to \underset{\dot{}}{1}sw=\underset{\dot{}}{1}\underset{\dot{}}{·}w$$
95	94	eqeq1d	$$⊢\left(s=\underset{\dot{}}{·}\wedge k=K\wedge p=\underset{\dot{}}{⨣}\right)\to \left(\underset{\dot{}}{1}sw=w\leftrightarrow \underset{\dot{}}{1}\underset{\dot{}}{·}w=w\right)$$
96	93 95	anbi12d	$$⊢\left(s=\underset{\dot{}}{·}\wedge k=K\wedge p=\underset{\dot{}}{⨣}\right)\to \left(\left(\left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\wedge \underset{\dot{}}{1}sw=w\right)\leftrightarrow \left(\left(q\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=q\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}w=w\right)\right)$$
97	88 96	anbi12d	$$⊢\left(s=\underset{\dot{}}{·}\wedge k=K\wedge p=\underset{\dot{}}{⨣}\right)\to \left(\left(\left(rsw\in V\wedge rs\left(w\underset{\dot{}}{+}x\right)=\left(rsw\right)\underset{\dot{}}{+}\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)\underset{\dot{}}{+}\left(rsw\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\wedge \underset{\dot{}}{1}sw=w\right)\right)\leftrightarrow \left(\left(r\underset{\dot{}}{·}w\in V\wedge r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}x\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}x\right)\wedge \left(q\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(q\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=q\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}w=w\right)\right)\right)$$
98	97	2ralbidv	$$⊢\left(s=\underset{\dot{}}{·}\wedge k=K\wedge p=\underset{\dot{}}{⨣}\right)\to \left(\forall x\in V\forall w\in V\left(\left(rsw\in V\wedge rs\left(w\underset{\dot{}}{+}x\right)=\left(rsw\right)\underset{\dot{}}{+}\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)\underset{\dot{}}{+}\left(rsw\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\wedge \underset{\dot{}}{1}sw=w\right)\right)\leftrightarrow \forall x\in V\forall w\in V\left(\left(r\underset{\dot{}}{·}w\in V\wedge r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}x\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}x\right)\wedge \left(q\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(q\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=q\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}w=w\right)\right)\right)$$
99	72 98	raleqbidv	$$⊢\left(s=\underset{\dot{}}{·}\wedge k=K\wedge p=\underset{\dot{}}{⨣}\right)\to \left(\forall r\in k\forall x\in V\forall w\in V\left(\left(rsw\in V\wedge rs\left(w\underset{\dot{}}{+}x\right)=\left(rsw\right)\underset{\dot{}}{+}\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)\underset{\dot{}}{+}\left(rsw\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\wedge \underset{\dot{}}{1}sw=w\right)\right)\leftrightarrow \forall r\in K\forall x\in V\forall w\in V\left(\left(r\underset{\dot{}}{·}w\in V\wedge r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}x\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}x\right)\wedge \left(q\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(q\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=q\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}w=w\right)\right)\right)$$
100	72 99	raleqbidv	$$⊢\left(s=\underset{\dot{}}{·}\wedge k=K\wedge p=\underset{\dot{}}{⨣}\right)\to \left(\forall q\in k\forall r\in k\forall x\in V\forall w\in V\left(\left(rsw\in V\wedge rs\left(w\underset{\dot{}}{+}x\right)=\left(rsw\right)\underset{\dot{}}{+}\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)\underset{\dot{}}{+}\left(rsw\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\wedge \underset{\dot{}}{1}sw=w\right)\right)\leftrightarrow \forall q\in K\forall r\in K\forall x\in V\forall w\in V\left(\left(r\underset{\dot{}}{·}w\in V\wedge r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}x\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}x\right)\wedge \left(q\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(q\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=q\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}w=w\right)\right)\right)$$
101	100	anbi2d	$$⊢\left(s=\underset{\dot{}}{·}\wedge k=K\wedge p=\underset{\dot{}}{⨣}\right)\to \left(\left(F\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in V\forall w\in V\left(\left(rsw\in V\wedge rs\left(w\underset{\dot{}}{+}x\right)=\left(rsw\right)\underset{\dot{}}{+}\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)\underset{\dot{}}{+}\left(rsw\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\wedge \underset{\dot{}}{1}sw=w\right)\right)\right)\leftrightarrow \left(F\in \mathrm{Ring}\wedge \forall q\in K\forall r\in K\forall x\in V\forall w\in V\left(\left(r\underset{\dot{}}{·}w\in V\wedge r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}x\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}x\right)\wedge \left(q\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(q\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=q\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}w=w\right)\right)\right)\right)$$
102	69 70 71 101	sbc3ie	$$⊢\underset{\dot{}}{[}\underset{\dot{}}{·}/s\underset{\dot{}}{]}\underset{\dot{}}{[}K/k\underset{\dot{}}{]}\underset{\dot{}}{[}\underset{\dot{}}{⨣}/p\underset{\dot{}}{]}\left(F\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in V\forall w\in V\left(\left(rsw\in V\wedge rs\left(w\underset{\dot{}}{+}x\right)=\left(rsw\right)\underset{\dot{}}{+}\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)\underset{\dot{}}{+}\left(rsw\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)sw=qs\left(rsw\right)\wedge \underset{\dot{}}{1}sw=w\right)\right)\right)\leftrightarrow \left(F\in \mathrm{Ring}\wedge \forall q\in K\forall r\in K\forall x\in V\forall w\in V\left(\left(r\underset{\dot{}}{·}w\in V\wedge r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}x\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}x\right)\wedge \left(q\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(q\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=q\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}w=w\right)\right)\right)$$
103	68 102	bitri	$$⊢\underset{\dot{}}{[}V/v\underset{\dot{}}{]}\underset{\dot{}}{[}\underset{\dot{}}{+}/a\underset{\dot{}}{]}\underset{\dot{}}{[}F/f\underset{\dot{}}{]}\underset{\dot{}}{[}\underset{\dot{}}{·}/s\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)\leftrightarrow \left(F\in \mathrm{Ring}\wedge \forall q\in K\forall r\in K\forall x\in V\forall w\in V\left(\left(r\underset{\dot{}}{·}w\in V\wedge r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}x\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}x\right)\wedge \left(q\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(q\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=q\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}w=w\right)\right)\right)$$
104	20 103	syl6bb	$$⊢g=W\to \left(\underset{\dot{}}{[}{\mathrm{Base}}_g/v\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_g/a\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Scalar}\left(g\right)/f\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_g/s\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)\leftrightarrow \left(F\in \mathrm{Ring}\wedge \forall q\in K\forall r\in K\forall x\in V\forall w\in V\left(\left(r\underset{\dot{}}{·}w\in V\wedge r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}x\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}x\right)\wedge \left(q\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(q\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=q\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}w=w\right)\right)\right)\right)$$
105		df-lmod	$$⊢\mathrm{LMod}=\left\{g\in \mathrm{Grp}|\underset{\dot{}}{[}{\mathrm{Base}}_g/v\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_g/a\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Scalar}\left(g\right)/f\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_g/s\underset{\dot{}}{]}\underset{\dot{}}{[}{\mathrm{Base}}_f/k\underset{\dot{}}{]}\underset{\dot{}}{[}{+}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}{\cdot }_f/t\underset{\dot{}}{]}\left(f\in \mathrm{Ring}\wedge \forall q\in k\forall r\in k\forall x\in v\forall w\in v\left(\left(rsw\in v\wedge rs\left(wax\right)=\left(rsw\right)a\left(rsx\right)\wedge \left(qpr\right)sw=\left(qsw\right)a\left(rsw\right)\right)\wedge \left(\left(qtr\right)sw=qs\left(rsw\right)\wedge 1_{f}sw=w\right)\right)\right)\right\}$$
106	104 105	elrab2	$$⊢W\in \mathrm{LMod}\leftrightarrow \left(W\in \mathrm{Grp}\wedge \left(F\in \mathrm{Ring}\wedge \forall q\in K\forall r\in K\forall x\in V\forall w\in V\left(\left(r\underset{\dot{}}{·}w\in V\wedge r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}x\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}x\right)\wedge \left(q\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(q\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=q\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}w=w\right)\right)\right)\right)$$
107		3anass	$$⊢\left(W\in \mathrm{Grp}\wedge F\in \mathrm{Ring}\wedge \forall q\in K\forall r\in K\forall x\in V\forall w\in V\left(\left(r\underset{\dot{}}{·}w\in V\wedge r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}x\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}x\right)\wedge \left(q\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(q\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=q\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}w=w\right)\right)\right)\leftrightarrow \left(W\in \mathrm{Grp}\wedge \left(F\in \mathrm{Ring}\wedge \forall q\in K\forall r\in K\forall x\in V\forall w\in V\left(\left(r\underset{\dot{}}{·}w\in V\wedge r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}x\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}x\right)\wedge \left(q\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(q\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=q\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}w=w\right)\right)\right)\right)$$
108	106 107	bitr4i	$$⊢W\in \mathrm{LMod}\leftrightarrow \left(W\in \mathrm{Grp}\wedge F\in \mathrm{Ring}\wedge \forall q\in K\forall r\in K\forall x\in V\forall w\in V\left(\left(r\underset{\dot{}}{·}w\in V\wedge r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}x\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}x\right)\wedge \left(q\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(q\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)\right)\wedge \left(\left(q\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=q\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}w=w\right)\right)\right)$$