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