Metamath Proof Explorer

Theorem mapdord

Description: Ordering property of the map defined by df-mapd . Property (b) of Baer p. 40. (Contributed by NM, 27-Jan-2015)

Ref Expression
Hypotheses mapdord.h ⊢ H = LHyp ⁡ K
mapdord.u ⊢ U = DVecH ⁡ K ⁡ W
mapdord.s ⊢ S = LSubSp ⁡ U
mapdord.m ⊢ M = mapd ⁡ K ⁡ W
mapdord.k ⊢ φ → K ∈ HL ∧ W ∈ H
mapdord.x ⊢ φ → X ∈ S
mapdord.y ⊢ φ → Y ∈ S
Assertion mapdord ⊢ φ → M ⁡ X ⊆ M ⁡ Y ↔ X ⊆ Y

Proof

Step Hyp Ref Expression
1 mapdord.h ⊢ H = LHyp ⁡ K
2 mapdord.u ⊢ U = DVecH ⁡ K ⁡ W
3 mapdord.s ⊢ S = LSubSp ⁡ U
4 mapdord.m ⊢ M = mapd ⁡ K ⁡ W
5 mapdord.k ⊢ φ → K ∈ HL ∧ W ∈ H
6 mapdord.x ⊢ φ → X ∈ S
7 mapdord.y ⊢ φ → Y ∈ S
8 eqid ⊢ ocH ⁡ K ⁡ W = ocH ⁡ K ⁡ W
9 eqid ⊢ LSAtoms ⁡ U = LSAtoms ⁡ U
10 eqid ⊢ LFnl ⁡ U = LFnl ⁡ U
11 eqid ⊢ LSHyp ⁡ U = LSHyp ⁡ U
12 eqid ⊢ LKer ⁡ U = LKer ⁡ U
13 eqid ⊢ g ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ g ∈ LSHyp ⁡ U = g ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ g ∈ LSHyp ⁡ U
14 eqid ⊢ g ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ g = LKer ⁡ U ⁡ g = g ∈ LFnl ⁡ U | ocH ⁡ K ⁡ W ⁡ ocH ⁡ K ⁡ W ⁡ LKer ⁡ U ⁡ g = LKer ⁡ U ⁡ g
15 1 2 3 4 5 6 7 8 9 10 11 12 13 14 mapdordlem2 ⊢ φ → M ⁡ X ⊆ M ⁡ Y ↔ X ⊆ Y