Metamath Proof Explorer

Theorem dihord6a

Description: Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014)

Ref Expression
Hypotheses dihord3.b ⊢ B = Base K
dihord3.l ⊢ ≤ ˙ = ≤ K
dihord3.h ⊢ H = LHyp ⁡ K
dihord3.i ⊢ I = DIsoH ⁡ K ⁡ W
Assertion dihord6a ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ ¬ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W ∧ I ⁡ X ⊆ I ⁡ Y → X ≤ ˙ Y

Proof

Step Hyp Ref Expression
1 dihord3.b ⊢ B = Base K
2 dihord3.l ⊢ ≤ ˙ = ≤ K
3 dihord3.h ⊢ H = LHyp ⁡ K
4 dihord3.i ⊢ I = DIsoH ⁡ K ⁡ W
5 eqid ⊢ Atoms ⁡ K = Atoms ⁡ K
6 eqid ⊢ oc ⁡ K ⁡ W = oc ⁡ K ⁡ W
7 eqid ⊢ h ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ B = h ∈ LTrn ⁡ K ⁡ W ⟼ I ↾ B
8 eqid ⊢ LTrn ⁡ K ⁡ W = LTrn ⁡ K ⁡ W
9 eqid ⊢ TEndo ⁡ K ⁡ W = TEndo ⁡ K ⁡ W
10 eqid ⊢ DVecH ⁡ K ⁡ W = DVecH ⁡ K ⁡ W
11 eqid ⊢ LSSum ⁡ DVecH ⁡ K ⁡ W = LSSum ⁡ DVecH ⁡ K ⁡ W
12 eqid ⊢ ι h ∈ LTrn ⁡ K ⁡ W | h ⁡ oc ⁡ K ⁡ W = q = ι h ∈ LTrn ⁡ K ⁡ W | h ⁡ oc ⁡ K ⁡ W = q
13 1 2 5 3 6 7 8 9 4 10 11 12 dihord6apre ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ ¬ X ≤ ˙ W ∧ Y ∈ B ∧ Y ≤ ˙ W ∧ I ⁡ X ⊆ I ⁡ Y → X ≤ ˙ Y