Metamath Proof Explorer


Theorem dihord5a

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

Ref Expression
Hypotheses dihord.b 𝐵 = ( Base ‘ 𝐾 )
dihord.l = ( le ‘ 𝐾 )
dihord.h 𝐻 = ( LHyp ‘ 𝐾 )
dihord.i 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
Assertion dihord5a ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑋 𝑊 ) ∧ ( 𝑌𝐵 ∧ ¬ 𝑌 𝑊 ) ) ∧ ( 𝐼𝑋 ) ⊆ ( 𝐼𝑌 ) ) → 𝑋 𝑌 )

Proof

Step Hyp Ref Expression
1 dihord.b 𝐵 = ( Base ‘ 𝐾 )
2 dihord.l = ( le ‘ 𝐾 )
3 dihord.h 𝐻 = ( LHyp ‘ 𝐾 )
4 dihord.i 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
5 eqid ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
6 eqid ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
7 eqid ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
8 eqid ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
9 eqid ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( LSSum ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
10 1 2 3 5 6 7 8 9 4 dihord5apre ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑋 𝑊 ) ∧ ( 𝑌𝐵 ∧ ¬ 𝑌 𝑊 ) ) ∧ ( 𝐼𝑋 ) ⊆ ( 𝐼𝑌 ) ) → 𝑋 𝑌 )