Metamath Proof Explorer

Theorem mapdfval

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

Ref Expression
Hypotheses mapdval.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
mapdval.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
mapdval.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
mapdval.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
mapdval.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
mapdval.o ⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
mapdval.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
Assertion mapdfval ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) → 𝑀 = ( 𝑠 ∈ 𝑆 ↦ { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑠 ) } ) )

Proof

Step Hyp Ref Expression
1 mapdval.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 mapdval.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 mapdval.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
4 mapdval.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
5 mapdval.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
6 mapdval.o ⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
7 mapdval.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
8 1 mapdffval ⊢ ( 𝐾 ∈ 𝑋 → ( mapd ‘ 𝐾 ) = ( 𝑤 ∈ 𝐻 ↦ ( 𝑠 ∈ ( LSubSp ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ∣ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ⊆ 𝑠 ) } ) ) )
9 8 fveq1d ⊢ ( 𝐾 ∈ 𝑋 → ( ( mapd ‘ 𝐾 ) ‘ 𝑊 ) = ( ( 𝑤 ∈ 𝐻 ↦ ( 𝑠 ∈ ( LSubSp ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ∣ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ⊆ 𝑠 ) } ) ) ‘ 𝑊 ) )
10 7 9 syl5eq ⊢ ( 𝐾 ∈ 𝑋 → 𝑀 = ( ( 𝑤 ∈ 𝐻 ↦ ( 𝑠 ∈ ( LSubSp ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ∣ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ⊆ 𝑠 ) } ) ) ‘ 𝑊 ) )
11 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
12 11 2 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) = 𝑈 )
13 12 fveq2d ⊢ ( 𝑤 = 𝑊 → ( LSubSp ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) = ( LSubSp ‘ 𝑈 ) )
14 13 3 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( LSubSp ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) = 𝑆 )
15 12 fveq2d ⊢ ( 𝑤 = 𝑊 → ( LFnl ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) = ( LFnl ‘ 𝑈 ) )
16 15 4 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( LFnl ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) = 𝐹 )
17 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) )
18 17 6 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) = 𝑂 )
19 12 fveq2d ⊢ ( 𝑤 = 𝑊 → ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) = ( LKer ‘ 𝑈 ) )
20 19 5 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) = 𝐿 )
21 20 fveq1d ⊢ ( 𝑤 = 𝑊 → ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) = ( 𝐿 ‘ 𝑓 ) )
22 18 21 fveq12d ⊢ ( 𝑤 = 𝑊 → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) = ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) )
23 18 22 fveq12d ⊢ ( 𝑤 = 𝑊 → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) )
24 23 21 eqeq12d ⊢ ( 𝑤 = 𝑊 → ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ↔ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ) )
25 22 sseq1d ⊢ ( 𝑤 = 𝑊 → ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ⊆ 𝑠 ↔ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑠 ) )
26 24 25 anbi12d ⊢ ( 𝑤 = 𝑊 → ( ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ⊆ 𝑠 ) ↔ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑠 ) ) )
27 16 26 rabeqbidv ⊢ ( 𝑤 = 𝑊 → { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ∣ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ⊆ 𝑠 ) } = { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑠 ) } )
28 14 27 mpteq12dv ⊢ ( 𝑤 = 𝑊 → ( 𝑠 ∈ ( LSubSp ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ∣ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ⊆ 𝑠 ) } ) = ( 𝑠 ∈ 𝑆 ↦ { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑠 ) } ) )
29 eqid ⊢ ( 𝑤 ∈ 𝐻 ↦ ( 𝑠 ∈ ( 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 ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ⊆ 𝑠 ) } ) )
30 28 29 3 mptfvmpt ⊢ ( 𝑊 ∈ 𝐻 → ( ( 𝑤 ∈ 𝐻 ↦ ( 𝑠 ∈ ( LSubSp ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ↦ { 𝑓 ∈ ( LFnl ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ∣ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ) = ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ∧ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑤 ) ‘ ( ( LKer ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑤 ) ) ‘ 𝑓 ) ) ⊆ 𝑠 ) } ) ) ‘ 𝑊 ) = ( 𝑠 ∈ 𝑆 ↦ { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑠 ) } ) )
31 10 30 sylan9eq ⊢ ( ( 𝐾 ∈ 𝑋 ∧ 𝑊 ∈ 𝐻 ) → 𝑀 = ( 𝑠 ∈ 𝑆 ↦ { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑠 ) } ) )