Metamath Proof Explorer

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 ⊢ H = LHyp ⁡ K
mapdsn3.o ⊢ O = ocH ⁡ K ⁡ W
mapdsn3.m ⊢ M = mapd ⁡ K ⁡ W
mapdsn3.u ⊢ U = DVecH ⁡ K ⁡ W
mapdsn3.v ⊢ V = Base U
mapdsn3.n ⊢ N = LSpan ⁡ U
mapdsn3.f ⊢ F = LFnl ⁡ U
mapdsn3.l ⊢ L = LKer ⁡ U
mapdsn3.d ⊢ D = LDual ⁡ U
mapdsn3.p ⊢ P = LSpan ⁡ D
mapdsn3.k ⊢ φ → K ∈ HL ∧ W ∈ H
mapdsn3.x ⊢ φ → X ∈ V
mapdsn3.g ⊢ φ → G ∈ F
mapdsn3.e ⊢ φ → L ⁡ G = O ⁡ X
Assertion mapdsn3 ⊢ φ → M ⁡ N ⁡ X = P ⁡ G

Proof

Step Hyp Ref Expression
1 mapdsn3.h ⊢ H = LHyp ⁡ K
2 mapdsn3.o ⊢ O = ocH ⁡ K ⁡ W
3 mapdsn3.m ⊢ M = mapd ⁡ K ⁡ W
4 mapdsn3.u ⊢ U = DVecH ⁡ K ⁡ W
5 mapdsn3.v ⊢ V = Base U
6 mapdsn3.n ⊢ N = LSpan ⁡ U
7 mapdsn3.f ⊢ F = LFnl ⁡ U
8 mapdsn3.l ⊢ L = LKer ⁡ U
9 mapdsn3.d ⊢ D = LDual ⁡ U
10 mapdsn3.p ⊢ P = LSpan ⁡ D
11 mapdsn3.k ⊢ φ → K ∈ HL ∧ W ∈ H
12 mapdsn3.x ⊢ φ → X ∈ V
13 mapdsn3.g ⊢ φ → G ∈ F
14 mapdsn3.e ⊢ φ → L ⁡ G = O ⁡ X
15 1 2 3 4 5 6 7 8 11 12 14 mapdsn2 ⊢ φ → M ⁡ N ⁡ X = f ∈ F | L ⁡ G ⊆ L ⁡ f
16 1 4 11 dvhlvec ⊢ φ → U ∈ LVec
17 7 8 9 10 16 13 ldual1dim ⊢ φ → P ⁡ G = f ∈ F | L ⁡ G ⊆ L ⁡ f
18 15 17 eqtr4d ⊢ φ → M ⁡ N ⁡ X = P ⁡ G