Theorem islmodd

Description: Properties that determine a left module. See note in isgrpd2 regarding the ph on hypotheses that name structure components. (Contributed by Mario Carneiro, 22-Jun-2014)

	Ref	Expression
Hypotheses	islmodd.v	$$⊢\phi \to V={\mathrm{Base}}_W$$
	islmodd.a	$$⊢\phi \to \underset{\dot{}}{+}={+}_W$$
	islmodd.f	$$⊢\phi \to F=\mathrm{Scalar}\left(W\right)$$
	islmodd.s	$$⊢\phi \to \underset{\dot{}}{·}={\cdot }_W$$
	islmodd.b	$$⊢\phi \to B={\mathrm{Base}}_F$$
	islmodd.p	$$⊢\phi \to \underset{\dot{}}{⨣}={+}_F$$
	islmodd.t	$$⊢\phi \to \underset{\dot{}}{\times }={\cdot }_F$$
	islmodd.u	$$⊢\phi \to \underset{\dot{}}{1}=1_F$$
	islmodd.r	$$⊢\phi \to F\in \mathrm{Ring}$$
	islmodd.l	$$⊢\phi \to W\in \mathrm{Grp}$$
	islmodd.w	$$⊢\left(\phi \wedge x\in B\wedge y\in V\right)\to x\underset{\dot{}}{·}y\in V$$
	islmodd.c	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in V\wedge z\in V\right)\right)\to x\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)$$
	islmodd.d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\wedge z\in V\right)\right)\to \left(x\underset{\dot{}}{⨣}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)$$
	islmodd.e	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\wedge z\in V\right)\right)\to \left(x\underset{\dot{}}{\times }y\right)\underset{\dot{}}{·}z=x\underset{\dot{}}{·}\left(y\underset{\dot{}}{·}z\right)$$
	islmodd.g	$$⊢\left(\phi \wedge x\in V\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}x=x$$
Assertion	islmodd	$$⊢\phi \to W\in \mathrm{LMod}$$

Proof

Step	Hyp	Ref	Expression
1		islmodd.v	$$⊢\phi \to V={\mathrm{Base}}_W$$
2		islmodd.a	$$⊢\phi \to \underset{\dot{}}{+}={+}_W$$
3		islmodd.f	$$⊢\phi \to F=\mathrm{Scalar}\left(W\right)$$
4		islmodd.s	$$⊢\phi \to \underset{\dot{}}{·}={\cdot }_W$$
5		islmodd.b	$$⊢\phi \to B={\mathrm{Base}}_F$$
6		islmodd.p	$$⊢\phi \to \underset{\dot{}}{⨣}={+}_F$$
7		islmodd.t	$$⊢\phi \to \underset{\dot{}}{\times }={\cdot }_F$$
8		islmodd.u	$$⊢\phi \to \underset{\dot{}}{1}=1_F$$
9		islmodd.r	$$⊢\phi \to F\in \mathrm{Ring}$$
10		islmodd.l	$$⊢\phi \to W\in \mathrm{Grp}$$
11		islmodd.w	$$⊢\left(\phi \wedge x\in B\wedge y\in V\right)\to x\underset{\dot{}}{·}y\in V$$
12		islmodd.c	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in V\wedge z\in V\right)\right)\to x\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)$$
13		islmodd.d	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\wedge z\in V\right)\right)\to \left(x\underset{\dot{}}{⨣}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)$$
14		islmodd.e	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\wedge z\in V\right)\right)\to \left(x\underset{\dot{}}{\times }y\right)\underset{\dot{}}{·}z=x\underset{\dot{}}{·}\left(y\underset{\dot{}}{·}z\right)$$
15		islmodd.g	$$⊢\left(\phi \wedge x\in V\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}x=x$$
16	3 9	eqeltrrd	$$⊢\phi \to \mathrm{Scalar}\left(W\right)\in \mathrm{Ring}$$
17	11	3expb	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in V\right)\right)\to x\underset{\dot{}}{·}y\in V$$
18	17	ralrimivva	$$⊢\phi \to \forall x\in B\forall y\in Vx\underset{\dot{}}{·}y\in V$$
19		oveq1	$$⊢x=r\to x\underset{\dot{}}{·}y=r\underset{\dot{}}{·}y$$
20	19	eleq1d	$$⊢x=r\to \left(x\underset{\dot{}}{·}y\in V\leftrightarrow r\underset{\dot{}}{·}y\in V\right)$$
21		oveq2	$$⊢y=w\to r\underset{\dot{}}{·}y=r\underset{\dot{}}{·}w$$
22	21	eleq1d	$$⊢y=w\to \left(r\underset{\dot{}}{·}y\in V\leftrightarrow r\underset{\dot{}}{·}w\in V\right)$$
23	20 22	rspc2v	$$⊢\left(r\in B\wedge w\in V\right)\to \left(\forall x\in B\forall y\in Vx\underset{\dot{}}{·}y\in V\to r\underset{\dot{}}{·}w\in V\right)$$
24	23	ad2ant2l	$$⊢\left(\left(x\in B\wedge r\in B\right)\wedge \left(u\in V\wedge w\in V\right)\right)\to \left(\forall x\in B\forall y\in Vx\underset{\dot{}}{·}y\in V\to r\underset{\dot{}}{·}w\in V\right)$$
25	18 24	mpan9	$$⊢\left(\phi \wedge \left(\left(x\in B\wedge r\in B\right)\wedge \left(u\in V\wedge w\in V\right)\right)\right)\to r\underset{\dot{}}{·}w\in V$$
26	12	ralrimivvva	$$⊢\phi \to \forall x\in B\forall y\in V\forall z\in Vx\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)$$
27		oveq1	$$⊢x=r\to x\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=r\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)$$
28		oveq1	$$⊢x=r\to x\underset{\dot{}}{·}z=r\underset{\dot{}}{·}z$$
29	19 28	oveq12d	$$⊢x=r\to \left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)=\left(r\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}z\right)$$
30	27 29	eqeq12d	$$⊢x=r\to \left(x\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)\leftrightarrow r\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(r\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}z\right)\right)$$
31		oveq1	$$⊢y=w\to y\underset{\dot{}}{+}z=w\underset{\dot{}}{+}z$$
32	31	oveq2d	$$⊢y=w\to r\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}z\right)$$
33	21	oveq1d	$$⊢y=w\to \left(r\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}z\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}z\right)$$
34	32 33	eqeq12d	$$⊢y=w\to \left(r\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(r\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}z\right)\leftrightarrow r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}z\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}z\right)\right)$$
35		oveq2	$$⊢z=u\to w\underset{\dot{}}{+}z=w\underset{\dot{}}{+}u$$
36	35	oveq2d	$$⊢z=u\to r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}z\right)=r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}u\right)$$
37		oveq2	$$⊢z=u\to r\underset{\dot{}}{·}z=r\underset{\dot{}}{·}u$$
38	37	oveq2d	$$⊢z=u\to \left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}z\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}u\right)$$
39	36 38	eqeq12d	$$⊢z=u\to \left(r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}z\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}z\right)\leftrightarrow r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}u\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}u\right)\right)$$
40	30 34 39	rspc3v	$$⊢\left(r\in B\wedge w\in V\wedge u\in V\right)\to \left(\forall x\in B\forall y\in V\forall z\in Vx\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)\to r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}u\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}u\right)\right)$$
41	40	3com23	$$⊢\left(r\in B\wedge u\in V\wedge w\in V\right)\to \left(\forall x\in B\forall y\in V\forall z\in Vx\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)\to r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}u\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}u\right)\right)$$
42	41	3expb	$$⊢\left(r\in B\wedge \left(u\in V\wedge w\in V\right)\right)\to \left(\forall x\in B\forall y\in V\forall z\in Vx\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)\to r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}u\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}u\right)\right)$$
43	42	adantll	$$⊢\left(\left(x\in B\wedge r\in B\right)\wedge \left(u\in V\wedge w\in V\right)\right)\to \left(\forall x\in B\forall y\in V\forall z\in Vx\underset{\dot{}}{·}\left(y\underset{\dot{}}{+}z\right)=\left(x\underset{\dot{}}{·}y\right)\underset{\dot{}}{+}\left(x\underset{\dot{}}{·}z\right)\to r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}u\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}u\right)\right)$$
44	26 43	mpan9	$$⊢\left(\phi \wedge \left(\left(x\in B\wedge r\in B\right)\wedge \left(u\in V\wedge w\in V\right)\right)\right)\to r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}u\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}u\right)$$
45		simpll	$$⊢\left(\left(x\in B\wedge r\in B\right)\wedge \left(u\in V\wedge w\in V\right)\right)\to x\in B$$
46	13	3exp2	$$⊢\phi \to \left(x\in B\to \left(y\in B\to \left(z\in V\to \left(x\underset{\dot{}}{⨣}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)\right)\right)\right)$$
47	46	imp43	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge \left(y\in B\wedge z\in V\right)\right)\to \left(x\underset{\dot{}}{⨣}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)$$
48	47	ralrimivva	$$⊢\left(\phi \wedge x\in B\right)\to \forall y\in B\forall z\in V\left(x\underset{\dot{}}{⨣}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)$$
49	45 48	sylan2	$$⊢\left(\phi \wedge \left(\left(x\in B\wedge r\in B\right)\wedge \left(u\in V\wedge w\in V\right)\right)\right)\to \forall y\in B\forall z\in V\left(x\underset{\dot{}}{⨣}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)$$
50		simprlr	$$⊢\left(\phi \wedge \left(\left(x\in B\wedge r\in B\right)\wedge \left(u\in V\wedge w\in V\right)\right)\right)\to r\in B$$
51		simprrr	$$⊢\left(\phi \wedge \left(\left(x\in B\wedge r\in B\right)\wedge \left(u\in V\wedge w\in V\right)\right)\right)\to w\in V$$
52		oveq2	$$⊢y=r\to x\underset{\dot{}}{⨣}y=x\underset{\dot{}}{⨣}r$$
53	52	oveq1d	$$⊢y=r\to \left(x\underset{\dot{}}{⨣}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}z$$
54		oveq1	$$⊢y=r\to y\underset{\dot{}}{·}z=r\underset{\dot{}}{·}z$$
55	54	oveq2d	$$⊢y=r\to \left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}z\right)$$
56	53 55	eqeq12d	$$⊢y=r\to \left(\left(x\underset{\dot{}}{⨣}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)\leftrightarrow \left(x\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}z\right)\right)$$
57		oveq2	$$⊢z=w\to \left(x\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w$$
58		oveq2	$$⊢z=w\to x\underset{\dot{}}{·}z=x\underset{\dot{}}{·}w$$
59		oveq2	$$⊢z=w\to r\underset{\dot{}}{·}z=r\underset{\dot{}}{·}w$$
60	58 59	oveq12d	$$⊢z=w\to \left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}z\right)=\left(x\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)$$
61	57 60	eqeq12d	$$⊢z=w\to \left(\left(x\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}z\right)\leftrightarrow \left(x\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(x\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)\right)$$
62	56 61	rspc2v	$$⊢\left(r\in B\wedge w\in V\right)\to \left(\forall y\in B\forall z\in V\left(x\underset{\dot{}}{⨣}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)\to \left(x\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(x\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)\right)$$
63	50 51 62	syl2anc	$$⊢\left(\phi \wedge \left(\left(x\in B\wedge r\in B\right)\wedge \left(u\in V\wedge w\in V\right)\right)\right)\to \left(\forall y\in B\forall z\in V\left(x\underset{\dot{}}{⨣}y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{·}z\right)\underset{\dot{}}{+}\left(y\underset{\dot{}}{·}z\right)\to \left(x\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(x\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)\right)$$
64	49 63	mpd	$$⊢\left(\phi \wedge \left(\left(x\in B\wedge r\in B\right)\wedge \left(u\in V\wedge w\in V\right)\right)\right)\to \left(x\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(x\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)$$
65	25 44 64	3jca	$$⊢\left(\phi \wedge \left(\left(x\in B\wedge r\in B\right)\wedge \left(u\in V\wedge w\in V\right)\right)\right)\to \left(r\underset{\dot{}}{·}w\in V\wedge r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}u\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}u\right)\wedge \left(x\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(x\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)\right)$$
66	14	3exp2	$$⊢\phi \to \left(x\in B\to \left(y\in B\to \left(z\in V\to \left(x\underset{\dot{}}{\times }y\right)\underset{\dot{}}{·}z=x\underset{\dot{}}{·}\left(y\underset{\dot{}}{·}z\right)\right)\right)\right)$$
67	66	imp43	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge \left(y\in B\wedge z\in V\right)\right)\to \left(x\underset{\dot{}}{\times }y\right)\underset{\dot{}}{·}z=x\underset{\dot{}}{·}\left(y\underset{\dot{}}{·}z\right)$$
68	67	ralrimivva	$$⊢\left(\phi \wedge x\in B\right)\to \forall y\in B\forall z\in V\left(x\underset{\dot{}}{\times }y\right)\underset{\dot{}}{·}z=x\underset{\dot{}}{·}\left(y\underset{\dot{}}{·}z\right)$$
69	45 68	sylan2	$$⊢\left(\phi \wedge \left(\left(x\in B\wedge r\in B\right)\wedge \left(u\in V\wedge w\in V\right)\right)\right)\to \forall y\in B\forall z\in V\left(x\underset{\dot{}}{\times }y\right)\underset{\dot{}}{·}z=x\underset{\dot{}}{·}\left(y\underset{\dot{}}{·}z\right)$$
70		oveq2	$$⊢y=r\to x\underset{\dot{}}{\times }y=x\underset{\dot{}}{\times }r$$
71	70	oveq1d	$$⊢y=r\to \left(x\underset{\dot{}}{\times }y\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}z$$
72	54	oveq2d	$$⊢y=r\to x\underset{\dot{}}{·}\left(y\underset{\dot{}}{·}z\right)=x\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}z\right)$$
73	71 72	eqeq12d	$$⊢y=r\to \left(\left(x\underset{\dot{}}{\times }y\right)\underset{\dot{}}{·}z=x\underset{\dot{}}{·}\left(y\underset{\dot{}}{·}z\right)\leftrightarrow \left(x\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}z=x\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}z\right)\right)$$
74		oveq2	$$⊢z=w\to \left(x\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}z=\left(x\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w$$
75	59	oveq2d	$$⊢z=w\to x\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}z\right)=x\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)$$
76	74 75	eqeq12d	$$⊢z=w\to \left(\left(x\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}z=x\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}z\right)\leftrightarrow \left(x\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=x\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)\right)$$
77	73 76	rspc2v	$$⊢\left(r\in B\wedge w\in V\right)\to \left(\forall y\in B\forall z\in V\left(x\underset{\dot{}}{\times }y\right)\underset{\dot{}}{·}z=x\underset{\dot{}}{·}\left(y\underset{\dot{}}{·}z\right)\to \left(x\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=x\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)\right)$$
78	50 51 77	syl2anc	$$⊢\left(\phi \wedge \left(\left(x\in B\wedge r\in B\right)\wedge \left(u\in V\wedge w\in V\right)\right)\right)\to \left(\forall y\in B\forall z\in V\left(x\underset{\dot{}}{\times }y\right)\underset{\dot{}}{·}z=x\underset{\dot{}}{·}\left(y\underset{\dot{}}{·}z\right)\to \left(x\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=x\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)\right)$$
79	69 78	mpd	$$⊢\left(\phi \wedge \left(\left(x\in B\wedge r\in B\right)\wedge \left(u\in V\wedge w\in V\right)\right)\right)\to \left(x\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=x\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)$$
80	15	ralrimiva	$$⊢\phi \to \forall x\in V\underset{\dot{}}{1}\underset{\dot{}}{·}x=x$$
81		oveq2	$$⊢x=w\to \underset{\dot{}}{1}\underset{\dot{}}{·}x=\underset{\dot{}}{1}\underset{\dot{}}{·}w$$
82		id	$$⊢x=w\to x=w$$
83	81 82	eqeq12d	$$⊢x=w\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}x=x\leftrightarrow \underset{\dot{}}{1}\underset{\dot{}}{·}w=w\right)$$
84	83	rspcv	$$⊢w\in V\to \left(\forall x\in V\underset{\dot{}}{1}\underset{\dot{}}{·}x=x\to \underset{\dot{}}{1}\underset{\dot{}}{·}w=w\right)$$
85	84	ad2antll	$$⊢\left(\left(x\in B\wedge r\in B\right)\wedge \left(u\in V\wedge w\in V\right)\right)\to \left(\forall x\in V\underset{\dot{}}{1}\underset{\dot{}}{·}x=x\to \underset{\dot{}}{1}\underset{\dot{}}{·}w=w\right)$$
86	80 85	mpan9	$$⊢\left(\phi \wedge \left(\left(x\in B\wedge r\in B\right)\wedge \left(u\in V\wedge w\in V\right)\right)\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}w=w$$
87	65 79 86	jca32	$$⊢\left(\phi \wedge \left(\left(x\in B\wedge r\in B\right)\wedge \left(u\in V\wedge w\in V\right)\right)\right)\to \left(\left(r\underset{\dot{}}{·}w\in V\wedge r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}u\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}u\right)\wedge \left(x\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(x\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)\right)\wedge \left(\left(x\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=x\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}w=w\right)\right)$$
88	87	anassrs	$$⊢\left(\left(\phi \wedge \left(x\in B\wedge r\in B\right)\right)\wedge \left(u\in V\wedge w\in V\right)\right)\to \left(\left(r\underset{\dot{}}{·}w\in V\wedge r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}u\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}u\right)\wedge \left(x\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(x\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)\right)\wedge \left(\left(x\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=x\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}w=w\right)\right)$$
89	88	ralrimivva	$$⊢\left(\phi \wedge \left(x\in B\wedge r\in B\right)\right)\to \forall u\in V\forall w\in V\left(\left(r\underset{\dot{}}{·}w\in V\wedge r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}u\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}u\right)\wedge \left(x\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(x\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)\right)\wedge \left(\left(x\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=x\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}w=w\right)\right)$$
90	89	ralrimivva	$$⊢\phi \to \forall x\in B\forall r\in B\forall u\in V\forall w\in V\left(\left(r\underset{\dot{}}{·}w\in V\wedge r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}u\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}u\right)\wedge \left(x\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(x\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)\right)\wedge \left(\left(x\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=x\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}w=w\right)\right)$$
91	3	fveq2d	$$⊢\phi \to {\mathrm{Base}}_F={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
92	5 91	eqtrd	$$⊢\phi \to B={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
93	4	oveqd	$$⊢\phi \to r\underset{\dot{}}{·}w=r{\cdot }_{W}w$$
94	93 1	eleq12d	$$⊢\phi \to \left(r\underset{\dot{}}{·}w\in V\leftrightarrow r{\cdot }_{W}w\in {\mathrm{Base}}_W\right)$$
95		eqidd	$$⊢\phi \to r=r$$
96	2	oveqd	$$⊢\phi \to w\underset{\dot{}}{+}u=w{+}_{W}u$$
97	4 95 96	oveq123d	$$⊢\phi \to r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}u\right)=r{\cdot }_W\left(w{+}_{W}u\right)$$
98	4	oveqd	$$⊢\phi \to r\underset{\dot{}}{·}u=r{\cdot }_{W}u$$
99	2 93 98	oveq123d	$$⊢\phi \to \left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}u\right)=\left(r{\cdot }_{W}w\right){+}_W\left(r{\cdot }_{W}u\right)$$
100	97 99	eqeq12d	$$⊢\phi \to \left(r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}u\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}u\right)\leftrightarrow r{\cdot }_W\left(w{+}_{W}u\right)=\left(r{\cdot }_{W}w\right){+}_W\left(r{\cdot }_{W}u\right)\right)$$
101	3	fveq2d	$$⊢\phi \to {+}_F={+}_{\mathrm{Scalar}\left(W\right)}$$
102	6 101	eqtrd	$$⊢\phi \to \underset{\dot{}}{⨣}={+}_{\mathrm{Scalar}\left(W\right)}$$
103	102	oveqd	$$⊢\phi \to x\underset{\dot{}}{⨣}r=x{+}_{\mathrm{Scalar}\left(W\right)}r$$
104		eqidd	$$⊢\phi \to w=w$$
105	4 103 104	oveq123d	$$⊢\phi \to \left(x\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(x{+}_{\mathrm{Scalar}\left(W\right)}r\right){\cdot }_{W}w$$
106	4	oveqd	$$⊢\phi \to x\underset{\dot{}}{·}w=x{\cdot }_{W}w$$
107	2 106 93	oveq123d	$$⊢\phi \to \left(x\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)=\left(x{\cdot }_{W}w\right){+}_W\left(r{\cdot }_{W}w\right)$$
108	105 107	eqeq12d	$$⊢\phi \to \left(\left(x\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(x\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)\leftrightarrow \left(x{+}_{\mathrm{Scalar}\left(W\right)}r\right){\cdot }_{W}w=\left(x{\cdot }_{W}w\right){+}_W\left(r{\cdot }_{W}w\right)\right)$$
109	94 100 108	3anbi123d	$$⊢\phi \to \left(\left(r\underset{\dot{}}{·}w\in V\wedge r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}u\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}u\right)\wedge \left(x\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(x\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)\right)\leftrightarrow \left(r{\cdot }_{W}w\in {\mathrm{Base}}_W\wedge r{\cdot }_W\left(w{+}_{W}u\right)=\left(r{\cdot }_{W}w\right){+}_W\left(r{\cdot }_{W}u\right)\wedge \left(x{+}_{\mathrm{Scalar}\left(W\right)}r\right){\cdot }_{W}w=\left(x{\cdot }_{W}w\right){+}_W\left(r{\cdot }_{W}w\right)\right)\right)$$
110	3	fveq2d	$$⊢\phi \to {\cdot }_F={\cdot }_{\mathrm{Scalar}\left(W\right)}$$
111	7 110	eqtrd	$$⊢\phi \to \underset{\dot{}}{\times }={\cdot }_{\mathrm{Scalar}\left(W\right)}$$
112	111	oveqd	$$⊢\phi \to x\underset{\dot{}}{\times }r=x{\cdot }_{\mathrm{Scalar}\left(W\right)}r$$
113	4 112 104	oveq123d	$$⊢\phi \to \left(x\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=\left(x{\cdot }_{\mathrm{Scalar}\left(W\right)}r\right){\cdot }_{W}w$$
114		eqidd	$$⊢\phi \to x=x$$
115	4 114 93	oveq123d	$$⊢\phi \to x\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)=x{\cdot }_W\left(r{\cdot }_{W}w\right)$$
116	113 115	eqeq12d	$$⊢\phi \to \left(\left(x\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=x\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)\leftrightarrow \left(x{\cdot }_{\mathrm{Scalar}\left(W\right)}r\right){\cdot }_{W}w=x{\cdot }_W\left(r{\cdot }_{W}w\right)\right)$$
117	3	fveq2d	$$⊢\phi \to 1_F=1_{\mathrm{Scalar}\left(W\right)}$$
118	8 117	eqtrd	$$⊢\phi \to \underset{\dot{}}{1}=1_{\mathrm{Scalar}\left(W\right)}$$
119	4 118 104	oveq123d	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{·}w=1_{\mathrm{Scalar}\left(W\right)}{\cdot }_{W}w$$
120	119	eqeq1d	$$⊢\phi \to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}w=w\leftrightarrow 1_{\mathrm{Scalar}\left(W\right)}{\cdot }_{W}w=w\right)$$
121	116 120	anbi12d	$$⊢\phi \to \left(\left(\left(x\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=x\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}w=w\right)\leftrightarrow \left(\left(x{\cdot }_{\mathrm{Scalar}\left(W\right)}r\right){\cdot }_{W}w=x{\cdot }_W\left(r{\cdot }_{W}w\right)\wedge 1_{\mathrm{Scalar}\left(W\right)}{\cdot }_{W}w=w\right)\right)$$
122	109 121	anbi12d	$$⊢\phi \to \left(\left(\left(r\underset{\dot{}}{·}w\in V\wedge r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}u\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}u\right)\wedge \left(x\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(x\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)\right)\wedge \left(\left(x\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=x\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}w=w\right)\right)\leftrightarrow \left(\left(r{\cdot }_{W}w\in {\mathrm{Base}}_W\wedge r{\cdot }_W\left(w{+}_{W}u\right)=\left(r{\cdot }_{W}w\right){+}_W\left(r{\cdot }_{W}u\right)\wedge \left(x{+}_{\mathrm{Scalar}\left(W\right)}r\right){\cdot }_{W}w=\left(x{\cdot }_{W}w\right){+}_W\left(r{\cdot }_{W}w\right)\right)\wedge \left(\left(x{\cdot }_{\mathrm{Scalar}\left(W\right)}r\right){\cdot }_{W}w=x{\cdot }_W\left(r{\cdot }_{W}w\right)\wedge 1_{\mathrm{Scalar}\left(W\right)}{\cdot }_{W}w=w\right)\right)\right)$$
123	1 122	raleqbidv	$$⊢\phi \to \left(\forall w\in V\left(\left(r\underset{\dot{}}{·}w\in V\wedge r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}u\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}u\right)\wedge \left(x\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(x\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)\right)\wedge \left(\left(x\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=x\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}w=w\right)\right)\leftrightarrow \forall w\in {\mathrm{Base}}_W\left(\left(r{\cdot }_{W}w\in {\mathrm{Base}}_W\wedge r{\cdot }_W\left(w{+}_{W}u\right)=\left(r{\cdot }_{W}w\right){+}_W\left(r{\cdot }_{W}u\right)\wedge \left(x{+}_{\mathrm{Scalar}\left(W\right)}r\right){\cdot }_{W}w=\left(x{\cdot }_{W}w\right){+}_W\left(r{\cdot }_{W}w\right)\right)\wedge \left(\left(x{\cdot }_{\mathrm{Scalar}\left(W\right)}r\right){\cdot }_{W}w=x{\cdot }_W\left(r{\cdot }_{W}w\right)\wedge 1_{\mathrm{Scalar}\left(W\right)}{\cdot }_{W}w=w\right)\right)\right)$$
124	1 123	raleqbidv	$$⊢\phi \to \left(\forall u\in V\forall w\in V\left(\left(r\underset{\dot{}}{·}w\in V\wedge r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}u\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}u\right)\wedge \left(x\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(x\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)\right)\wedge \left(\left(x\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=x\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}w=w\right)\right)\leftrightarrow \forall u\in {\mathrm{Base}}_W\forall w\in {\mathrm{Base}}_W\left(\left(r{\cdot }_{W}w\in {\mathrm{Base}}_W\wedge r{\cdot }_W\left(w{+}_{W}u\right)=\left(r{\cdot }_{W}w\right){+}_W\left(r{\cdot }_{W}u\right)\wedge \left(x{+}_{\mathrm{Scalar}\left(W\right)}r\right){\cdot }_{W}w=\left(x{\cdot }_{W}w\right){+}_W\left(r{\cdot }_{W}w\right)\right)\wedge \left(\left(x{\cdot }_{\mathrm{Scalar}\left(W\right)}r\right){\cdot }_{W}w=x{\cdot }_W\left(r{\cdot }_{W}w\right)\wedge 1_{\mathrm{Scalar}\left(W\right)}{\cdot }_{W}w=w\right)\right)\right)$$
125	92 124	raleqbidv	$$⊢\phi \to \left(\forall r\in B\forall u\in V\forall w\in V\left(\left(r\underset{\dot{}}{·}w\in V\wedge r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}u\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}u\right)\wedge \left(x\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(x\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)\right)\wedge \left(\left(x\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=x\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}w=w\right)\right)\leftrightarrow \forall r\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\forall u\in {\mathrm{Base}}_W\forall w\in {\mathrm{Base}}_W\left(\left(r{\cdot }_{W}w\in {\mathrm{Base}}_W\wedge r{\cdot }_W\left(w{+}_{W}u\right)=\left(r{\cdot }_{W}w\right){+}_W\left(r{\cdot }_{W}u\right)\wedge \left(x{+}_{\mathrm{Scalar}\left(W\right)}r\right){\cdot }_{W}w=\left(x{\cdot }_{W}w\right){+}_W\left(r{\cdot }_{W}w\right)\right)\wedge \left(\left(x{\cdot }_{\mathrm{Scalar}\left(W\right)}r\right){\cdot }_{W}w=x{\cdot }_W\left(r{\cdot }_{W}w\right)\wedge 1_{\mathrm{Scalar}\left(W\right)}{\cdot }_{W}w=w\right)\right)\right)$$
126	92 125	raleqbidv	$$⊢\phi \to \left(\forall x\in B\forall r\in B\forall u\in V\forall w\in V\left(\left(r\underset{\dot{}}{·}w\in V\wedge r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}u\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}u\right)\wedge \left(x\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(x\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)\right)\wedge \left(\left(x\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=x\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}w=w\right)\right)\leftrightarrow \forall x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\forall r\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\forall u\in {\mathrm{Base}}_W\forall w\in {\mathrm{Base}}_W\left(\left(r{\cdot }_{W}w\in {\mathrm{Base}}_W\wedge r{\cdot }_W\left(w{+}_{W}u\right)=\left(r{\cdot }_{W}w\right){+}_W\left(r{\cdot }_{W}u\right)\wedge \left(x{+}_{\mathrm{Scalar}\left(W\right)}r\right){\cdot }_{W}w=\left(x{\cdot }_{W}w\right){+}_W\left(r{\cdot }_{W}w\right)\right)\wedge \left(\left(x{\cdot }_{\mathrm{Scalar}\left(W\right)}r\right){\cdot }_{W}w=x{\cdot }_W\left(r{\cdot }_{W}w\right)\wedge 1_{\mathrm{Scalar}\left(W\right)}{\cdot }_{W}w=w\right)\right)\right)$$
127	90 126	mpbid	$$⊢\phi \to \forall x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\forall r\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\forall u\in {\mathrm{Base}}_W\forall w\in {\mathrm{Base}}_W\left(\left(r{\cdot }_{W}w\in {\mathrm{Base}}_W\wedge r{\cdot }_W\left(w{+}_{W}u\right)=\left(r{\cdot }_{W}w\right){+}_W\left(r{\cdot }_{W}u\right)\wedge \left(x{+}_{\mathrm{Scalar}\left(W\right)}r\right){\cdot }_{W}w=\left(x{\cdot }_{W}w\right){+}_W\left(r{\cdot }_{W}w\right)\right)\wedge \left(\left(x{\cdot }_{\mathrm{Scalar}\left(W\right)}r\right){\cdot }_{W}w=x{\cdot }_W\left(r{\cdot }_{W}w\right)\wedge 1_{\mathrm{Scalar}\left(W\right)}{\cdot }_{W}w=w\right)\right)$$
128		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
129		eqid	$$⊢{+}_W={+}_W$$
130		eqid	$$⊢{\cdot }_W={\cdot }_W$$
131		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
132		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
133		eqid	$$⊢{+}_{\mathrm{Scalar}\left(W\right)}={+}_{\mathrm{Scalar}\left(W\right)}$$
134		eqid	$$⊢{\cdot }_{\mathrm{Scalar}\left(W\right)}={\cdot }_{\mathrm{Scalar}\left(W\right)}$$
135		eqid	$$⊢1_{\mathrm{Scalar}\left(W\right)}=1_{\mathrm{Scalar}\left(W\right)}$$
136	128 129 130 131 132 133 134 135	islmod	$$⊢W\in \mathrm{LMod}\leftrightarrow \left(W\in \mathrm{Grp}\wedge \mathrm{Scalar}\left(W\right)\in \mathrm{Ring}\wedge \forall x\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\forall r\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\forall u\in {\mathrm{Base}}_W\forall w\in {\mathrm{Base}}_W\left(\left(r{\cdot }_{W}w\in {\mathrm{Base}}_W\wedge r{\cdot }_W\left(w{+}_{W}u\right)=\left(r{\cdot }_{W}w\right){+}_W\left(r{\cdot }_{W}u\right)\wedge \left(x{+}_{\mathrm{Scalar}\left(W\right)}r\right){\cdot }_{W}w=\left(x{\cdot }_{W}w\right){+}_W\left(r{\cdot }_{W}w\right)\right)\wedge \left(\left(x{\cdot }_{\mathrm{Scalar}\left(W\right)}r\right){\cdot }_{W}w=x{\cdot }_W\left(r{\cdot }_{W}w\right)\wedge 1_{\mathrm{Scalar}\left(W\right)}{\cdot }_{W}w=w\right)\right)\right)$$
137	10 16 127 136	syl3anbrc	$$⊢\phi \to W\in \mathrm{LMod}$$