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 } ) 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) ) )