Metamath Proof Explorer

Theorem mapdhvmap

Description: Relationship between mapd and HVMap , which can be used to satisfy the last hypothesis of mapdpg . Equation 10 of Baer p. 48. (Contributed by NM, 29-Mar-2015)

Ref Expression
Hypotheses mapdhvmap.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
mapdhvmap.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
mapdhvmap.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
mapdhvmap.z ⊢ 0 = ( 0g ‘ 𝑈 )
mapdhvmap.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
mapdhvmap.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
mapdhvmap.j ⊢ 𝐽 = ( LSpan ‘ 𝐶 )
mapdhvmap.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
mapdhvmap.p ⊢ 𝑃 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
mapdhvmap.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
mapdhvmap.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
Assertion mapdhvmap ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝐽 ‘ { ( 𝑃 ‘ 𝑋 ) } ) )

Proof

Step Hyp Ref Expression
1 mapdhvmap.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 mapdhvmap.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 mapdhvmap.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 mapdhvmap.z ⊢ 0 = ( 0g ‘ 𝑈 )
5 mapdhvmap.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
6 mapdhvmap.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
7 mapdhvmap.j ⊢ 𝐽 = ( LSpan ‘ 𝐶 )
8 mapdhvmap.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
9 mapdhvmap.p ⊢ 𝑃 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
10 mapdhvmap.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
11 mapdhvmap.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
12 eqid ⊢ ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
13 eqid ⊢ ( LFnl ‘ 𝑈 ) = ( LFnl ‘ 𝑈 )
14 eqid ⊢ ( LKer ‘ 𝑈 ) = ( LKer ‘ 𝑈 )
15 eqid ⊢ ( LDual ‘ 𝑈 ) = ( LDual ‘ 𝑈 )
16 eqid ⊢ ( LSpan ‘ ( LDual ‘ 𝑈 ) ) = ( LSpan ‘ ( LDual ‘ 𝑈 ) )
17 11 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
18 1 2 3 4 13 9 10 11 hvmaplfl ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑋 ) ∈ ( LFnl ‘ 𝑈 ) )
19 1 12 2 3 4 14 9 10 11 hvmaplkr ⊢ ( 𝜑 → ( ( LKer ‘ 𝑈 ) ‘ ( 𝑃 ‘ 𝑋 ) ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ { 𝑋 } ) )
20 1 12 8 2 3 5 13 14 15 16 10 17 18 19 mapdsn3 ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( ( LSpan ‘ ( LDual ‘ 𝑈 ) ) ‘ { ( 𝑃 ‘ 𝑋 ) } ) )
21 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
22 eqid ⊢ ( 0g ‘ 𝐶 ) = ( 0g ‘ 𝐶 )
23 1 2 3 4 6 21 22 9 10 11 hvmapcl2 ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑋 ) ∈ ( ( Base ‘ 𝐶 ) ∖ { ( 0g ‘ 𝐶 ) } ) )
24 23 eldifad ⊢ ( 𝜑 → ( 𝑃 ‘ 𝑋 ) ∈ ( Base ‘ 𝐶 ) )
25 24 snssd ⊢ ( 𝜑 → { ( 𝑃 ‘ 𝑋 ) } ⊆ ( Base ‘ 𝐶 ) )
26 1 2 15 16 6 21 7 10 25 lcdlsp ⊢ ( 𝜑 → ( 𝐽 ‘ { ( 𝑃 ‘ 𝑋 ) } ) = ( ( LSpan ‘ ( LDual ‘ 𝑈 ) ) ‘ { ( 𝑃 ‘ 𝑋 ) } ) )
27 20 26 eqtr4d ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝐽 ‘ { ( 𝑃 ‘ 𝑋 ) } ) )