Metamath Proof Explorer


Theorem lcfrlem8

Description: Lemma for lcf1o and lcfr . (Contributed by NM, 21-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 ∧ 𝑊𝐻 ) )
lcfrlem8.x ( 𝜑𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
Assertion lcfrlem8 ( 𝜑 → ( 𝐽𝑋 ) = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑋 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) ) )

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 lcfrlem8.x ( 𝜑𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
18 sneq ( 𝑥 = 𝑋 → { 𝑥 } = { 𝑋 } )
19 18 fveq2d ( 𝑥 = 𝑋 → ( ‘ { 𝑥 } ) = ( ‘ { 𝑋 } ) )
20 oveq2 ( 𝑥 = 𝑋 → ( 𝑘 · 𝑥 ) = ( 𝑘 · 𝑋 ) )
21 20 oveq2d ( 𝑥 = 𝑋 → ( 𝑤 + ( 𝑘 · 𝑥 ) ) = ( 𝑤 + ( 𝑘 · 𝑋 ) ) )
22 21 eqeq2d ( 𝑥 = 𝑋 → ( 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ↔ 𝑣 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) )
23 19 22 rexeqbidv ( 𝑥 = 𝑋 → ( ∃ 𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ↔ ∃ 𝑤 ∈ ( ‘ { 𝑋 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) )
24 23 riotabidv ( 𝑥 = 𝑋 → ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) = ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑋 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) )
25 24 mpteq2dv ( 𝑥 = 𝑋 → ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑋 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) ) )
26 25 15 4 mptfvmpt ( 𝑋 ∈ ( 𝑉 ∖ { 0 } ) → ( 𝐽𝑋 ) = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑋 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) ) )
27 17 26 syl ( 𝜑 → ( 𝐽𝑋 ) = ( 𝑣𝑉 ↦ ( 𝑘𝑅𝑤 ∈ ( ‘ { 𝑋 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) ) )