Theorem lcfrlem31

Description: Lemma for lcfr . (Contributed by NM, 10-Mar-2015)

	Ref	Expression
Hypotheses	lcfrlem17.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lcfrlem17.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
	lcfrlem17.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lcfrlem17.v	$$⊢V={\mathrm{Base}}_U$$
	lcfrlem17.p	$$⊢\underset{\dot{}}{+}={+}_U$$
	lcfrlem17.z	$$⊢\underset{\dot{}}{0}=0_U$$
	lcfrlem17.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
	lcfrlem17.a	$$⊢A=\mathrm{LSAtoms}\left(U\right)$$
	lcfrlem17.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
	lcfrlem17.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	lcfrlem17.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	lcfrlem17.ne	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
	lcfrlem22.b	$$⊢B=N\left(\left\{X,Y\right\}\right)\cap \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)$$
	lcfrlem24.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
	lcfrlem24.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
	lcfrlem24.q	$$⊢Q=0_S$$
	lcfrlem24.r	$$⊢R={\mathrm{Base}}_S$$
	lcfrlem24.j	$$⊢J=\left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\right)$$
	lcfrlem24.ib	$$⊢\phi \to I\in B$$
	lcfrlem24.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
	lcfrlem25.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
	lcfrlem28.jn	$$⊢\phi \to J\left(Y\right)\left(I\right)\ne Q$$
	lcfrlem29.i	$$⊢F={inv}_r\left(S\right)$$
	lcfrlem30.m	$$⊢\underset{\dot{}}{-}={-}_D$$
	lcfrlem30.c	$$⊢C=J\left(X\right)\underset{\dot{}}{-}\left(\left(F\left(J\left(Y\right)\left(I\right)\right){\cdot }_{S}J\left(X\right)\left(I\right)\right){\cdot }_{D}J\left(Y\right)\right)$$
	lcfrlem31.xi	$$⊢\phi \to J\left(X\right)\left(I\right)\ne Q$$
	lcfrlem31.cn	$$⊢\phi \to C=0_D$$
Assertion	lcfrlem31	$$⊢\phi \to N\left(\left\{X\right\}\right)=N\left(\left\{Y\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		lcfrlem17.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lcfrlem17.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		lcfrlem17.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		lcfrlem17.v	$$⊢V={\mathrm{Base}}_U$$
5		lcfrlem17.p	$$⊢\underset{\dot{}}{+}={+}_U$$
6		lcfrlem17.z	$$⊢\underset{\dot{}}{0}=0_U$$
7		lcfrlem17.n	$$⊢N=\mathrm{LSpan}\left(U\right)$$
8		lcfrlem17.a	$$⊢A=\mathrm{LSAtoms}\left(U\right)$$
9		lcfrlem17.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
10		lcfrlem17.x	$$⊢\phi \to X\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
11		lcfrlem17.y	$$⊢\phi \to Y\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
12		lcfrlem17.ne	$$⊢\phi \to N\left(\left\{X\right\}\right)\ne N\left(\left\{Y\right\}\right)$$
13		lcfrlem22.b	$$⊢B=N\left(\left\{X,Y\right\}\right)\cap \underset{\dot{}}{\perp }\left(\left\{X\underset{\dot{}}{+}Y\right\}\right)$$
14		lcfrlem24.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
15		lcfrlem24.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
16		lcfrlem24.q	$$⊢Q=0_S$$
17		lcfrlem24.r	$$⊢R={\mathrm{Base}}_S$$
18		lcfrlem24.j	$$⊢J=\left(x\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)⟼\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{x\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}x\right)\right)\right)\right)$$
19		lcfrlem24.ib	$$⊢\phi \to I\in B$$
20		lcfrlem24.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
21		lcfrlem25.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
22		lcfrlem28.jn	$$⊢\phi \to J\left(Y\right)\left(I\right)\ne Q$$
23		lcfrlem29.i	$$⊢F={inv}_r\left(S\right)$$
24		lcfrlem30.m	$$⊢\underset{\dot{}}{-}={-}_D$$
25		lcfrlem30.c	$$⊢C=J\left(X\right)\underset{\dot{}}{-}\left(\left(F\left(J\left(Y\right)\left(I\right)\right){\cdot }_{S}J\left(X\right)\left(I\right)\right){\cdot }_{D}J\left(Y\right)\right)$$
26		lcfrlem31.xi	$$⊢\phi \to J\left(X\right)\left(I\right)\ne Q$$
27		lcfrlem31.cn	$$⊢\phi \to C=0_D$$
28	25 27	eqtr3id	$$⊢\phi \to J\left(X\right)\underset{\dot{}}{-}\left(\left(F\left(J\left(Y\right)\left(I\right)\right){\cdot }_{S}J\left(X\right)\left(I\right)\right){\cdot }_{D}J\left(Y\right)\right)=0_D$$
29	1 3 9	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
30	21 29	lduallmod	$$⊢\phi \to D\in \mathrm{LMod}$$
31		eqid	$$⊢\mathrm{LFnl}\left(U\right)=\mathrm{LFnl}\left(U\right)$$
32		eqid	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_D$$
33		eqid	$$⊢0_D=0_D$$
34		eqid	$$⊢\left\{f\in \mathrm{LFnl}\left(U\right)|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}=\left\{f\in \mathrm{LFnl}\left(U\right)|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}$$
35	1 2 3 4 5 14 15 17 6 31 20 21 33 34 18 9 10	lcfrlem10	$$⊢\phi \to J\left(X\right)\in \mathrm{LFnl}\left(U\right)$$
36	31 21 32 29 35	ldualelvbase	$$⊢\phi \to J\left(X\right)\in {\mathrm{Base}}_D$$
37		eqid	$$⊢{\cdot }_D={\cdot }_D$$
38	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23	lcfrlem29	$$⊢\phi \to F\left(J\left(Y\right)\left(I\right)\right){\cdot }_{S}J\left(X\right)\left(I\right)\in R$$
39	1 2 3 4 5 14 15 17 6 31 20 21 33 34 18 9 11	lcfrlem10	$$⊢\phi \to J\left(Y\right)\in \mathrm{LFnl}\left(U\right)$$
40	31 15 17 21 37 29 38 39	ldualvscl	$$⊢\phi \to \left(F\left(J\left(Y\right)\left(I\right)\right){\cdot }_{S}J\left(X\right)\left(I\right)\right){\cdot }_{D}J\left(Y\right)\in \mathrm{LFnl}\left(U\right)$$
41	31 21 32 29 40	ldualelvbase	$$⊢\phi \to \left(F\left(J\left(Y\right)\left(I\right)\right){\cdot }_{S}J\left(X\right)\left(I\right)\right){\cdot }_{D}J\left(Y\right)\in {\mathrm{Base}}_D$$
42	32 33 24	lmodsubeq0	$$⊢\left(D\in \mathrm{LMod}\wedge J\left(X\right)\in {\mathrm{Base}}_D\wedge \left(F\left(J\left(Y\right)\left(I\right)\right){\cdot }_{S}J\left(X\right)\left(I\right)\right){\cdot }_{D}J\left(Y\right)\in {\mathrm{Base}}_D\right)\to \left(J\left(X\right)\underset{\dot{}}{-}\left(\left(F\left(J\left(Y\right)\left(I\right)\right){\cdot }_{S}J\left(X\right)\left(I\right)\right){\cdot }_{D}J\left(Y\right)\right)=0_D\leftrightarrow J\left(X\right)=\left(F\left(J\left(Y\right)\left(I\right)\right){\cdot }_{S}J\left(X\right)\left(I\right)\right){\cdot }_{D}J\left(Y\right)\right)$$
43	30 36 41 42	syl3anc	$$⊢\phi \to \left(J\left(X\right)\underset{\dot{}}{-}\left(\left(F\left(J\left(Y\right)\left(I\right)\right){\cdot }_{S}J\left(X\right)\left(I\right)\right){\cdot }_{D}J\left(Y\right)\right)=0_D\leftrightarrow J\left(X\right)=\left(F\left(J\left(Y\right)\left(I\right)\right){\cdot }_{S}J\left(X\right)\left(I\right)\right){\cdot }_{D}J\left(Y\right)\right)$$
44	28 43	mpbid	$$⊢\phi \to J\left(X\right)=\left(F\left(J\left(Y\right)\left(I\right)\right){\cdot }_{S}J\left(X\right)\left(I\right)\right){\cdot }_{D}J\left(Y\right)$$
45	44	fveq2d	$$⊢\phi \to L\left(J\left(X\right)\right)=L\left(\left(F\left(J\left(Y\right)\left(I\right)\right){\cdot }_{S}J\left(X\right)\left(I\right)\right){\cdot }_{D}J\left(Y\right)\right)$$
46	1 3 9	dvhlvec	$$⊢\phi \to U\in \mathrm{LVec}$$
47	15	lvecdrng	$$⊢U\in \mathrm{LVec}\to S\in \mathrm{DivRing}$$
48	46 47	syl	$$⊢\phi \to S\in \mathrm{DivRing}$$
49	1 2 3 4 5 6 7 8 9 10 11 12 13	lcfrlem22	$$⊢\phi \to B\in A$$
50	4 8 29 49	lsatssv	$$⊢\phi \to B\subseteq V$$
51	50 19	sseldd	$$⊢\phi \to I\in V$$
52	15 17 4 31	lflcl	$$⊢\left(U\in \mathrm{LMod}\wedge J\left(Y\right)\in \mathrm{LFnl}\left(U\right)\wedge I\in V\right)\to J\left(Y\right)\left(I\right)\in R$$
53	29 39 51 52	syl3anc	$$⊢\phi \to J\left(Y\right)\left(I\right)\in R$$
54	17 16 23	drnginvrn0	$$⊢\left(S\in \mathrm{DivRing}\wedge J\left(Y\right)\left(I\right)\in R\wedge J\left(Y\right)\left(I\right)\ne Q\right)\to F\left(J\left(Y\right)\left(I\right)\right)\ne Q$$
55	48 53 22 54	syl3anc	$$⊢\phi \to F\left(J\left(Y\right)\left(I\right)\right)\ne Q$$
56		eqid	$$⊢{\cdot }_S={\cdot }_S$$
57	17 16 23	drnginvrcl	$$⊢\left(S\in \mathrm{DivRing}\wedge J\left(Y\right)\left(I\right)\in R\wedge J\left(Y\right)\left(I\right)\ne Q\right)\to F\left(J\left(Y\right)\left(I\right)\right)\in R$$
58	48 53 22 57	syl3anc	$$⊢\phi \to F\left(J\left(Y\right)\left(I\right)\right)\in R$$
59	15 17 4 31	lflcl	$$⊢\left(U\in \mathrm{LMod}\wedge J\left(X\right)\in \mathrm{LFnl}\left(U\right)\wedge I\in V\right)\to J\left(X\right)\left(I\right)\in R$$
60	29 35 51 59	syl3anc	$$⊢\phi \to J\left(X\right)\left(I\right)\in R$$
61	17 16 56 48 58 60	drngmulne0	$$⊢\phi \to \left(F\left(J\left(Y\right)\left(I\right)\right){\cdot }_{S}J\left(X\right)\left(I\right)\ne Q\leftrightarrow \left(F\left(J\left(Y\right)\left(I\right)\right)\ne Q\wedge J\left(X\right)\left(I\right)\ne Q\right)\right)$$
62	55 26 61	mpbir2and	$$⊢\phi \to F\left(J\left(Y\right)\left(I\right)\right){\cdot }_{S}J\left(X\right)\left(I\right)\ne Q$$
63	15 17 16 31 20 21 37 46 39 38 62	ldualkrsc	$$⊢\phi \to L\left(\left(F\left(J\left(Y\right)\left(I\right)\right){\cdot }_{S}J\left(X\right)\left(I\right)\right){\cdot }_{D}J\left(Y\right)\right)=L\left(J\left(Y\right)\right)$$
64	45 63	eqtrd	$$⊢\phi \to L\left(J\left(X\right)\right)=L\left(J\left(Y\right)\right)$$
65	64	fveq2d	$$⊢\phi \to \underset{\dot{}}{\perp }\left(L\left(J\left(X\right)\right)\right)=\underset{\dot{}}{\perp }\left(L\left(J\left(Y\right)\right)\right)$$
66	1 2 3 4 5 14 15 17 6 31 20 21 33 34 18 9 10 7	lcfrlem14	$$⊢\phi \to \underset{\dot{}}{\perp }\left(L\left(J\left(X\right)\right)\right)=N\left(\left\{X\right\}\right)$$
67	1 2 3 4 5 14 15 17 6 31 20 21 33 34 18 9 11 7	lcfrlem14	$$⊢\phi \to \underset{\dot{}}{\perp }\left(L\left(J\left(Y\right)\right)\right)=N\left(\left\{Y\right\}\right)$$
68	65 66 67	3eqtr3d	$$⊢\phi \to N\left(\left\{X\right\}\right)=N\left(\left\{Y\right\}\right)$$