Metamath Proof Explorer

Theorem mapdffval

Description: Projectivity from vector space H to dual space. (Contributed by NM, 25-Jan-2015)

Ref Expression
Hypothesis mapdval.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
Assertion mapdffval ( 𝐾 ∈ 𝑋 → ( mapd ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑠 ∈ ( LSubSp ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ∣ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ⊆ 𝑠 ) } ) ) )

Proof

Step Hyp Ref Expression
1 mapdval.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 elex ⊢ ( 𝐾 ∈ 𝑋 → 𝐾 ∈ V )
3 fveq2 ⊢ ( 𝑘 = 𝐾 → ( LHyp ‘ 𝑘 ) = ( LHyp ‘ 𝐾 ) )
4 3 1 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( LHyp ‘ 𝑘 ) = 𝐻 )
5 fveq2 ⊢ ( 𝑘 = 𝐾 → ( DVecH ‘ 𝑘 ) = ( DVecH ‘ 𝐾 ) )
6 5 fveq1d ⊢ ( 𝑘 = 𝐾 → ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) )
7 6 fveq2d ⊢ ( 𝑘 = 𝐾 → ( LSubSp ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) = ( LSubSp ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) )
8 6 fveq2d ⊢ ( 𝑘 = 𝐾 → ( LFnl ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) = ( LFnl ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) )
9 fveq2 ⊢ ( 𝑘 = 𝐾 → ( ocH ‘ 𝑘 ) = ( ocH ‘ 𝐾 ) )
10 9 fveq1d ⊢ ( 𝑘 = 𝐾 → ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) = ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) )
11 6 fveq2d ⊢ ( 𝑘 = 𝐾 → ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) = ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) )
12 11 fveq1d ⊢ ( 𝑘 = 𝐾 → ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) = ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) )
13 10 12 fveq12d ⊢ ( 𝑘 = 𝐾 → ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) )
14 10 13 fveq12d ⊢ ( 𝑘 = 𝐾 → ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) )
15 14 12 eqeq12d ⊢ ( 𝑘 = 𝐾 → ( ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ↔ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) )
16 13 sseq1d ⊢ ( 𝑘 = 𝐾 → ( ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ⊆ 𝑠 ↔ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ⊆ 𝑠 ) )
17 15 16 anbi12d ⊢ ( 𝑘 = 𝐾 → ( ( ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ⊆ 𝑠 ) ↔ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ⊆ 𝑠 ) ) )
18 8 17 rabeqbidv ⊢ ( 𝑘 = 𝐾 → { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∣ ( ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ⊆ 𝑠 ) } = { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ∣ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ⊆ 𝑠 ) } )
19 7 18 mpteq12dv ⊢ ( 𝑘 = 𝐾 → ( 𝑠 ∈ ( LSubSp ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∣ ( ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ⊆ 𝑠 ) } ) = ( 𝑠 ∈ ( LSubSp ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ∣ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ⊆ 𝑠 ) } ) )
20 4 19 mpteq12dv ⊢ ( 𝑘 = 𝐾 → ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑠 ∈ ( LSubSp ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∣ ( ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ⊆ 𝑠 ) } ) ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑠 ∈ ( LSubSp ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ∣ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ⊆ 𝑠 ) } ) ) )
21 df-mapd ⊢ mapd = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑠 ∈ ( LSubSp ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ↦ { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∣ ( ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ⊆ 𝑠 ) } ) ) )
22 20 21 1 mptfvmpt ⊢ ( 𝐾 ∈ V → ( mapd ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑠 ∈ ( LSubSp ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ∣ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ⊆ 𝑠 ) } ) ) )
23 2 22 syl ⊢ ( 𝐾 ∈ 𝑋 → ( mapd ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑠 ∈ ( LSubSp ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ∣ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ⊆ 𝑠 ) } ) ) )