Theorem lcfl6

Description: Property of a functional with a closed kernel. Note that ( LG ) = V means the functional is zero by lkr0f . (Contributed by NM, 3-Jan-2015)

	Ref	Expression
Hypotheses	lcfl6.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lcfl6.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	lcfl6.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lcfl6.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	lcfl6.a	⊢ + = ( +g ‘ 𝑈 )
	lcfl6.t	⊢ · = ( ·𝑠 ‘ 𝑈 )
	lcfl6.s	⊢ 𝑆 = ( Scalar ‘ 𝑈 )
	lcfl6.r	⊢ 𝑅 = ( Base ‘ 𝑆 )
	lcfl6.z	⊢ 0 = ( 0g ‘ 𝑈 )
	lcfl6.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	lcfl6.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	lcfl6.c	⊢ 𝐶 = { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
	lcfl6.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	lcfl6.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
Assertion	lcfl6	⊢ ( 𝜑 → ( 𝐺 ∈ 𝐶 ↔ ( ( 𝐿 ‘ 𝐺 ) = 𝑉 ∨ ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		lcfl6.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcfl6.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		lcfl6.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		lcfl6.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		lcfl6.a	⊢ + = ( +g ‘ 𝑈 )
6		lcfl6.t	⊢ · = ( ·𝑠 ‘ 𝑈 )
7		lcfl6.s	⊢ 𝑆 = ( Scalar ‘ 𝑈 )
8		lcfl6.r	⊢ 𝑅 = ( Base ‘ 𝑆 )
9		lcfl6.z	⊢ 0 = ( 0g ‘ 𝑈 )
10		lcfl6.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
11		lcfl6.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
12		lcfl6.c	⊢ 𝐶 = { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
13		lcfl6.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
14		lcfl6.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
15		df-ne	⊢ ( ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ↔ ¬ ( 𝐿 ‘ 𝐺 ) = 𝑉 )
16		eqid	⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
17	13	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
18	14	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) → 𝐺 ∈ 𝐹 )
19	1 2 3 4 10 11 12 13 14	lcfl2	⊢ ( 𝜑 → ( 𝐺 ∈ 𝐶 ↔ ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ∨ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) ) )
20	19	biimpa	⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ∨ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) )
21	20	orcomd	⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) → ( ( 𝐿 ‘ 𝐺 ) = 𝑉 ∨ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ) )
22	21	ord	⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) → ( ¬ ( 𝐿 ‘ 𝐺 ) = 𝑉 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ) )
23	15 22	biimtrid	⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) → ( ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ) )
24	23	imp	⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 )
25	1 2 3 4 7 9 16 10 11 17 18 24	dochkr1	⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) → ∃ 𝑥 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) ( 𝐺 ‘ 𝑥 ) = ( 1r ‘ 𝑆 ) )
26	1 3 13	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
27	4 10 11 26 14	lkrssv	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) ⊆ 𝑉 )
28	1 3 4 2	dochssv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ 𝑉 ) → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ⊆ 𝑉 )
29	13 27 28	syl2anc	⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ⊆ 𝑉 )
30	29	ssdifd	⊢ ( 𝜑 → ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) ⊆ ( 𝑉 ∖ { 0 } ) )
31	30	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) ∧ ( 𝑥 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 1r ‘ 𝑆 ) ) ) → ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) ⊆ ( 𝑉 ∖ { 0 } ) )
32		simprl	⊢ ( ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) ∧ ( 𝑥 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 1r ‘ 𝑆 ) ) ) → 𝑥 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) )
33	31 32	sseldd	⊢ ( ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) ∧ ( 𝑥 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 1r ‘ 𝑆 ) ) ) → 𝑥 ∈ ( 𝑉 ∖ { 0 } ) )
34	13	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) ∧ ( 𝑥 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 1r ‘ 𝑆 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
35	14	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) ∧ ( 𝑥 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 1r ‘ 𝑆 ) ) ) → 𝐺 ∈ 𝐹 )
36		simprr	⊢ ( ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) ∧ ( 𝑥 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 1r ‘ 𝑆 ) ) ) → ( 𝐺 ‘ 𝑥 ) = ( 1r ‘ 𝑆 ) )
37	1 2 3 4 5 6 7 16 8 9 10 11 34 35 32 36	lcfl6lem	⊢ ( ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) ∧ ( 𝑥 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 1r ‘ 𝑆 ) ) ) → 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) )
38	25 33 37	reximssdv	⊢ ( ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) ∧ ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 ) → ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) )
39	38	ex	⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) → ( ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 → ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) )
40	15 39	biimtrrid	⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) → ( ¬ ( 𝐿 ‘ 𝐺 ) = 𝑉 → ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) )
41	40	orrd	⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) → ( ( 𝐿 ‘ 𝐺 ) = 𝑉 ∨ ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) )
42	41	ex	⊢ ( 𝜑 → ( 𝐺 ∈ 𝐶 → ( ( 𝐿 ‘ 𝐺 ) = 𝑉 ∨ ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) ) )
43		olc	⊢ ( ( 𝐿 ‘ 𝐺 ) = 𝑉 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ∨ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) )
44	43 19	imbitrrid	⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐺 ) = 𝑉 → 𝐺 ∈ 𝐶 ) )
45	13	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
46		eldifi	⊢ ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) → 𝑥 ∈ 𝑉 )
47	46	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → 𝑥 ∈ 𝑉 )
48	47	snssd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → { 𝑥 } ⊆ 𝑉 )
49		eqid	⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
50	1 49 3 4 2	dochcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { 𝑥 } ⊆ 𝑉 ) → ( ⊥ ‘ { 𝑥 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
51	45 48 50	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ⊥ ‘ { 𝑥 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
52	1 49 2	dochoc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ { 𝑥 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ { 𝑥 } ) ) ) = ( ⊥ ‘ { 𝑥 } ) )
53	45 51 52	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ { 𝑥 } ) ) ) = ( ⊥ ‘ { 𝑥 } ) )
54	53	3adant3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ { 𝑥 } ) ) ) = ( ⊥ ‘ { 𝑥 } ) )
55		simp3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) → 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) )
56	55	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) → ( 𝐿 ‘ 𝐺 ) = ( 𝐿 ‘ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) )
57		eqid	⊢ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) )
58		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → 𝑥 ∈ ( 𝑉 ∖ { 0 } ) )
59	1 2 3 4 9 5 6 11 7 8 57 45 58	dochsnkr2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝐿 ‘ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) = ( ⊥ ‘ { 𝑥 } ) )
60	59	3adant3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) → ( 𝐿 ‘ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) = ( ⊥ ‘ { 𝑥 } ) )
61	56 60	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) → ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑥 } ) )
62	61	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( ⊥ ‘ ( ⊥ ‘ { 𝑥 } ) ) )
63	62	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ { 𝑥 } ) ) ) )
64	54 63 61	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) )
65	14	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) → 𝐺 ∈ 𝐹 )
66	12 65	lcfl1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) → ( 𝐺 ∈ 𝐶 ↔ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) = ( 𝐿 ‘ 𝐺 ) ) )
67	64 66	mpbird	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) → 𝐺 ∈ 𝐶 )
68	67	rexlimdv3a	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) → 𝐺 ∈ 𝐶 ) )
69	44 68	jaod	⊢ ( 𝜑 → ( ( ( 𝐿 ‘ 𝐺 ) = 𝑉 ∨ ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) → 𝐺 ∈ 𝐶 ) )
70	42 69	impbid	⊢ ( 𝜑 → ( 𝐺 ∈ 𝐶 ↔ ( ( 𝐿 ‘ 𝐺 ) = 𝑉 ∨ ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) ) )