Theorem slmdlema

Description: Lemma for properties of a semimodule. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014) (Revised by Thierry Arnoux, 1-Apr-2018)

	Ref	Expression
Hypotheses	isslmd.v	$$⊢V={\mathrm{Base}}_W$$
	isslmd.a	$$⊢\underset{\dot{}}{+}={+}_W$$
	isslmd.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	isslmd.0	$$⊢\underset{\dot{}}{0}=0_W$$
	isslmd.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	isslmd.k	$$⊢K={\mathrm{Base}}_F$$
	isslmd.p	$$⊢\underset{\dot{}}{⨣}={+}_F$$
	isslmd.t	$$⊢\underset{\dot{}}{\times }={\cdot }_F$$
	isslmd.u	$$⊢\underset{\dot{}}{1}=1_F$$
	isslmd.o	$$⊢O=0_F$$
Assertion	slmdlema	$$⊢\left(W\in \mathrm{SLMod}\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\wedge O\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		isslmd.v	$$⊢V={\mathrm{Base}}_W$$
2		isslmd.a	$$⊢\underset{\dot{}}{+}={+}_W$$
3		isslmd.s	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
4		isslmd.0	$$⊢\underset{\dot{}}{0}=0_W$$
5		isslmd.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
6		isslmd.k	$$⊢K={\mathrm{Base}}_F$$
7		isslmd.p	$$⊢\underset{\dot{}}{⨣}={+}_F$$
8		isslmd.t	$$⊢\underset{\dot{}}{\times }={\cdot }_F$$
9		isslmd.u	$$⊢\underset{\dot{}}{1}=1_F$$
10		isslmd.o	$$⊢O=0_F$$
11	1 2 3 4 5 6 7 8 9 10	isslmd	$$⊢W\in \mathrm{SLMod}\leftrightarrow \left(W\in \mathrm{CMnd}\wedge F\in \mathrm{SRing}\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\wedge O\underset{\dot{}}{·}w=\underset{\dot{}}{0}\right)\right)\right)$$
12	11	simp3bi	$$⊢W\in \mathrm{SLMod}\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\wedge O\underset{\dot{}}{·}w=\underset{\dot{}}{0}\right)\right)$$
13		oveq1	$$⊢q=Q\to q\underset{\dot{}}{⨣}r=Q\underset{\dot{}}{⨣}r$$
14	13	oveq1d	$$⊢q=Q\to \left(q\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(Q\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w$$
15		oveq1	$$⊢q=Q\to q\underset{\dot{}}{·}w=Q\underset{\dot{}}{·}w$$
16	15	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)$$
17	14 16	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)$$
18	17	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)$$
19		oveq1	$$⊢q=Q\to q\underset{\dot{}}{\times }r=Q\underset{\dot{}}{\times }r$$
20	19	oveq1d	$$⊢q=Q\to \left(q\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=\left(Q\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w$$
21		oveq1	$$⊢q=Q\to q\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)=Q\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)$$
22	20 21	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)$$
23	22	3anbi1d	$$⊢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\wedge O\underset{\dot{}}{·}w=\underset{\dot{}}{0}\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\wedge O\underset{\dot{}}{·}w=\underset{\dot{}}{0}\right)\right)$$
24	18 23	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\wedge O\underset{\dot{}}{·}w=\underset{\dot{}}{0}\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\wedge O\underset{\dot{}}{·}w=\underset{\dot{}}{0}\right)\right)\right)$$
25	24	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\wedge O\underset{\dot{}}{·}w=\underset{\dot{}}{0}\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\wedge O\underset{\dot{}}{·}w=\underset{\dot{}}{0}\right)\right)\right)$$
26		oveq1	$$⊢r=R\to r\underset{\dot{}}{·}w=R\underset{\dot{}}{·}w$$
27	26	eleq1d	$$⊢r=R\to \left(r\underset{\dot{}}{·}w\in V\leftrightarrow R\underset{\dot{}}{·}w\in V\right)$$
28		oveq1	$$⊢r=R\to r\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}x\right)=R\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}x\right)$$
29		oveq1	$$⊢r=R\to r\underset{\dot{}}{·}x=R\underset{\dot{}}{·}x$$
30	26 29	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)$$
31	28 30	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)$$
32		oveq2	$$⊢r=R\to Q\underset{\dot{}}{⨣}r=Q\underset{\dot{}}{⨣}R$$
33	32	oveq1d	$$⊢r=R\to \left(Q\underset{\dot{}}{⨣}r\right)\underset{\dot{}}{·}w=\left(Q\underset{\dot{}}{⨣}R\right)\underset{\dot{}}{·}w$$
34	26	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)$$
35	33 34	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)$$
36	27 31 35	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)$$
37		oveq2	$$⊢r=R\to Q\underset{\dot{}}{\times }r=Q\underset{\dot{}}{\times }R$$
38	37	oveq1d	$$⊢r=R\to \left(Q\underset{\dot{}}{\times }r\right)\underset{\dot{}}{·}w=\left(Q\underset{\dot{}}{\times }R\right)\underset{\dot{}}{·}w$$
39	26	oveq2d	$$⊢r=R\to Q\underset{\dot{}}{·}\left(r\underset{\dot{}}{·}w\right)=Q\underset{\dot{}}{·}\left(R\underset{\dot{}}{·}w\right)$$
40	38 39	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)$$
41	40	3anbi1d	$$⊢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\wedge O\underset{\dot{}}{·}w=\underset{\dot{}}{0}\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\wedge O\underset{\dot{}}{·}w=\underset{\dot{}}{0}\right)\right)$$
42	36 41	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\wedge O\underset{\dot{}}{·}w=\underset{\dot{}}{0}\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\wedge O\underset{\dot{}}{·}w=\underset{\dot{}}{0}\right)\right)\right)$$
43	42	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\wedge O\underset{\dot{}}{·}w=\underset{\dot{}}{0}\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\wedge O\underset{\dot{}}{·}w=\underset{\dot{}}{0}\right)\right)\right)$$
44	25 43	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\wedge O\underset{\dot{}}{·}w=\underset{\dot{}}{0}\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\wedge O\underset{\dot{}}{·}w=\underset{\dot{}}{0}\right)\right)\right)$$
45	12 44	mpan9	$$⊢\left(W\in \mathrm{SLMod}\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\wedge O\underset{\dot{}}{·}w=\underset{\dot{}}{0}\right)\right)$$
46		oveq2	$$⊢x=X\to w\underset{\dot{}}{+}x=w\underset{\dot{}}{+}X$$
47	46	oveq2d	$$⊢x=X\to R\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}x\right)=R\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}X\right)$$
48		oveq2	$$⊢x=X\to R\underset{\dot{}}{·}x=R\underset{\dot{}}{·}X$$
49	48	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)$$
50	47 49	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)$$
51	50	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)$$
52	51	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\wedge O\underset{\dot{}}{·}w=\underset{\dot{}}{0}\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\wedge O\underset{\dot{}}{·}w=\underset{\dot{}}{0}\right)\right)\right)$$
53		oveq2	$$⊢w=Y\to R\underset{\dot{}}{·}w=R\underset{\dot{}}{·}Y$$
54	53	eleq1d	$$⊢w=Y\to \left(R\underset{\dot{}}{·}w\in V\leftrightarrow R\underset{\dot{}}{·}Y\in V\right)$$
55		oveq1	$$⊢w=Y\to w\underset{\dot{}}{+}X=Y\underset{\dot{}}{+}X$$
56	55	oveq2d	$$⊢w=Y\to R\underset{\dot{}}{·}\left(w\underset{\dot{}}{+}X\right)=R\underset{\dot{}}{·}\left(Y\underset{\dot{}}{+}X\right)$$
57	53	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)$$
58	56 57	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)$$
59		oveq2	$$⊢w=Y\to \left(Q\underset{\dot{}}{⨣}R\right)\underset{\dot{}}{·}w=\left(Q\underset{\dot{}}{⨣}R\right)\underset{\dot{}}{·}Y$$
60		oveq2	$$⊢w=Y\to Q\underset{\dot{}}{·}w=Q\underset{\dot{}}{·}Y$$
61	60 53	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)$$
62	59 61	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)$$
63	54 58 62	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)$$
64		oveq2	$$⊢w=Y\to \left(Q\underset{\dot{}}{\times }R\right)\underset{\dot{}}{·}w=\left(Q\underset{\dot{}}{\times }R\right)\underset{\dot{}}{·}Y$$
65	53	oveq2d	$$⊢w=Y\to Q\underset{\dot{}}{·}\left(R\underset{\dot{}}{·}w\right)=Q\underset{\dot{}}{·}\left(R\underset{\dot{}}{·}Y\right)$$
66	64 65	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)$$
67		oveq2	$$⊢w=Y\to \underset{\dot{}}{1}\underset{\dot{}}{·}w=\underset{\dot{}}{1}\underset{\dot{}}{·}Y$$
68		id	$$⊢w=Y\to w=Y$$
69	67 68	eqeq12d	$$⊢w=Y\to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}w=w\leftrightarrow \underset{\dot{}}{1}\underset{\dot{}}{·}Y=Y\right)$$
70		oveq2	$$⊢w=Y\to O\underset{\dot{}}{·}w=O\underset{\dot{}}{·}Y$$
71	70	eqeq1d	$$⊢w=Y\to \left(O\underset{\dot{}}{·}w=\underset{\dot{}}{0}\leftrightarrow O\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)$$
72	66 69 71	3anbi123d	$$⊢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\wedge O\underset{\dot{}}{·}w=\underset{\dot{}}{0}\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\wedge O\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)\right)$$
73	63 72	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\wedge O\underset{\dot{}}{·}w=\underset{\dot{}}{0}\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\wedge O\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)\right)\right)$$
74	52 73	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\wedge O\underset{\dot{}}{·}w=\underset{\dot{}}{0}\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\wedge O\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)\right)\right)$$
75	45 74	syl5com	$$⊢\left(W\in \mathrm{SLMod}\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\wedge O\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)\right)\right)$$
76	75	3impia	$$⊢\left(W\in \mathrm{SLMod}\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\wedge O\underset{\dot{}}{·}Y=\underset{\dot{}}{0}\right)\right)$$