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	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lcf1o.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	lcf1o.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lcf1o.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	lcf1o.a	⊢ + = ( +g ‘ 𝑈 )
	lcf1o.t	⊢ · = ( ·𝑠 ‘ 𝑈 )
	lcf1o.s	⊢ 𝑆 = ( Scalar ‘ 𝑈 )
	lcf1o.r	⊢ 𝑅 = ( Base ‘ 𝑆 )
	lcf1o.z	⊢ 0 = ( 0g ‘ 𝑈 )
	lcf1o.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	lcf1o.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	lcf1o.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
	lcf1o.q	⊢ 𝑄 = ( 0g ‘ 𝐷 )
	lcf1o.c	⊢ 𝐶 = { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
	lcf1o.j	⊢ 𝐽 = ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) )
	lcflo.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion	lcfrlem9	⊢ ( 𝜑 → 𝐽 : ( 𝑉 ∖ { 0 } ) –1-1-onto→ ( 𝐶 ∖ { 𝑄 } ) )

Proof

Step	Hyp	Ref	Expression
1		lcf1o.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcf1o.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		lcf1o.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		lcf1o.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		lcf1o.a	⊢ + = ( +g ‘ 𝑈 )
6		lcf1o.t	⊢ · = ( ·𝑠 ‘ 𝑈 )
7		lcf1o.s	⊢ 𝑆 = ( Scalar ‘ 𝑈 )
8		lcf1o.r	⊢ 𝑅 = ( Base ‘ 𝑆 )
9		lcf1o.z	⊢ 0 = ( 0g ‘ 𝑈 )
10		lcf1o.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
11		lcf1o.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
12		lcf1o.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
13		lcf1o.q	⊢ 𝑄 = ( 0g ‘ 𝐷 )
14		lcf1o.c	⊢ 𝐶 = { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
15		lcf1o.j	⊢ 𝐽 = ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) )
16		lcflo.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
17	4	fvexi	⊢ 𝑉 ∈ V
18	17	mptex	⊢ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∈ V
19	18 15	fnmpti	⊢ 𝐽 Fn ( 𝑉 ∖ { 0 } )
20	19	a1i	⊢ ( 𝜑 → 𝐽 Fn ( 𝑉 ∖ { 0 } ) )
21		fvelrnb	⊢ ( 𝐽 Fn ( 𝑉 ∖ { 0 } ) → ( 𝑔 ∈ ran 𝐽 ↔ ∃ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ( 𝐽 ‘ 𝑧 ) = 𝑔 ) )
22	20 21	syl	⊢ ( 𝜑 → ( 𝑔 ∈ ran 𝐽 ↔ ∃ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ( 𝐽 ‘ 𝑧 ) = 𝑔 ) )
23	16	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
24		simpr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → 𝑧 ∈ ( 𝑉 ∖ { 0 } ) )
25	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 23 24	lcfrlem8	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝐽 ‘ 𝑧 ) = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) )
26		eqid	⊢ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) )
27		sneq	⊢ ( 𝑦 = 𝑧 → { 𝑦 } = { 𝑧 } )
28	27	fveq2d	⊢ ( 𝑦 = 𝑧 → ( ⊥ ‘ { 𝑦 } ) = ( ⊥ ‘ { 𝑧 } ) )
29		oveq2	⊢ ( 𝑦 = 𝑧 → ( 𝑘 · 𝑦 ) = ( 𝑘 · 𝑧 ) )
30	29	oveq2d	⊢ ( 𝑦 = 𝑧 → ( 𝑤 + ( 𝑘 · 𝑦 ) ) = ( 𝑤 + ( 𝑘 · 𝑧 ) ) )
31	30	eqeq2d	⊢ ( 𝑦 = 𝑧 → ( 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ↔ 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) )
32	28 31	rexeqbidv	⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ↔ ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) )
33	32	riotabidv	⊢ ( 𝑦 = 𝑧 → ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) = ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) )
34	33	mpteq2dv	⊢ ( 𝑦 = 𝑧 → ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) )
35	34	rspceeqv	⊢ ( ( 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ∧ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) ) → ∃ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) )
36	24 26 35	sylancl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ∃ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) )
37	36	olcd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ( 𝐿 ‘ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) ) = 𝑉 ∨ ∃ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) ) )
38	1 2 3 4 9 5 6 10 7 8 26 23 24	dochflcl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) ∈ 𝐹 )
39	1 2 3 4 5 6 7 8 9 10 11 14 23 38	lcfl6	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) ∈ 𝐶 ↔ ( ( 𝐿 ‘ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) ) = 𝑉 ∨ ∃ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) ) ) )
40	37 39	mpbird	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) ∈ 𝐶 )
41	1 2 3 4 9 5 6 11 7 8 26 23 24	dochsnkr2cl	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → 𝑧 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) ) ) ∖ { 0 } ) )
42	1 2 3 4 9 10 11 23 38 41	dochsnkrlem3	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) ) ) ) = ( 𝐿 ‘ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) ) )
43	1 2 3 4 9 10 11 23 38 41	dochsnkrlem1	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) ) ) ) ≠ 𝑉 )
44	42 43	eqnetrrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝐿 ‘ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) ) ≠ 𝑉 )
45	1 3 16	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
46	45	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → 𝑈 ∈ LMod )
47	4 10 11 12 13 46 38	lkr0f2	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ( 𝐿 ‘ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) ) = 𝑉 ↔ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) = 𝑄 ) )
48	47	necon3bid	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ( 𝐿 ‘ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) ) ≠ 𝑉 ↔ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) ≠ 𝑄 ) )
49	44 48	mpbid	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) ≠ 𝑄 )
50		eldifsn	⊢ ( ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) ∈ ( 𝐶 ∖ { 𝑄 } ) ↔ ( ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) ∈ 𝐶 ∧ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) ≠ 𝑄 ) )
51	40 49 50	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) ∈ ( 𝐶 ∖ { 𝑄 } ) )
52	25 51	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝐽 ‘ 𝑧 ) ∈ ( 𝐶 ∖ { 𝑄 } ) )
53		eleq1	⊢ ( ( 𝐽 ‘ 𝑧 ) = 𝑔 → ( ( 𝐽 ‘ 𝑧 ) ∈ ( 𝐶 ∖ { 𝑄 } ) ↔ 𝑔 ∈ ( 𝐶 ∖ { 𝑄 } ) ) )
54	52 53	syl5ibcom	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ( 𝐽 ‘ 𝑧 ) = 𝑔 → 𝑔 ∈ ( 𝐶 ∖ { 𝑄 } ) ) )
55	54	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ( 𝐽 ‘ 𝑧 ) = 𝑔 → 𝑔 ∈ ( 𝐶 ∖ { 𝑄 } ) ) )
56		eldifsn	⊢ ( 𝑔 ∈ ( 𝐶 ∖ { 𝑄 } ) ↔ ( 𝑔 ∈ 𝐶 ∧ 𝑔 ≠ 𝑄 ) )
57		simprl	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐶 ∧ 𝑔 ≠ 𝑄 ) ) → 𝑔 ∈ 𝐶 )
58	45	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐶 ) → 𝑈 ∈ LMod )
59	14	lcfl1lem	⊢ ( 𝑔 ∈ 𝐶 ↔ ( 𝑔 ∈ 𝐹 ∧ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) = ( 𝐿 ‘ 𝑔 ) ) )
60	59	simplbi	⊢ ( 𝑔 ∈ 𝐶 → 𝑔 ∈ 𝐹 )
61	60	adantl	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐶 ) → 𝑔 ∈ 𝐹 )
62	4 10 11 12 13 58 61	lkr0f2	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐶 ) → ( ( 𝐿 ‘ 𝑔 ) = 𝑉 ↔ 𝑔 = 𝑄 ) )
63	62	necon3bid	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐶 ) → ( ( 𝐿 ‘ 𝑔 ) ≠ 𝑉 ↔ 𝑔 ≠ 𝑄 ) )
64	63	biimprd	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐶 ) → ( 𝑔 ≠ 𝑄 → ( 𝐿 ‘ 𝑔 ) ≠ 𝑉 ) )
65	64	impr	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐶 ∧ 𝑔 ≠ 𝑄 ) ) → ( 𝐿 ‘ 𝑔 ) ≠ 𝑉 )
66	65	neneqd	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐶 ∧ 𝑔 ≠ 𝑄 ) ) → ¬ ( 𝐿 ‘ 𝑔 ) = 𝑉 )
67	16	adantr	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐶 ∧ 𝑔 ≠ 𝑄 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
68	60	adantr	⊢ ( ( 𝑔 ∈ 𝐶 ∧ 𝑔 ≠ 𝑄 ) → 𝑔 ∈ 𝐹 )
69	68	adantl	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐶 ∧ 𝑔 ≠ 𝑄 ) ) → 𝑔 ∈ 𝐹 )
70	1 2 3 4 5 6 7 8 9 10 11 14 67 69	lcfl6	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐶 ∧ 𝑔 ≠ 𝑄 ) ) → ( 𝑔 ∈ 𝐶 ↔ ( ( 𝐿 ‘ 𝑔 ) = 𝑉 ∨ ∃ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) 𝑔 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) ) ) )
71	70	biimpa	⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐶 ∧ 𝑔 ≠ 𝑄 ) ) ∧ 𝑔 ∈ 𝐶 ) → ( ( 𝐿 ‘ 𝑔 ) = 𝑉 ∨ ∃ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) 𝑔 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) ) )
72	71	ord	⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐶 ∧ 𝑔 ≠ 𝑄 ) ) ∧ 𝑔 ∈ 𝐶 ) → ( ¬ ( 𝐿 ‘ 𝑔 ) = 𝑉 → ∃ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) 𝑔 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) ) )
73	72	3impia	⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐶 ∧ 𝑔 ≠ 𝑄 ) ) ∧ 𝑔 ∈ 𝐶 ∧ ¬ ( 𝐿 ‘ 𝑔 ) = 𝑉 ) → ∃ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) 𝑔 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) )
74	57 66 73	mpd3an23	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐶 ∧ 𝑔 ≠ 𝑄 ) ) → ∃ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) 𝑔 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) )
75	56 74	sylan2b	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐶 ∖ { 𝑄 } ) ) → ∃ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) 𝑔 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) )
76		eqcom	⊢ ( ( 𝐽 ‘ 𝑧 ) = 𝑔 ↔ 𝑔 = ( 𝐽 ‘ 𝑧 ) )
77	16	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐶 ∖ { 𝑄 } ) ) ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
78		simpr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐶 ∖ { 𝑄 } ) ) ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → 𝑧 ∈ ( 𝑉 ∖ { 0 } ) )
79	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 77 78	lcfrlem8	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐶 ∖ { 𝑄 } ) ) ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝐽 ‘ 𝑧 ) = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) )
80	79	eqeq2d	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐶 ∖ { 𝑄 } ) ) ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝑔 = ( 𝐽 ‘ 𝑧 ) ↔ 𝑔 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) ) )
81	76 80	syl5bb	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐶 ∖ { 𝑄 } ) ) ∧ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ( 𝐽 ‘ 𝑧 ) = 𝑔 ↔ 𝑔 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) ) )
82	81	rexbidva	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐶 ∖ { 𝑄 } ) ) → ( ∃ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ( 𝐽 ‘ 𝑧 ) = 𝑔 ↔ ∃ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) 𝑔 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑧 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑧 ) ) ) ) ) )
83	75 82	mpbird	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐶 ∖ { 𝑄 } ) ) → ∃ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ( 𝐽 ‘ 𝑧 ) = 𝑔 )
84	83	ex	⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝐶 ∖ { 𝑄 } ) → ∃ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ( 𝐽 ‘ 𝑧 ) = 𝑔 ) )
85	55 84	impbid	⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ( 𝑉 ∖ { 0 } ) ( 𝐽 ‘ 𝑧 ) = 𝑔 ↔ 𝑔 ∈ ( 𝐶 ∖ { 𝑄 } ) ) )
86	22 85	bitrd	⊢ ( 𝜑 → ( 𝑔 ∈ ran 𝐽 ↔ 𝑔 ∈ ( 𝐶 ∖ { 𝑄 } ) ) )
87	86	eqrdv	⊢ ( 𝜑 → ran 𝐽 = ( 𝐶 ∖ { 𝑄 } ) )
88	16	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑢 ∈ ( 𝑉 ∖ { 0 } ) ) ) ∧ ( 𝐽 ‘ 𝑡 ) = ( 𝐽 ‘ 𝑢 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
89		eqid	⊢ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑡 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑡 ) ) ) ) = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑡 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑡 ) ) ) )
90		eqid	⊢ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑢 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑢 ) ) ) ) = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑢 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑢 ) ) ) )
91		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑢 ∈ ( 𝑉 ∖ { 0 } ) ) ) ∧ ( 𝐽 ‘ 𝑡 ) = ( 𝐽 ‘ 𝑢 ) ) → 𝑡 ∈ ( 𝑉 ∖ { 0 } ) )
92		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑢 ∈ ( 𝑉 ∖ { 0 } ) ) ) ∧ ( 𝐽 ‘ 𝑡 ) = ( 𝐽 ‘ 𝑢 ) ) → 𝑢 ∈ ( 𝑉 ∖ { 0 } ) )
93		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑢 ∈ ( 𝑉 ∖ { 0 } ) ) ) ∧ ( 𝐽 ‘ 𝑡 ) = ( 𝐽 ‘ 𝑢 ) ) → ( 𝐽 ‘ 𝑡 ) = ( 𝐽 ‘ 𝑢 ) )
94	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 88 91	lcfrlem8	⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑢 ∈ ( 𝑉 ∖ { 0 } ) ) ) ∧ ( 𝐽 ‘ 𝑡 ) = ( 𝐽 ‘ 𝑢 ) ) → ( 𝐽 ‘ 𝑡 ) = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑡 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑡 ) ) ) ) )
95	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 88 92	lcfrlem8	⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑢 ∈ ( 𝑉 ∖ { 0 } ) ) ) ∧ ( 𝐽 ‘ 𝑡 ) = ( 𝐽 ‘ 𝑢 ) ) → ( 𝐽 ‘ 𝑢 ) = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑢 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑢 ) ) ) ) )
96	93 94 95	3eqtr3d	⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑢 ∈ ( 𝑉 ∖ { 0 } ) ) ) ∧ ( 𝐽 ‘ 𝑡 ) = ( 𝐽 ‘ 𝑢 ) ) → ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑡 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑡 ) ) ) ) = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑢 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑢 ) ) ) ) )
97	1 2 3 4 5 6 7 8 9 10 11 88 89 90 91 92 96	lcfl7lem	⊢ ( ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑢 ∈ ( 𝑉 ∖ { 0 } ) ) ) ∧ ( 𝐽 ‘ 𝑡 ) = ( 𝐽 ‘ 𝑢 ) ) → 𝑡 = 𝑢 )
98	97	ex	⊢ ( ( 𝜑 ∧ ( 𝑡 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑢 ∈ ( 𝑉 ∖ { 0 } ) ) ) → ( ( 𝐽 ‘ 𝑡 ) = ( 𝐽 ‘ 𝑢 ) → 𝑡 = 𝑢 ) )
99	98	ralrimivva	⊢ ( 𝜑 → ∀ 𝑡 ∈ ( 𝑉 ∖ { 0 } ) ∀ 𝑢 ∈ ( 𝑉 ∖ { 0 } ) ( ( 𝐽 ‘ 𝑡 ) = ( 𝐽 ‘ 𝑢 ) → 𝑡 = 𝑢 ) )
100		dff1o6	⊢ ( 𝐽 : ( 𝑉 ∖ { 0 } ) –1-1-onto→ ( 𝐶 ∖ { 𝑄 } ) ↔ ( 𝐽 Fn ( 𝑉 ∖ { 0 } ) ∧ ran 𝐽 = ( 𝐶 ∖ { 𝑄 } ) ∧ ∀ 𝑡 ∈ ( 𝑉 ∖ { 0 } ) ∀ 𝑢 ∈ ( 𝑉 ∖ { 0 } ) ( ( 𝐽 ‘ 𝑡 ) = ( 𝐽 ‘ 𝑢 ) → 𝑡 = 𝑢 ) ) )
101	20 87 99 100	syl3anbrc	⊢ ( 𝜑 → 𝐽 : ( 𝑉 ∖ { 0 } ) –1-1-onto→ ( 𝐶 ∖ { 𝑄 } ) )