Theorem lmodlema

Description: Lemma for properties of a left module. (Contributed by NM, 8-Dec-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	lmodlema	$$⊢\left(W\in \mathrm{LMod}\wedge \left(Q\in K\wedge R\in K\right)\wedge \left(X\in V\wedge Y\in V\right)\right)\to \left(\left(R\underset{\dot{}}{·}Y\in V\wedge R\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}X\right)=\left(R\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}X\right)\wedge \left(Q\underset{\dot{}}{⨣}R\right)\underset{\dot{}}{·}Y=\left(Q\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}Y\right)\right)\wedge \left(\left(Q\underset{\dot{}}{\times }R\right)\underset{\dot{}}{·}Y=Q\underset{\dot{}}{·}\left(R\underset{\dot{}}{·}Y\right)\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}Y=Y\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	1 2 3 4 5 6 7 8	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)$$
10	9	simp3bi	$$⊢W\in \mathrm{LMod}\to \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)$$
11		oveq1	$$⊢q=Q\to q\underset{\dot{}}{⨣}r=Q\underset{\dot{}}{⨣}r$$
12	11	oveq1d	$$⊢q=Q\to \left(q\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(Q\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w$$
13		oveq1	$$⊢q=Q\to q\underset{\dot{}}{·}w=Q\underset{\dot{}}{·}w$$
14	13	oveq1d	$$⊢q=Q\to \left(q\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)=\left(Q\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)$$
15	12 14	eqeq12d	$$⊢q=Q\to \left(\left(q\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(q\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\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)$$
16	15	3anbi3d	$$⊢q=Q\to \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)\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)$$
17		oveq1	$$⊢q=Q\to q\underset{\dot{}}{\times }r=Q\underset{\dot{}}{\times }r$$
18	17	oveq1d	$$⊢q=Q\to \left(q\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=\left(Q\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w$$
19		oveq1	$$⊢q=Q\to q\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)=Q\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)$$
20	18 19	eqeq12d	$$⊢q=Q\to \left(\left(q\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=q\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)\leftrightarrow \left(Q\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=Q\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)\right)$$
21	20	anbi1d	$$⊢q=Q\to \left(\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)\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)$$
22	16 21	anbi12d	$$⊢q=Q\to \left(\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)\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)$$
23	22	2ralbidv	$$⊢q=Q\to \left(\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)\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)$$
24		oveq1	$$⊢r=R\to r\underset{\dot{}}{·}w=R\underset{\dot{}}{·}w$$
25	24	eleq1d	$$⊢r=R\to \left(r\underset{\dot{}}{·}w\in V\leftrightarrow R\underset{\dot{}}{·}w\in V\right)$$
26		oveq1	$$⊢r=R\to r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}x\right)=R\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}x\right)$$
27		oveq1	$$⊢r=R\to r\underset{\dot{}}{·}x=R\underset{\dot{}}{·}x$$
28	24 27	oveq12d	$$⊢r=R\to \left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}x\right)=\left(R\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}x\right)$$
29	26 28	eqeq12d	$$⊢r=R\to \left(r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}x\right)=\left(r\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}x\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)$$
30		oveq2	$$⊢r=R\to Q\underset{\dot{}}{⨣}r=Q\underset{\dot{}}{⨣}R$$
31	30	oveq1d	$$⊢r=R\to \left(Q\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(Q\underset{\dot{}}{⨣}R\right)\underset{\dot{}}{·}w$$
32	24	oveq2d	$$⊢r=R\to \left(Q\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\right)=\left(Q\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}w\right)$$
33	31 32	eqeq12d	$$⊢r=R\to \left(\left(Q\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(Q\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(r\underset{\dot{}}{·}w\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)$$
34	25 29 33	3anbi123d	$$⊢r=R\to \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)\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)$$
35		oveq2	$$⊢r=R\to Q\underset{\dot{}}{\times }r=Q\underset{\dot{}}{\times }R$$
36	35	oveq1d	$$⊢r=R\to \left(Q\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=\left(Q\underset{\dot{}}{\times }R\right)\underset{\dot{}}{·}w$$
37	24	oveq2d	$$⊢r=R\to Q\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)=Q\underset{\dot{}}{·}\left(R\underset{\dot{}}{·}w\right)$$
38	36 37	eqeq12d	$$⊢r=R\to \left(\left(Q\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=Q\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)\leftrightarrow \left(Q\underset{\dot{}}{\times }R\right)\underset{\dot{}}{·}w=Q\underset{\dot{}}{·}\left(R\underset{\dot{}}{·}w\right)\right)$$
39	38	anbi1d	$$⊢r=R\to \left(\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)\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)$$
40	34 39	anbi12d	$$⊢r=R\to \left(\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)\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)$$
41	40	2ralbidv	$$⊢r=R\to \left(\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)\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)$$
42	23 41	rspc2v	$$⊢\left(Q\in K\wedge R\in K\right)\to \left(\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)\to \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)$$
43	10 42	mpan9	$$⊢\left(W\in \mathrm{LMod}\wedge \left(Q\in K\wedge R\in K\right)\right)\to \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)$$
44		oveq2	$$⊢x=X\to w\underset{\dot{}}{+}x=w\underset{\dot{}}{+}X$$
45	44	oveq2d	$$⊢x=X\to R\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}x\right)=R\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}X\right)$$
46		oveq2	$$⊢x=X\to R\underset{\dot{}}{·}x=R\underset{\dot{}}{·}X$$
47	46	oveq2d	$$⊢x=X\to \left(R\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}x\right)=\left(R\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}X\right)$$
48	45 47	eqeq12d	$$⊢x=X\to \left(R\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}x\right)=\left(R\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}x\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)$$
49	48	3anbi2d	$$⊢x=X\to \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)\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)$$
50	49	anbi1d	$$⊢x=X\to \left(\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)\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)$$
51		oveq2	$$⊢w=Y\to R\underset{\dot{}}{·}w=R\underset{\dot{}}{·}Y$$
52	51	eleq1d	$$⊢w=Y\to \left(R\underset{\dot{}}{·}w\in V\leftrightarrow R\underset{\dot{}}{·}Y\in V\right)$$
53		oveq1	$$⊢w=Y\to w\underset{\dot{}}{+}X=Y\underset{\dot{}}{+}X$$
54	53	oveq2d	$$⊢w=Y\to R\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}X\right)=R\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}X\right)$$
55	51	oveq1d	$$⊢w=Y\to \left(R\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}X\right)=\left(R\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}X\right)$$
56	54 55	eqeq12d	$$⊢w=Y\to \left(R\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}X\right)=\left(R\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}X\right)\leftrightarrow R\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}X\right)=\left(R\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}X\right)\right)$$
57		oveq2	$$⊢w=Y\to \left(Q\underset{\dot{}}{⨣}R\right)\underset{\dot{}}{·}w=\left(Q\underset{\dot{}}{⨣}R\right)\underset{\dot{}}{·}Y$$
58		oveq2	$$⊢w=Y\to Q\underset{\dot{}}{·}w=Q\underset{\dot{}}{·}Y$$
59	58 51	oveq12d	$$⊢w=Y\to \left(Q\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}w\right)=\left(Q\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}Y\right)$$
60	57 59	eqeq12d	$$⊢w=Y\to \left(\left(Q\underset{\dot{}}{⨣}R\right)\underset{\dot{}}{·}w=\left(Q\underset{\dot{}}{·}w\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}w\right)\leftrightarrow \left(Q\underset{\dot{}}{⨣}R\right)\underset{\dot{}}{·}Y=\left(Q\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}Y\right)\right)$$
61	52 56 60	3anbi123d	$$⊢w=Y\to \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)\leftrightarrow \left(R\underset{\dot{}}{·}Y\in V\wedge R\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}X\right)=\left(R\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}X\right)\wedge \left(Q\underset{\dot{}}{⨣}R\right)\underset{\dot{}}{·}Y=\left(Q\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}Y\right)\right)\right)$$
62		oveq2	$$⊢w=Y\to \left(Q\underset{\dot{}}{\times }R\right)\underset{\dot{}}{·}w=\left(Q\underset{\dot{}}{\times }R\right)\underset{\dot{}}{·}Y$$
63	51	oveq2d	$$⊢w=Y\to Q\underset{\dot{}}{·}\left(R\underset{\dot{}}{·}w\right)=Q\underset{\dot{}}{·}\left(R\underset{\dot{}}{·}Y\right)$$
64	62 63	eqeq12d	$$⊢w=Y\to \left(\left(Q\underset{\dot{}}{\times }R\right)\underset{\dot{}}{·}w=Q\underset{\dot{}}{·}\left(R\underset{\dot{}}{·}w\right)\leftrightarrow \left(Q\underset{\dot{}}{\times }R\right)\underset{\dot{}}{·}Y=Q\underset{\dot{}}{·}\left(R\underset{\dot{}}{·}Y\right)\right)$$
65		oveq2	$$⊢w=Y\to \underset{\dot{}}{1}\underset{\dot{}}{·}w=\underset{\dot{}}{1}\underset{\dot{}}{·}Y$$
66		id	$$⊢w=Y\to w=Y$$
67	65 66	eqeq12d	$$⊢w=Y\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}w=w\leftrightarrow \underset{\dot{}}{1}\underset{\dot{}}{·}Y=Y\right)$$
68	64 67	anbi12d	$$⊢w=Y\to \left(\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)\leftrightarrow \left(\left(Q\underset{\dot{}}{\times }R\right)\underset{\dot{}}{·}Y=Q\underset{\dot{}}{·}\left(R\underset{\dot{}}{·}Y\right)\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}Y=Y\right)\right)$$
69	61 68	anbi12d	$$⊢w=Y\to \left(\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)\leftrightarrow \left(\left(R\underset{\dot{}}{·}Y\in V\wedge R\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}X\right)=\left(R\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}X\right)\wedge \left(Q\underset{\dot{}}{⨣}R\right)\underset{\dot{}}{·}Y=\left(Q\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}Y\right)\right)\wedge \left(\left(Q\underset{\dot{}}{\times }R\right)\underset{\dot{}}{·}Y=Q\underset{\dot{}}{·}\left(R\underset{\dot{}}{·}Y\right)\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}Y=Y\right)\right)\right)$$
70	50 69	rspc2v	$$⊢\left(X\in V\wedge Y\in V\right)\to \left(\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)\to \left(\left(R\underset{\dot{}}{·}Y\in V\wedge R\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}X\right)=\left(R\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}X\right)\wedge \left(Q\underset{\dot{}}{⨣}R\right)\underset{\dot{}}{·}Y=\left(Q\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}Y\right)\right)\wedge \left(\left(Q\underset{\dot{}}{\times }R\right)\underset{\dot{}}{·}Y=Q\underset{\dot{}}{·}\left(R\underset{\dot{}}{·}Y\right)\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}Y=Y\right)\right)\right)$$
71	43 70	syl5com	$$⊢\left(W\in \mathrm{LMod}\wedge \left(Q\in K\wedge R\in K\right)\right)\to \left(\left(X\in V\wedge Y\in V\right)\to \left(\left(R\underset{\dot{}}{·}Y\in V\wedge R\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}X\right)=\left(R\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}X\right)\wedge \left(Q\underset{\dot{}}{⨣}R\right)\underset{\dot{}}{·}Y=\left(Q\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}Y\right)\right)\wedge \left(\left(Q\underset{\dot{}}{\times }R\right)\underset{\dot{}}{·}Y=Q\underset{\dot{}}{·}\left(R\underset{\dot{}}{·}Y\right)\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}Y=Y\right)\right)\right)$$
72	71	3impia	$$⊢\left(W\in \mathrm{LMod}\wedge \left(Q\in K\wedge R\in K\right)\wedge \left(X\in V\wedge Y\in V\right)\right)\to \left(\left(R\underset{\dot{}}{·}Y\in V\wedge R\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}X\right)=\left(R\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}X\right)\wedge \left(Q\underset{\dot{}}{⨣}R\right)\underset{\dot{}}{·}Y=\left(Q\underset{\dot{}}{·}Y\right)\underset{\dot{}}{+}\left(R\underset{\dot{}}{·}Y\right)\right)\wedge \left(\left(Q\underset{\dot{}}{\times }R\right)\underset{\dot{}}{·}Y=Q\underset{\dot{}}{·}\left(R\underset{\dot{}}{·}Y\right)\wedge \underset{\dot{}}{1}\underset{\dot{}}{·}Y=Y\right)\right)$$