Metamath Proof Explorer


Theorem mapdcl

Description: Closure the value of the map defined by df-mapd . (Contributed by NM, 13-Mar-2015)

Ref Expression
Hypotheses mapdcnvcl.h 𝐻 = ( LHyp ‘ 𝐾 )
mapdcnvcl.m 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
mapdcnvcl.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
mapdcnvcl.s 𝑆 = ( LSubSp ‘ 𝑈 )
mapdcnvcl.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
mapdcl.x ( 𝜑𝑋𝑆 )
Assertion mapdcl ( 𝜑 → ( 𝑀𝑋 ) ∈ ran 𝑀 )

Proof

Step Hyp Ref Expression
1 mapdcnvcl.h 𝐻 = ( LHyp ‘ 𝐾 )
2 mapdcnvcl.m 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
3 mapdcnvcl.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 mapdcnvcl.s 𝑆 = ( LSubSp ‘ 𝑈 )
5 mapdcnvcl.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
6 mapdcl.x ( 𝜑𝑋𝑆 )
7 eqid ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
8 eqid ( LFnl ‘ 𝑈 ) = ( LFnl ‘ 𝑈 )
9 eqid ( LKer ‘ 𝑈 ) = ( LKer ‘ 𝑈 )
10 eqid ( LDual ‘ 𝑈 ) = ( LDual ‘ 𝑈 )
11 eqid ( LSubSp ‘ ( LDual ‘ 𝑈 ) ) = ( LSubSp ‘ ( LDual ‘ 𝑈 ) )
12 eqid { 𝑔 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) } = { 𝑔 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) }
13 1 7 2 3 4 8 9 10 11 12 5 mapd1o ( 𝜑𝑀 : 𝑆1-1-onto→ ( ( LSubSp ‘ ( LDual ‘ 𝑈 ) ) ∩ 𝒫 { 𝑔 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) } ) )
14 f1ofn ( 𝑀 : 𝑆1-1-onto→ ( ( LSubSp ‘ ( LDual ‘ 𝑈 ) ) ∩ 𝒫 { 𝑔 ∈ ( LFnl ‘ 𝑈 ) ∣ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) ) ) = ( ( LKer ‘ 𝑈 ) ‘ 𝑔 ) } ) → 𝑀 Fn 𝑆 )
15 13 14 syl ( 𝜑𝑀 Fn 𝑆 )
16 dffn3 ( 𝑀 Fn 𝑆𝑀 : 𝑆 ⟶ ran 𝑀 )
17 15 16 sylib ( 𝜑𝑀 : 𝑆 ⟶ ran 𝑀 )
18 17 6 ffvelrnd ( 𝜑 → ( 𝑀𝑋 ) ∈ ran 𝑀 )