Theorem lcfrlem3

Description: Lemma for lcfr . (Contributed by NM, 27-Feb-2015)

	Ref	Expression
Hypotheses	lcfrlem1.v	$$⊢V={\mathrm{Base}}_U$$
	lcfrlem1.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
	lcfrlem1.q	$$⊢\underset{\dot{}}{\times }={\cdot }_S$$
	lcfrlem1.z	$$⊢\underset{\dot{}}{0}=0_S$$
	lcfrlem1.i	$$⊢I={inv}_r\left(S\right)$$
	lcfrlem1.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
	lcfrlem1.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
	lcfrlem1.t	$$⊢\underset{\dot{}}{·}={\cdot }_D$$
	lcfrlem1.m	$$⊢\underset{\dot{}}{-}={-}_D$$
	lcfrlem1.u	$$⊢\phi \to U\in \mathrm{LVec}$$
	lcfrlem1.e	$$⊢\phi \to E\in F$$
	lcfrlem1.g	$$⊢\phi \to G\in F$$
	lcfrlem1.x	$$⊢\phi \to X\in V$$
	lcfrlem1.n	$$⊢\phi \to G\left(X\right)\ne \underset{\dot{}}{0}$$
	lcfrlem1.h	$$⊢H=E\underset{\dot{}}{-}\left(\left(I\left(G\left(X\right)\right)\underset{\dot{}}{\times }E\left(X\right)\right)\underset{\dot{}}{·}G\right)$$
	lcfrlem2.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
Assertion	lcfrlem3	$$⊢\phi \to X\in L\left(H\right)$$

Proof

Step	Hyp	Ref	Expression
1		lcfrlem1.v	$$⊢V={\mathrm{Base}}_U$$
2		lcfrlem1.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
3		lcfrlem1.q	$$⊢\underset{\dot{}}{\times }={\cdot }_S$$
4		lcfrlem1.z	$$⊢\underset{\dot{}}{0}=0_S$$
5		lcfrlem1.i	$$⊢I={inv}_r\left(S\right)$$
6		lcfrlem1.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
7		lcfrlem1.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
8		lcfrlem1.t	$$⊢\underset{\dot{}}{·}={\cdot }_D$$
9		lcfrlem1.m	$$⊢\underset{\dot{}}{-}={-}_D$$
10		lcfrlem1.u	$$⊢\phi \to U\in \mathrm{LVec}$$
11		lcfrlem1.e	$$⊢\phi \to E\in F$$
12		lcfrlem1.g	$$⊢\phi \to G\in F$$
13		lcfrlem1.x	$$⊢\phi \to X\in V$$
14		lcfrlem1.n	$$⊢\phi \to G\left(X\right)\ne \underset{\dot{}}{0}$$
15		lcfrlem1.h	$$⊢H=E\underset{\dot{}}{-}\left(\left(I\left(G\left(X\right)\right)\underset{\dot{}}{\times }E\left(X\right)\right)\underset{\dot{}}{·}G\right)$$
16		lcfrlem2.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
17	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	lcfrlem1	$$⊢\phi \to H\left(X\right)=\underset{\dot{}}{0}$$
18		lveclmod	$$⊢U\in \mathrm{LVec}\to U\in \mathrm{LMod}$$
19	10 18	syl	$$⊢\phi \to U\in \mathrm{LMod}$$
20		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
21	2	lmodring	$$⊢U\in \mathrm{LMod}\to S\in \mathrm{Ring}$$
22	19 21	syl	$$⊢\phi \to S\in \mathrm{Ring}$$
23	2	lvecdrng	$$⊢U\in \mathrm{LVec}\to S\in \mathrm{DivRing}$$
24	10 23	syl	$$⊢\phi \to S\in \mathrm{DivRing}$$
25	2 20 1 6	lflcl	$$⊢\left(U\in \mathrm{LVec}\wedge G\in F\wedge X\in V\right)\to G\left(X\right)\in {\mathrm{Base}}_S$$
26	10 12 13 25	syl3anc	$$⊢\phi \to G\left(X\right)\in {\mathrm{Base}}_S$$
27	20 4 5	drnginvrcl	$$⊢\left(S\in \mathrm{DivRing}\wedge G\left(X\right)\in {\mathrm{Base}}_S\wedge G\left(X\right)\ne \underset{\dot{}}{0}\right)\to I\left(G\left(X\right)\right)\in {\mathrm{Base}}_S$$
28	24 26 14 27	syl3anc	$$⊢\phi \to I\left(G\left(X\right)\right)\in {\mathrm{Base}}_S$$
29	2 20 1 6	lflcl	$$⊢\left(U\in \mathrm{LVec}\wedge E\in F\wedge X\in V\right)\to E\left(X\right)\in {\mathrm{Base}}_S$$
30	10 11 13 29	syl3anc	$$⊢\phi \to E\left(X\right)\in {\mathrm{Base}}_S$$
31	20 3	ringcl	$$⊢\left(S\in \mathrm{Ring}\wedge I\left(G\left(X\right)\right)\in {\mathrm{Base}}_S\wedge E\left(X\right)\in {\mathrm{Base}}_S\right)\to I\left(G\left(X\right)\right)\underset{\dot{}}{\times }E\left(X\right)\in {\mathrm{Base}}_S$$
32	22 28 30 31	syl3anc	$$⊢\phi \to I\left(G\left(X\right)\right)\underset{\dot{}}{\times }E\left(X\right)\in {\mathrm{Base}}_S$$
33	6 2 20 7 8 19 32 12	ldualvscl	$$⊢\phi \to \left(I\left(G\left(X\right)\right)\underset{\dot{}}{\times }E\left(X\right)\right)\underset{\dot{}}{·}G\in F$$
34	6 7 9 19 11 33	ldualvsubcl	$$⊢\phi \to E\underset{\dot{}}{-}\left(\left(I\left(G\left(X\right)\right)\underset{\dot{}}{\times }E\left(X\right)\right)\underset{\dot{}}{·}G\right)\in F$$
35	15 34	eqeltrid	$$⊢\phi \to H\in F$$
36	1 2 4 6 16 10 35 13	ellkr2	$$⊢\phi \to \left(X\in L\left(H\right)\leftrightarrow H\left(X\right)=\underset{\dot{}}{0}\right)$$
37	17 36	mpbird	$$⊢\phi \to X\in L\left(H\right)$$