Theorem lcf1o

Description: Define a function J that provides a bijection from nonzero vectors V to nonzero functionals with closed kernels C . (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	lcf1o	⊢ ( 𝜑 → 𝐽 : ( 𝑉 ∖ { 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		oveq1	⊢ ( 𝑤 = 𝑧 → ( 𝑤 + ( 𝑘 · 𝑥 ) ) = ( 𝑧 + ( 𝑘 · 𝑥 ) ) )
18	17	eqeq2d	⊢ ( 𝑤 = 𝑧 → ( 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ↔ 𝑣 = ( 𝑧 + ( 𝑘 · 𝑥 ) ) ) )
19	18	cbvrexvw	⊢ ( ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ↔ ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑧 + ( 𝑘 · 𝑥 ) ) )
20		oveq1	⊢ ( 𝑘 = 𝑙 → ( 𝑘 · 𝑥 ) = ( 𝑙 · 𝑥 ) )
21	20	oveq2d	⊢ ( 𝑘 = 𝑙 → ( 𝑧 + ( 𝑘 · 𝑥 ) ) = ( 𝑧 + ( 𝑙 · 𝑥 ) ) )
22	21	eqeq2d	⊢ ( 𝑘 = 𝑙 → ( 𝑣 = ( 𝑧 + ( 𝑘 · 𝑥 ) ) ↔ 𝑣 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) ) )
23	22	rexbidv	⊢ ( 𝑘 = 𝑙 → ( ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑧 + ( 𝑘 · 𝑥 ) ) ↔ ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) ) )
24	19 23	syl5bb	⊢ ( 𝑘 = 𝑙 → ( ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ↔ ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) ) )
25	24	cbvriotavw	⊢ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) = ( ℩ 𝑙 ∈ 𝑅 ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) )
26		eqeq1	⊢ ( 𝑣 = 𝑢 → ( 𝑣 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) ↔ 𝑢 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) ) )
27	26	rexbidv	⊢ ( 𝑣 = 𝑢 → ( ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) ↔ ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) ) )
28	27	riotabidv	⊢ ( 𝑣 = 𝑢 → ( ℩ 𝑙 ∈ 𝑅 ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) ) = ( ℩ 𝑙 ∈ 𝑅 ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) ) )
29	25 28	syl5eq	⊢ ( 𝑣 = 𝑢 → ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) = ( ℩ 𝑙 ∈ 𝑅 ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) ) )
30	29	cbvmptv	⊢ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) = ( 𝑢 ∈ 𝑉 ↦ ( ℩ 𝑙 ∈ 𝑅 ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) ) )
31		sneq	⊢ ( 𝑥 = 𝑦 → { 𝑥 } = { 𝑦 } )
32	31	fveq2d	⊢ ( 𝑥 = 𝑦 → ( ⊥ ‘ { 𝑥 } ) = ( ⊥ ‘ { 𝑦 } ) )
33		oveq2	⊢ ( 𝑥 = 𝑦 → ( 𝑙 · 𝑥 ) = ( 𝑙 · 𝑦 ) )
34	33	oveq2d	⊢ ( 𝑥 = 𝑦 → ( 𝑧 + ( 𝑙 · 𝑥 ) ) = ( 𝑧 + ( 𝑙 · 𝑦 ) ) )
35	34	eqeq2d	⊢ ( 𝑥 = 𝑦 → ( 𝑢 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) ↔ 𝑢 = ( 𝑧 + ( 𝑙 · 𝑦 ) ) ) )
36	32 35	rexeqbidv	⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) ↔ ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑦 ) ) ) )
37	36	riotabidv	⊢ ( 𝑥 = 𝑦 → ( ℩ 𝑙 ∈ 𝑅 ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) ) = ( ℩ 𝑙 ∈ 𝑅 ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑦 ) ) ) )
38	37	mpteq2dv	⊢ ( 𝑥 = 𝑦 → ( 𝑢 ∈ 𝑉 ↦ ( ℩ 𝑙 ∈ 𝑅 ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑥 ) ) ) ) = ( 𝑢 ∈ 𝑉 ↦ ( ℩ 𝑙 ∈ 𝑅 ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑦 ) ) ) ) )
39	30 38	syl5eq	⊢ ( 𝑥 = 𝑦 → ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) = ( 𝑢 ∈ 𝑉 ↦ ( ℩ 𝑙 ∈ 𝑅 ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑦 ) ) ) ) )
40	39	cbvmptv	⊢ ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) ) = ( 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑢 ∈ 𝑉 ↦ ( ℩ 𝑙 ∈ 𝑅 ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑦 ) ) ) ) )
41	15 40	eqtri	⊢ 𝐽 = ( 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑢 ∈ 𝑉 ↦ ( ℩ 𝑙 ∈ 𝑅 ∃ 𝑧 ∈ ( ⊥ ‘ { 𝑦 } ) 𝑢 = ( 𝑧 + ( 𝑙 · 𝑦 ) ) ) ) )
42	1 2 3 4 5 6 7 8 9 10 11 12 13 14 41 16	lcfrlem9	⊢ ( 𝜑 → 𝐽 : ( 𝑉 ∖ { 0 } ) –1-1-onto→ ( 𝐶 ∖ { 𝑄 } ) )