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	⊢ ( 𝜑 → ( 𝑀 ‘ 𝑇 ) = { 𝑓 ∈ 𝐹 ∣ ( ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) ∧ ( 𝑂 ‘ ( 𝐿 ‘ 𝑓 ) ) ⊆ 𝑇 ) } )