Metamath Proof Explorer

Theorem mapdsn2

Description: Value of the map defined by df-mapd at the span of a singleton. (Contributed by NM, 16-Feb-2015)

Ref Expression
Hypotheses mapdsn.h ⊢ H = LHyp ⁡ K
mapdsn.o ⊢ O = ocH ⁡ K ⁡ W
mapdsn.m ⊢ M = mapd ⁡ K ⁡ W
mapdsn.u ⊢ U = DVecH ⁡ K ⁡ W
mapdsn.v ⊢ V = Base U
mapdsn.n ⊢ N = LSpan ⁡ U
mapdsn.f ⊢ F = LFnl ⁡ U
mapdsn.l ⊢ L = LKer ⁡ U
mapdsn.k ⊢ φ → K ∈ HL ∧ W ∈ H
mapdsn.x ⊢ φ → X ∈ V
mapdsn2.e ⊢ φ → L ⁡ G = O ⁡ X
Assertion mapdsn2 ⊢ φ → M ⁡ N ⁡ X = f ∈ F | L ⁡ G ⊆ L ⁡ f

Proof

Step Hyp Ref Expression
1 mapdsn.h ⊢ H = LHyp ⁡ K
2 mapdsn.o ⊢ O = ocH ⁡ K ⁡ W
3 mapdsn.m ⊢ M = mapd ⁡ K ⁡ W
4 mapdsn.u ⊢ U = DVecH ⁡ K ⁡ W
5 mapdsn.v ⊢ V = Base U
6 mapdsn.n ⊢ N = LSpan ⁡ U
7 mapdsn.f ⊢ F = LFnl ⁡ U
8 mapdsn.l ⊢ L = LKer ⁡ U
9 mapdsn.k ⊢ φ → K ∈ HL ∧ W ∈ H
10 mapdsn.x ⊢ φ → X ∈ V
11 mapdsn2.e ⊢ φ → L ⁡ G = O ⁡ X
12 1 2 3 4 5 6 7 8 9 10 mapdsn ⊢ φ → M ⁡ N ⁡ X = f ∈ F | O ⁡ X ⊆ L ⁡ f
13 11 sseq1d ⊢ φ → L ⁡ G ⊆ L ⁡ f ↔ O ⁡ X ⊆ L ⁡ f
14 13 rabbidv ⊢ φ → f ∈ F | L ⁡ G ⊆ L ⁡ f = f ∈ F | O ⁡ X ⊆ L ⁡ f
15 12 14 eqtr4d ⊢ φ → M ⁡ N ⁡ X = f ∈ F | L ⁡ G ⊆ L ⁡ f