Metamath Proof Explorer


Theorem mapd1dim2lem1N

Description: Value of the map defined by df-mapd at an atom. (Contributed by NM, 10-Feb-2015) (New usage is discouraged.)

Ref Expression
Hypotheses mapd1dim2.h 𝐻 = ( LHyp ‘ 𝐾 )
mapd1dim2.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
mapd1dim2.a 𝐴 = ( LSAtoms ‘ 𝑈 )
mapd1dim2.f 𝐹 = ( LFnl ‘ 𝑈 )
mapd1dim2.l 𝐿 = ( LKer ‘ 𝑈 )
mapd1dim2.o 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
mapd1dim2.m 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
mapd1dim2.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
mapd1dim2.t ( 𝜑𝑄𝐴 )
Assertion mapd1dim2lem1N ( 𝜑 → ( 𝑀𝑄 ) = { 𝑓𝐹 ∣ ∃ 𝑣𝑄 ( 𝑂 ‘ { 𝑣 } ) = ( 𝐿𝑓 ) } )

Proof

Step Hyp Ref Expression
1 mapd1dim2.h 𝐻 = ( LHyp ‘ 𝐾 )
2 mapd1dim2.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 mapd1dim2.a 𝐴 = ( LSAtoms ‘ 𝑈 )
4 mapd1dim2.f 𝐹 = ( LFnl ‘ 𝑈 )
5 mapd1dim2.l 𝐿 = ( LKer ‘ 𝑈 )
6 mapd1dim2.o 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
7 mapd1dim2.m 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
8 mapd1dim2.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
9 mapd1dim2.t ( 𝜑𝑄𝐴 )
10 eqid ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
11 1 2 8 dvhlmod ( 𝜑𝑈 ∈ LMod )
12 10 3 11 9 lsatlssel ( 𝜑𝑄 ∈ ( LSubSp ‘ 𝑈 ) )
13 1 2 10 4 5 6 7 8 12 mapdval4N ( 𝜑 → ( 𝑀𝑄 ) = { 𝑓𝐹 ∣ ∃ 𝑣𝑄 ( 𝑂 ‘ { 𝑣 } ) = ( 𝐿𝑓 ) } )