Theorem lcfrlem9

Description: Lemma for lcf1o . (This part has undesirable $d's on J and ph that we remove in lcf1o .) TODO: ugly proof; maybe have better subtheorems or abbreviate some iota_ k expansions with Jz ? TODO: Some redundant $d's? (Contributed by NM, 22-Feb-2015)

	Ref	Expression
Hypotheses	lcf1o.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
	lcf1o.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
	lcf1o.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
	lcf1o.v	$$⊢V={\mathrm{Base}}_U$$
	lcf1o.a	$$⊢\underset{\dot{}}{+}={+}_U$$
	lcf1o.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
	lcf1o.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
	lcf1o.r	$$⊢R={\mathrm{Base}}_S$$
	lcf1o.z	$$⊢\underset{\dot{}}{0}=0_U$$
	lcf1o.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
	lcf1o.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
	lcf1o.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
	lcf1o.q	$$⊢Q=0_D$$
	lcf1o.c	$$⊢C=\left\{f\in F|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}$$
	lcf1o.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)$$
	lcflo.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
Assertion	lcfrlem9	$$⊢\phi \to J:V\setminus \left\{\underset{\dot{}}{0}\right\}\underset{1-1\; onto}{⟶}C\setminus \left\{Q\right\}$$

Proof

Step	Hyp	Ref	Expression
1		lcf1o.h	$$⊢H=\mathrm{LHyp}\left(K\right)$$
2		lcf1o.o	$$⊢\underset{\dot{}}{\perp }=\mathrm{ocH}\left(K\right)\left(W\right)$$
3		lcf1o.u	$$⊢U=\mathrm{DVecH}\left(K\right)\left(W\right)$$
4		lcf1o.v	$$⊢V={\mathrm{Base}}_U$$
5		lcf1o.a	$$⊢\underset{\dot{}}{+}={+}_U$$
6		lcf1o.t	$$⊢\underset{\dot{}}{·}={\cdot }_U$$
7		lcf1o.s	$$⊢S=\mathrm{Scalar}\left(U\right)$$
8		lcf1o.r	$$⊢R={\mathrm{Base}}_S$$
9		lcf1o.z	$$⊢\underset{\dot{}}{0}=0_U$$
10		lcf1o.f	$$⊢F=\mathrm{LFnl}\left(U\right)$$
11		lcf1o.l	$$⊢L=\mathrm{LKer}\left(U\right)$$
12		lcf1o.d	$$⊢D=\mathrm{LDual}\left(U\right)$$
13		lcf1o.q	$$⊢Q=0_D$$
14		lcf1o.c	$$⊢C=\left\{f\in F|\underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(f\right)\right)\right)=L\left(f\right)\right\}$$
15		lcf1o.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)$$
16		lcflo.k	$$⊢\phi \to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
17	4	fvexi	$$⊢V\in \mathrm{V}$$
18	17	mptex	$$⊢\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)\in \mathrm{V}$$
19	18 15	fnmpti	$$⊢JFn\left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
20	19	a1i	$$⊢\phi \to JFn\left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
21		fvelrnb	$$⊢JFn\left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to \left(g\in \mathrm{ran}J\leftrightarrow \exists z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)J\left(z\right)=g\right)$$
22	20 21	syl	$$⊢\phi \to \left(g\in \mathrm{ran}J\leftrightarrow \exists z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)J\left(z\right)=g\right)$$
23	16	adantr	$$⊢\left(\phi \wedge z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
24		simpr	$$⊢\left(\phi \wedge z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
25	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 23 24	lcfrlem8	$$⊢\left(\phi \wedge z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to J\left(z\right)=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)$$
26		eqid	$$⊢\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)$$
27		sneq	$$⊢y=z\to \left\{y\right\}=\left\{z\right\}$$
28	27	fveq2d	$$⊢y=z\to \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)=\underset{\dot{}}{\perp }\left(\left\{z\right\}\right)$$
29		oveq2	$$⊢y=z\to k\underset{\dot{}}{·}y=k\underset{\dot{}}{·}z$$
30	29	oveq2d	$$⊢y=z\to w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)$$
31	30	eqeq2d	$$⊢y=z\to \left(v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\leftrightarrow v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)$$
32	28 31	rexeqbidv	$$⊢y=z\to \left(\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\leftrightarrow \exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)$$
33	32	riotabidv	$$⊢y=z\to \left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)=\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)$$
34	33	mpteq2dv	$$⊢y=z\to \left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)\right)=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)$$
35	34	rspceeqv	$$⊢\left(z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge \left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)\right)\to \exists y\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\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)\right)$$
36	24 26 35	sylancl	$$⊢\left(\phi \wedge z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \exists y\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\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)\right)$$
37	36	olcd	$$⊢\left(\phi \wedge z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \left(L\left(\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)\right)=V\vee \exists y\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\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)\right)\right)$$
38	1 2 3 4 9 5 6 10 7 8 26 23 24	dochflcl	$$⊢\left(\phi \wedge z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)\in F$$
39	1 2 3 4 5 6 7 8 9 10 11 14 23 38	lcfl6	$$⊢\left(\phi \wedge z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \left(\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)\in C\leftrightarrow \left(L\left(\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)\right)=V\vee \exists y\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\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{y\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}y\right)\right)\right)\right)\right)$$
40	37 39	mpbird	$$⊢\left(\phi \wedge z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)\in C$$
41	1 2 3 4 9 5 6 11 7 8 26 23 24	dochsnkr2cl	$$⊢\left(\phi \wedge z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to z\in \left(\underset{\dot{}}{\perp }\left(L\left(\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)\right)\right)\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
42	1 2 3 4 9 10 11 23 38 41	dochsnkrlem3	$$⊢\left(\phi \wedge z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)\right)\right)\right)=L\left(\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)\right)$$
43	1 2 3 4 9 10 11 23 38 41	dochsnkrlem1	$$⊢\left(\phi \wedge z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)\right)\right)\right)\ne V$$
44	42 43	eqnetrrd	$$⊢\left(\phi \wedge z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to L\left(\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)\right)\ne V$$
45	1 3 16	dvhlmod	$$⊢\phi \to U\in \mathrm{LMod}$$
46	45	adantr	$$⊢\left(\phi \wedge z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to U\in \mathrm{LMod}$$
47	4 10 11 12 13 46 38	lkr0f2	$$⊢\left(\phi \wedge z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \left(L\left(\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)\right)=V\leftrightarrow \left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)=Q\right)$$
48	47	necon3bid	$$⊢\left(\phi \wedge z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \left(L\left(\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)\right)\ne V\leftrightarrow \left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)\ne Q\right)$$
49	44 48	mpbid	$$⊢\left(\phi \wedge z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)\ne Q$$
50		eldifsn	$$⊢\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)\in \left(C\setminus \left\{Q\right\}\right)\leftrightarrow \left(\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)\in C\wedge \left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)\ne Q\right)$$
51	40 49 50	sylanbrc	$$⊢\left(\phi \wedge z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)\in \left(C\setminus \left\{Q\right\}\right)$$
52	25 51	eqeltrd	$$⊢\left(\phi \wedge z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to J\left(z\right)\in \left(C\setminus \left\{Q\right\}\right)$$
53		eleq1	$$⊢J\left(z\right)=g\to \left(J\left(z\right)\in \left(C\setminus \left\{Q\right\}\right)\leftrightarrow g\in \left(C\setminus \left\{Q\right\}\right)\right)$$
54	52 53	syl5ibcom	$$⊢\left(\phi \wedge z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \left(J\left(z\right)=g\to g\in \left(C\setminus \left\{Q\right\}\right)\right)$$
55	54	rexlimdva	$$⊢\phi \to \left(\exists z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)J\left(z\right)=g\to g\in \left(C\setminus \left\{Q\right\}\right)\right)$$
56		eldifsn	$$⊢g\in \left(C\setminus \left\{Q\right\}\right)\leftrightarrow \left(g\in C\wedge g\ne Q\right)$$
57		simprl	$$⊢\left(\phi \wedge \left(g\in C\wedge g\ne Q\right)\right)\to g\in C$$
58	45	adantr	$$⊢\left(\phi \wedge g\in C\right)\to U\in \mathrm{LMod}$$
59	14	lcfl1lem	$$⊢g\in C\leftrightarrow \left(g\in F\wedge \underset{\dot{}}{\perp }\left(\underset{\dot{}}{\perp }\left(L\left(g\right)\right)\right)=L\left(g\right)\right)$$
60	59	simplbi	$$⊢g\in C\to g\in F$$
61	60	adantl	$$⊢\left(\phi \wedge g\in C\right)\to g\in F$$
62	4 10 11 12 13 58 61	lkr0f2	$$⊢\left(\phi \wedge g\in C\right)\to \left(L\left(g\right)=V\leftrightarrow g=Q\right)$$
63	62	necon3bid	$$⊢\left(\phi \wedge g\in C\right)\to \left(L\left(g\right)\ne V\leftrightarrow g\ne Q\right)$$
64	63	biimprd	$$⊢\left(\phi \wedge g\in C\right)\to \left(g\ne Q\to L\left(g\right)\ne V\right)$$
65	64	impr	$$⊢\left(\phi \wedge \left(g\in C\wedge g\ne Q\right)\right)\to L\left(g\right)\ne V$$
66	65	neneqd	$$⊢\left(\phi \wedge \left(g\in C\wedge g\ne Q\right)\right)\to \neg L\left(g\right)=V$$
67	16	adantr	$$⊢\left(\phi \wedge \left(g\in C\wedge g\ne Q\right)\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
68	60	adantr	$$⊢\left(g\in C\wedge g\ne Q\right)\to g\in F$$
69	68	adantl	$$⊢\left(\phi \wedge \left(g\in C\wedge g\ne Q\right)\right)\to g\in F$$
70	1 2 3 4 5 6 7 8 9 10 11 14 67 69	lcfl6	$$⊢\left(\phi \wedge \left(g\in C\wedge g\ne Q\right)\right)\to \left(g\in C\leftrightarrow \left(L\left(g\right)=V\vee \exists z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)g=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)\right)\right)$$
71	70	biimpa	$$⊢\left(\left(\phi \wedge \left(g\in C\wedge g\ne Q\right)\right)\wedge g\in C\right)\to \left(L\left(g\right)=V\vee \exists z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)g=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)\right)$$
72	71	ord	$$⊢\left(\left(\phi \wedge \left(g\in C\wedge g\ne Q\right)\right)\wedge g\in C\right)\to \left(\neg L\left(g\right)=V\to \exists z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)g=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)\right)$$
73	72	3impia	$$⊢\left(\left(\phi \wedge \left(g\in C\wedge g\ne Q\right)\right)\wedge g\in C\wedge \neg L\left(g\right)=V\right)\to \exists z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)g=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)$$
74	57 66 73	mpd3an23	$$⊢\left(\phi \wedge \left(g\in C\wedge g\ne Q\right)\right)\to \exists z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)g=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)$$
75	56 74	sylan2b	$$⊢\left(\phi \wedge g\in \left(C\setminus \left\{Q\right\}\right)\right)\to \exists z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)g=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)$$
76		eqcom	$$⊢J\left(z\right)=g\leftrightarrow g=J\left(z\right)$$
77	16	ad2antrr	$$⊢\left(\left(\phi \wedge g\in \left(C\setminus \left\{Q\right\}\right)\right)\wedge z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
78		simpr	$$⊢\left(\left(\phi \wedge g\in \left(C\setminus \left\{Q\right\}\right)\right)\wedge z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
79	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 77 78	lcfrlem8	$$⊢\left(\left(\phi \wedge g\in \left(C\setminus \left\{Q\right\}\right)\right)\wedge z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to J\left(z\right)=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)$$
80	79	eqeq2d	$$⊢\left(\left(\phi \wedge g\in \left(C\setminus \left\{Q\right\}\right)\right)\wedge z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \left(g=J\left(z\right)\leftrightarrow g=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)\right)$$
81	76 80	syl5bb	$$⊢\left(\left(\phi \wedge g\in \left(C\setminus \left\{Q\right\}\right)\right)\wedge z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\to \left(J\left(z\right)=g\leftrightarrow g=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)\right)$$
82	81	rexbidva	$$⊢\left(\phi \wedge g\in \left(C\setminus \left\{Q\right\}\right)\right)\to \left(\exists z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)J\left(z\right)=g\leftrightarrow \exists z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)g=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{z\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}z\right)\right)\right)\right)$$
83	75 82	mpbird	$$⊢\left(\phi \wedge g\in \left(C\setminus \left\{Q\right\}\right)\right)\to \exists z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)J\left(z\right)=g$$
84	83	ex	$$⊢\phi \to \left(g\in \left(C\setminus \left\{Q\right\}\right)\to \exists z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)J\left(z\right)=g\right)$$
85	55 84	impbid	$$⊢\phi \to \left(\exists z\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)J\left(z\right)=g\leftrightarrow g\in \left(C\setminus \left\{Q\right\}\right)\right)$$
86	22 85	bitrd	$$⊢\phi \to \left(g\in \mathrm{ran}J\leftrightarrow g\in \left(C\setminus \left\{Q\right\}\right)\right)$$
87	86	eqrdv	$$⊢\phi \to \mathrm{ran}J=C\setminus \left\{Q\right\}$$
88	16	ad2antrr	$$⊢\left(\left(\phi \wedge \left(t\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge u\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)\wedge J\left(t\right)=J\left(u\right)\right)\to \left(K\in \mathrm{HL}\wedge W\in H\right)$$
89		eqid	$$⊢\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{t\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}t\right)\right)\right)=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{t\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}t\right)\right)\right)$$
90		eqid	$$⊢\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{u\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}u\right)\right)\right)=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{u\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}u\right)\right)\right)$$
91		simplrl	$$⊢\left(\left(\phi \wedge \left(t\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge u\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)\wedge J\left(t\right)=J\left(u\right)\right)\to t\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
92		simplrr	$$⊢\left(\left(\phi \wedge \left(t\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge u\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)\wedge J\left(t\right)=J\left(u\right)\right)\to u\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
93		simpr	$$⊢\left(\left(\phi \wedge \left(t\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge u\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)\wedge J\left(t\right)=J\left(u\right)\right)\to J\left(t\right)=J\left(u\right)$$
94	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 88 91	lcfrlem8	$$⊢\left(\left(\phi \wedge \left(t\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge u\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)\wedge J\left(t\right)=J\left(u\right)\right)\to J\left(t\right)=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{t\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}t\right)\right)\right)$$
95	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 88 92	lcfrlem8	$$⊢\left(\left(\phi \wedge \left(t\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge u\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)\wedge J\left(t\right)=J\left(u\right)\right)\to J\left(u\right)=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{u\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}u\right)\right)\right)$$
96	93 94 95	3eqtr3d	$$⊢\left(\left(\phi \wedge \left(t\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge u\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)\wedge J\left(t\right)=J\left(u\right)\right)\to \left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{t\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}t\right)\right)\right)=\left(v\in V⟼\left(\iota k\in R|\exists w\in \underset{\dot{}}{\perp }\left(\left\{u\right\}\right)v=w\underset{\dot{}}{+}\left(k\underset{\dot{}}{·}u\right)\right)\right)$$
97	1 2 3 4 5 6 7 8 9 10 11 88 89 90 91 92 96	lcfl7lem	$$⊢\left(\left(\phi \wedge \left(t\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge u\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)\wedge J\left(t\right)=J\left(u\right)\right)\to t=u$$
98	97	ex	$$⊢\left(\phi \wedge \left(t\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge u\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\right)\right)\to \left(J\left(t\right)=J\left(u\right)\to t=u\right)$$
99	98	ralrimivva	$$⊢\phi \to \forall t\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\forall u\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\left(J\left(t\right)=J\left(u\right)\to t=u\right)$$
100		dff1o6	$$⊢J:V\setminus \left\{\underset{\dot{}}{0}\right\}\underset{1-1\; onto}{⟶}C\setminus \left\{Q\right\}\leftrightarrow \left(JFn\left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\wedge \mathrm{ran}J=C\setminus \left\{Q\right\}\wedge \forall t\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\forall u\in \left(V\setminus \left\{\underset{\dot{}}{0}\right\}\right)\left(J\left(t\right)=J\left(u\right)\to t=u\right)\right)$$
101	20 87 99 100	syl3anbrc	$$⊢\phi \to J:V\setminus \left\{\underset{\dot{}}{0}\right\}\underset{1-1\; onto}{⟶}C\setminus \left\{Q\right\}$$