Theorem lcfrlem1

Description: Lemma for lcfr . Note that X is z in Mario's notes. (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)$$
Assertion	lcfrlem1	$$⊢\phi \to H\left(X\right)=\underset{\dot{}}{0}$$

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	15	fveq1i	$$⊢H\left(X\right)=\left(E\underset{\dot{}}{-}\left(\left(I\left(G\left(X\right)\right)\underset{\dot{}}{\times }E\left(X\right)\right)\underset{\dot{}}{·}G\right)\right)\left(X\right)$$
17		eqid	$$⊢{-}_S={-}_S$$
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	lvecdrng	$$⊢U\in \mathrm{LVec}\to S\in \mathrm{DivRing}$$
22	10 21	syl	$$⊢\phi \to S\in \mathrm{DivRing}$$
23	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$$
24	10 12 13 23	syl3anc	$$⊢\phi \to G\left(X\right)\in {\mathrm{Base}}_S$$
25	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$$
26	22 24 14 25	syl3anc	$$⊢\phi \to I\left(G\left(X\right)\right)\in {\mathrm{Base}}_S$$
27	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$$
28	10 11 13 27	syl3anc	$$⊢\phi \to E\left(X\right)\in {\mathrm{Base}}_S$$
29	2 20 3	lmodmcl	$$⊢\left(U\in \mathrm{LMod}\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$$
30	19 26 28 29	syl3anc	$$⊢\phi \to I\left(G\left(X\right)\right)\underset{\dot{}}{\times }E\left(X\right)\in {\mathrm{Base}}_S$$
31	6 2 20 7 8 19 30 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$$
32	1 2 17 6 7 9 19 11 31 13	ldualvsubval	$$⊢\phi \to \left(E\underset{\dot{}}{-}\left(\left(I\left(G\left(X\right)\right)\underset{\dot{}}{\times }E\left(X\right)\right)\underset{\dot{}}{·}G\right)\right)\left(X\right)=E\left(X\right){-}_S\left(\left(I\left(G\left(X\right)\right)\underset{\dot{}}{\times }E\left(X\right)\right)\underset{\dot{}}{·}G\right)\left(X\right)$$
33	6 1 2 20 3 7 8 10 30 12 13	ldualvsval	$$⊢\phi \to \left(\left(I\left(G\left(X\right)\right)\underset{\dot{}}{\times }E\left(X\right)\right)\underset{\dot{}}{·}G\right)\left(X\right)=G\left(X\right)\underset{\dot{}}{\times }\left(I\left(G\left(X\right)\right)\underset{\dot{}}{\times }E\left(X\right)\right)$$
34		eqid	$$⊢1_S=1_S$$
35	20 4 3 34 5	drnginvrr	$$⊢\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 G\left(X\right)\underset{\dot{}}{\times }I\left(G\left(X\right)\right)=1_S$$
36	22 24 14 35	syl3anc	$$⊢\phi \to G\left(X\right)\underset{\dot{}}{\times }I\left(G\left(X\right)\right)=1_S$$
37	36	oveq1d	$$⊢\phi \to \left(G\left(X\right)\underset{\dot{}}{\times }I\left(G\left(X\right)\right)\right)\underset{\dot{}}{\times }E\left(X\right)=1_S\underset{\dot{}}{\times }E\left(X\right)$$
38	2	lmodring	$$⊢U\in \mathrm{LMod}\to S\in \mathrm{Ring}$$
39	19 38	syl	$$⊢\phi \to S\in \mathrm{Ring}$$
40	20 3	ringass	$$⊢\left(S\in \mathrm{Ring}\wedge \left(G\left(X\right)\in {\mathrm{Base}}_S\wedge I\left(G\left(X\right)\right)\in {\mathrm{Base}}_S\wedge E\left(X\right)\in {\mathrm{Base}}_S\right)\right)\to \left(G\left(X\right)\underset{\dot{}}{\times }I\left(G\left(X\right)\right)\right)\underset{\dot{}}{\times }E\left(X\right)=G\left(X\right)\underset{\dot{}}{\times }\left(I\left(G\left(X\right)\right)\underset{\dot{}}{\times }E\left(X\right)\right)$$
41	39 24 26 28 40	syl13anc	$$⊢\phi \to \left(G\left(X\right)\underset{\dot{}}{\times }I\left(G\left(X\right)\right)\right)\underset{\dot{}}{\times }E\left(X\right)=G\left(X\right)\underset{\dot{}}{\times }\left(I\left(G\left(X\right)\right)\underset{\dot{}}{\times }E\left(X\right)\right)$$
42	20 3 34	ringlidm	$$⊢\left(S\in \mathrm{Ring}\wedge E\left(X\right)\in {\mathrm{Base}}_S\right)\to 1_S\underset{\dot{}}{\times }E\left(X\right)=E\left(X\right)$$
43	39 28 42	syl2anc	$$⊢\phi \to 1_S\underset{\dot{}}{\times }E\left(X\right)=E\left(X\right)$$
44	37 41 43	3eqtr3d	$$⊢\phi \to G\left(X\right)\underset{\dot{}}{\times }\left(I\left(G\left(X\right)\right)\underset{\dot{}}{\times }E\left(X\right)\right)=E\left(X\right)$$
45	33 44	eqtrd	$$⊢\phi \to \left(\left(I\left(G\left(X\right)\right)\underset{\dot{}}{\times }E\left(X\right)\right)\underset{\dot{}}{·}G\right)\left(X\right)=E\left(X\right)$$
46	45	oveq2d	$$⊢\phi \to E\left(X\right){-}_S\left(\left(I\left(G\left(X\right)\right)\underset{\dot{}}{\times }E\left(X\right)\right)\underset{\dot{}}{·}G\right)\left(X\right)=E\left(X\right){-}_{S}E\left(X\right)$$
47	2	lmodfgrp	$$⊢U\in \mathrm{LMod}\to S\in \mathrm{Grp}$$
48	19 47	syl	$$⊢\phi \to S\in \mathrm{Grp}$$
49	20 4 17	grpsubid	$$⊢\left(S\in \mathrm{Grp}\wedge E\left(X\right)\in {\mathrm{Base}}_S\right)\to E\left(X\right){-}_{S}E\left(X\right)=\underset{\dot{}}{0}$$
50	48 28 49	syl2anc	$$⊢\phi \to E\left(X\right){-}_{S}E\left(X\right)=\underset{\dot{}}{0}$$
51	32 46 50	3eqtrd	$$⊢\phi \to \left(E\underset{\dot{}}{-}\left(\left(I\left(G\left(X\right)\right)\underset{\dot{}}{\times }E\left(X\right)\right)\underset{\dot{}}{·}G\right)\right)\left(X\right)=\underset{\dot{}}{0}$$
52	16 51	syl5eq	$$⊢\phi \to H\left(X\right)=\underset{\dot{}}{0}$$