Theorem mapdsn3

Description: Value of the map defined by df-mapd at the span of a singleton. (Contributed by NM, 17-Feb-2015)

	Ref	Expression
Hypotheses	mapdsn3.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	mapdsn3.o	⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	mapdsn3.m	⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
	mapdsn3.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	mapdsn3.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	mapdsn3.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
	mapdsn3.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	mapdsn3.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	mapdsn3.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
	mapdsn3.p	⊢ 𝑃 = ( LSpan ‘ 𝐷 )
	mapdsn3.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	mapdsn3.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	mapdsn3.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
	mapdsn3.e	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) = ( 𝑂 ‘ { 𝑋 } ) )
Assertion	mapdsn3	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝑃 ‘ { 𝐺 } ) )

Proof

Step	Hyp	Ref	Expression
1		mapdsn3.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		mapdsn3.o	⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		mapdsn3.m	⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
4		mapdsn3.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5		mapdsn3.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
6		mapdsn3.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
7		mapdsn3.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
8		mapdsn3.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
9		mapdsn3.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
10		mapdsn3.p	⊢ 𝑃 = ( LSpan ‘ 𝐷 )
11		mapdsn3.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12		mapdsn3.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
13		mapdsn3.g	⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
14		mapdsn3.e	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) = ( 𝑂 ‘ { 𝑋 } ) )
15	1 2 3 4 5 6 7 8 11 12 14	mapdsn2	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = { 𝑓 ∈ 𝐹 ∣ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑓 ) } )
16	1 4 11	dvhlvec	⊢ ( 𝜑 → 𝑈 ∈ LVec )
17	7 8 9 10 16 13	ldual1dim	⊢ ( 𝜑 → ( 𝑃 ‘ { 𝐺 } ) = { 𝑓 ∈ 𝐹 ∣ ( 𝐿 ‘ 𝐺 ) ⊆ ( 𝐿 ‘ 𝑓 ) } )
18	15 17	eqtr4d	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝑃 ‘ { 𝐺 } ) )