Metamath Proof Explorer


Theorem mapdval

Description: Value of projectivity from vector space H to dual space. (Contributed by NM, 27-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 ‘ 𝐾 ) ‘ 𝑊 )
mapdval.k ( 𝜑 → ( 𝐾𝑋𝑊𝐻 ) )
mapdval.t ( 𝜑𝑇𝑆 )
Assertion mapdval ( 𝜑 → ( 𝑀𝑇 ) = { 𝑓𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑇 ) } )

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 mapdval.k ( 𝜑 → ( 𝐾𝑋𝑊𝐻 ) )
9 mapdval.t ( 𝜑𝑇𝑆 )
10 1 2 3 4 5 6 7 mapdfval ( ( 𝐾𝑋𝑊𝐻 ) → 𝑀 = ( 𝑠𝑆 ↦ { 𝑓𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑠 ) } ) )
11 8 10 syl ( 𝜑𝑀 = ( 𝑠𝑆 ↦ { 𝑓𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑠 ) } ) )
12 11 fveq1d ( 𝜑 → ( 𝑀𝑇 ) = ( ( 𝑠𝑆 ↦ { 𝑓𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑠 ) } ) ‘ 𝑇 ) )
13 4 fvexi 𝐹 ∈ V
14 13 rabex { 𝑓𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑇 ) } ∈ V
15 sseq2 ( 𝑠 = 𝑇 → ( ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑠 ↔ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑇 ) )
16 15 anbi2d ( 𝑠 = 𝑇 → ( ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑠 ) ↔ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑇 ) ) )
17 16 rabbidv ( 𝑠 = 𝑇 → { 𝑓𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑠 ) } = { 𝑓𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑇 ) } )
18 eqid ( 𝑠𝑆 ↦ { 𝑓𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑠 ) } ) = ( 𝑠𝑆 ↦ { 𝑓𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑠 ) } )
19 17 18 fvmptg ( ( 𝑇𝑆 ∧ { 𝑓𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑇 ) } ∈ V ) → ( ( 𝑠𝑆 ↦ { 𝑓𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑠 ) } ) ‘ 𝑇 ) = { 𝑓𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑇 ) } )
20 9 14 19 sylancl ( 𝜑 → ( ( 𝑠𝑆 ↦ { 𝑓𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑠 ) } ) ‘ 𝑇 ) = { 𝑓𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑇 ) } )
21 12 20 eqtrd ( 𝜑 → ( 𝑀𝑇 ) = { 𝑓𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ) = ( 𝐿𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿𝑓 ) ) ⊆ 𝑇 ) } )