Metamath Proof Explorer

Theorem lcfl7N

Description: Property of a functional with a closed kernel. Every nonzero functional is determined by a unique nonzero vector. Note that ( LG ) = V means the functional is zero by lkr0f . (Contributed by NM, 4-Jan-2015) (New usage is discouraged.)

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 lcfl7N ( 𝜑 → ( 𝐺 ∈ 𝐶 ↔ ( ( 𝐿 ‘ 𝐺 ) = 𝑉 ∨ ∃! 𝑥 ∈ ( 𝑉 ∖ { 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 1 2 3 4 5 6 7 8 9 10 11 12 13 14 lcfl6 ⊢ ( 𝜑 → ( 𝐺 ∈ 𝐶 ↔ ( ( 𝐿 ‘ 𝐺 ) = 𝑉 ∨ ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) ) )
16 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ) ∧ ( 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∧ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
17 eqid ⊢ ( 𝑢 ∈ 𝑉 ↦ ( ℩ 𝑙 ∈ 𝑅 ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) ) ) = ( 𝑢 ∈ 𝑉 ↦ ( ℩ 𝑙 ∈ 𝑅 ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) ) )
18 eqid ⊢ ( 𝑢 ∈ 𝑉 ↦ ( ℩ 𝑙 ∈ 𝑅 ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑦 ) ) ) ) = ( 𝑢 ∈ 𝑉 ↦ ( ℩ 𝑙 ∈ 𝑅 ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑦 ) ) ) )
19 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ) ∧ ( 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∧ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) ) ) → 𝑥 ∈ ( 𝑉 ∖ { 0 } ) )
20 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ) ∧ ( 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∧ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) ) ) → 𝑦 ∈ ( 𝑉 ∖ { 0 } ) )
21 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ) ∧ ( 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∧ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) ) ) → 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) )
22 eqeq1 ⊢ ( 𝑣 = 𝑢 → ( 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ↔ 𝑢 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) )
23 22 rexbidv ⊢ ( 𝑣 = 𝑢 → ( ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ↔ ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑢 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) )
24 23 riotabidv ⊢ ( 𝑣 = 𝑢 → ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) = ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑢 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) )
25 oveq1 ⊢ ( 𝑘 = 𝑙 → ( 𝑘 · 𝑥 ) = ( 𝑙 · 𝑥 ) )
26 25 oveq2d ⊢ ( 𝑘 = 𝑙 → ( 𝑤 + ( 𝑘 · 𝑥 ) ) = ( 𝑤 + ( 𝑙 · 𝑥 ) ) )
27 26 eqeq2d ⊢ ( 𝑘 = 𝑙 → ( 𝑢 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ↔ 𝑢 = ( 𝑤 + ( 𝑙 · 𝑥 ) ) ) )
28 27 rexbidv ⊢ ( 𝑘 = 𝑙 → ( ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑢 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ↔ ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑢 = ( 𝑤 + ( 𝑙 · 𝑥 ) ) ) )
29 oveq1 ⊢ ( 𝑤 = 𝑧 → ( 𝑤 + ( 𝑙 · 𝑥 ) ) = ( 𝑧 + ( 𝑙 · 𝑥 ) ) )
30 29 eqeq2d ⊢ ( 𝑤 = 𝑧 → ( 𝑢 = ( 𝑤 + ( 𝑙 · 𝑥 ) ) ↔ 𝑢 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) ) )
31 30 cbvrexvw ⊢ ( ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑢 = ( 𝑤 + ( 𝑙 · 𝑥 ) ) ↔ ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) )
32 28 31 bitrdi ⊢ ( 𝑘 = 𝑙 → ( ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑢 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ↔ ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) ) )
33 32 cbvriotavw ⊢ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑢 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) = ( ℩ 𝑙 ∈ 𝑅 ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) )
34 24 33 eqtrdi ⊢ ( 𝑣 = 𝑢 → ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) = ( ℩ 𝑙 ∈ 𝑅 ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) ) )
35 34 cbvmptv ⊢ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) = ( 𝑢 ∈ 𝑉 ↦ ( ℩ 𝑙 ∈ 𝑅 ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) ) )
36 21 35 eqtrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ) ∧ ( 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∧ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) ) ) → 𝐺 = ( 𝑢 ∈ 𝑉 ↦ ( ℩ 𝑙 ∈ 𝑅 ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) ) ) )
37 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ) ∧ ( 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∧ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) ) ) → 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) )
38 eqeq1 ⊢ ( 𝑣 = 𝑢 → ( 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ↔ 𝑢 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) )
39 38 rexbidv ⊢ ( 𝑣 = 𝑢 → ( ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ↔ ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑢 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) )
40 39 riotabidv ⊢ ( 𝑣 = 𝑢 → ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) = ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑢 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) )
41 oveq1 ⊢ ( 𝑘 = 𝑙 → ( 𝑘 · 𝑦 ) = ( 𝑙 · 𝑦 ) )
42 41 oveq2d ⊢ ( 𝑘 = 𝑙 → ( 𝑤 + ( 𝑘 · 𝑦 ) ) = ( 𝑤 + ( 𝑙 · 𝑦 ) ) )
43 42 eqeq2d ⊢ ( 𝑘 = 𝑙 → ( 𝑢 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ↔ 𝑢 = ( 𝑤 + ( 𝑙 · 𝑦 ) ) ) )
44 43 rexbidv ⊢ ( 𝑘 = 𝑙 → ( ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑢 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ↔ ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑢 = ( 𝑤 + ( 𝑙 · 𝑦 ) ) ) )
45 oveq1 ⊢ ( 𝑤 = 𝑧 → ( 𝑤 + ( 𝑙 · 𝑦 ) ) = ( 𝑧 + ( 𝑙 · 𝑦 ) ) )
46 45 eqeq2d ⊢ ( 𝑤 = 𝑧 → ( 𝑢 = ( 𝑤 + ( 𝑙 · 𝑦 ) ) ↔ 𝑢 = ( 𝑧 + ( 𝑙 · 𝑦 ) ) ) )
47 46 cbvrexvw ⊢ ( ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑢 = ( 𝑤 + ( 𝑙 · 𝑦 ) ) ↔ ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑦 ) ) )
48 44 47 bitrdi ⊢ ( 𝑘 = 𝑙 → ( ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑢 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ↔ ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑦 ) ) ) )
49 48 cbvriotavw ⊢ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑢 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) = ( ℩ 𝑙 ∈ 𝑅 ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑦 ) ) )
50 40 49 eqtrdi ⊢ ( 𝑣 = 𝑢 → ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) = ( ℩ 𝑙 ∈ 𝑅 ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑦 ) ) ) )
51 50 cbvmptv ⊢ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) = ( 𝑢 ∈ 𝑉 ↦ ( ℩ 𝑙 ∈ 𝑅 ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑦 ) ) ) )
52 37 51 eqtrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ) ∧ ( 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∧ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) ) ) → 𝐺 = ( 𝑢 ∈ 𝑉 ↦ ( ℩ 𝑙 ∈ 𝑅 ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑦 ) ) ) ) )
53 36 52 eqtr3d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ) ∧ ( 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∧ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) ) ) → ( 𝑢 ∈ 𝑉 ↦ ( ℩ 𝑙 ∈ 𝑅 ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) ) ) = ( 𝑢 ∈ 𝑉 ↦ ( ℩ 𝑙 ∈ 𝑅 ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑦 ) ) ) ) )
54 1 2 3 4 5 6 7 8 9 10 11 16 17 18 19 20 53 lcfl7lem ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ) ∧ ( 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∧ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) ) ) → 𝑥 = 𝑦 )
55 54 ex ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ) → ( ( 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∧ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) ) → 𝑥 = 𝑦 ) )
56 55 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∀ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ( ( 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∧ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) ) → 𝑥 = 𝑦 ) )
57 56 a1d ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) → ∀ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∀ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ( ( 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∧ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) ) → 𝑥 = 𝑦 ) ) )
58 57 ancld ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) → ( ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∧ ∀ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∀ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ( ( 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∧ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) ) → 𝑥 = 𝑦 ) ) ) )
59 sneq ⊢ ( 𝑥 = 𝑦 → { 𝑥 } = { 𝑦 } )
60 59 fveq2d ⊢ ( 𝑥 = 𝑦 → ( ⊥ ‘ { 𝑥 } ) = ( ⊥ ‘ { 𝑦 } ) )
61 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑘 · 𝑥 ) = ( 𝑘 · 𝑦 ) )
62 61 oveq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑤 + ( 𝑘 · 𝑥 ) ) = ( 𝑤 + ( 𝑘 · 𝑦 ) ) )
63 62 eqeq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ↔ 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) )
64 60 63 rexeqbidv ⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ↔ ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) )
65 64 riotabidv ⊢ ( 𝑥 = 𝑦 → ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) = ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) )
66 65 mpteq2dv ⊢ ( 𝑥 = 𝑦 → ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) )
67 66 eqeq2d ⊢ ( 𝑥 = 𝑦 → ( 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ↔ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) ) )
68 67 reu4 ⊢ ( ∃! 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ↔ ( ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∧ ∀ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ∀ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ( ( 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ∧ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑦 ) ) ) ) ) → 𝑥 = 𝑦 ) ) )
69 58 68 imbitrrdi ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) → ∃! 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) )
70 reurex ⊢ ( ∃! 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) → ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) )
71 69 70 impbid1 ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ↔ ∃! 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) )
72 71 orbi2d ⊢ ( 𝜑 → ( ( ( 𝐿 ‘ 𝐺 ) = 𝑉 ∨ ∃ 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) ↔ ( ( 𝐿 ‘ 𝐺 ) = 𝑉 ∨ ∃! 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) ) )
73 15 72 bitrd ⊢ ( 𝜑 → ( 𝐺 ∈ 𝐶 ↔ ( ( 𝐿 ‘ 𝐺 ) = 𝑉 ∨ ∃! 𝑥 ∈ ( 𝑉 ∖ { 0 } ) 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) ) )