Metamath Proof Explorer

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 syl5bi ⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) → ( ( 𝐿 ‘ 𝐺 ) ≠ 𝑉 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ) )
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 syl5bir ⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) → ( ¬ ( 𝐿 ‘ 𝐺 ) = 𝑉 → ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) )
41 40 orrd ⊢ ( ( 𝜑 ∧ 𝐺 ∈ 𝐶 ) → ( ( 𝐿 ‘ 𝐺 ) = 𝑉 ∨ ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) )
42 41 ex ⊢ ( 𝜑 → ( 𝐺 ∈ 𝐶 → ( ( 𝐿 ‘ 𝐺 ) = 𝑉 ∨ ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) ) )
43 olc ⊢ ( ( 𝐿 ‘ 𝐺 ) = 𝑉 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ∨ ( 𝐿 ‘ 𝐺 ) = 𝑉 ) )
44 43 19 syl5ibr ⊢ ( 𝜑 → ( ( 𝐿 ‘ 𝐺 ) = 𝑉 → 𝐺 ∈ 𝐶 ) )
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 } ) 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) ) )