Metamath Proof Explorer


Theorem mapdrn

Description: Range of the map defined by df-mapd . (Contributed by NM, 12-Mar-2015)

Ref Expression
Hypotheses mapdrn.h 𝐻 = ( LHyp ‘ 𝐾 )
mapdrn.o 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
mapdrn.m 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
mapdrn.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
mapdrn.f 𝐹 = ( LFnl ‘ 𝑈 )
mapdrn.l 𝐿 = ( LKer ‘ 𝑈 )
mapdrn.d 𝐷 = ( LDual ‘ 𝑈 )
mapdrn.t 𝑇 = ( LSubSp ‘ 𝐷 )
mapdrn.c 𝐶 = { 𝑔𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝑔 ) ) ) = ( 𝐿𝑔 ) }
mapdrn.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
Assertion mapdrn ( 𝜑 → ran 𝑀 = ( 𝑇 ∩ 𝒫 𝐶 ) )

Proof

Step Hyp Ref Expression
1 mapdrn.h 𝐻 = ( LHyp ‘ 𝐾 )
2 mapdrn.o 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 mapdrn.m 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
4 mapdrn.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 mapdrn.f 𝐹 = ( LFnl ‘ 𝑈 )
6 mapdrn.l 𝐿 = ( LKer ‘ 𝑈 )
7 mapdrn.d 𝐷 = ( LDual ‘ 𝑈 )
8 mapdrn.t 𝑇 = ( LSubSp ‘ 𝐷 )
9 mapdrn.c 𝐶 = { 𝑔𝐹 ∣ ( 𝑂 ‘ ( 𝑂 ‘ ( 𝐿𝑔 ) ) ) = ( 𝐿𝑔 ) }
10 mapdrn.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
11 eqid ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
12 1 2 3 4 11 5 6 7 8 9 10 mapd1o ( 𝜑𝑀 : ( LSubSp ‘ 𝑈 ) –1-1-onto→ ( 𝑇 ∩ 𝒫 𝐶 ) )
13 f1ofo ( 𝑀 : ( LSubSp ‘ 𝑈 ) –1-1-onto→ ( 𝑇 ∩ 𝒫 𝐶 ) → 𝑀 : ( LSubSp ‘ 𝑈 ) –onto→ ( 𝑇 ∩ 𝒫 𝐶 ) )
14 forn ( 𝑀 : ( LSubSp ‘ 𝑈 ) –onto→ ( 𝑇 ∩ 𝒫 𝐶 ) → ran 𝑀 = ( 𝑇 ∩ 𝒫 𝐶 ) )
15 12 13 14 3syl ( 𝜑 → ran 𝑀 = ( 𝑇 ∩ 𝒫 𝐶 ) )