Metamath Proof Explorer


Theorem dihord

Description: The isomorphism H is order-preserving. Part of proof after Lemma N of Crawley p. 122 line 6. (Contributed by NM, 7-Mar-2014)

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

Proof

Step Hyp Ref Expression
1 dihord.b 𝐵 = ( Base ‘ 𝐾 )
2 dihord.l = ( le ‘ 𝐾 )
3 dihord.h 𝐻 = ( LHyp ‘ 𝐾 )
4 dihord.i 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
5 simpl1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( 𝑋 𝑊𝑌 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
6 simpl2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( 𝑋 𝑊𝑌 𝑊 ) ) → 𝑋𝐵 )
7 simprl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( 𝑋 𝑊𝑌 𝑊 ) ) → 𝑋 𝑊 )
8 simpl3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( 𝑋 𝑊𝑌 𝑊 ) ) → 𝑌𝐵 )
9 simprr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( 𝑋 𝑊𝑌 𝑊 ) ) → 𝑌 𝑊 )
10 1 2 3 4 dihord3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑋 𝑊 ) ∧ ( 𝑌𝐵𝑌 𝑊 ) ) → ( ( 𝐼𝑋 ) ⊆ ( 𝐼𝑌 ) ↔ 𝑋 𝑌 ) )
11 5 6 7 8 9 10 syl122anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( 𝑋 𝑊𝑌 𝑊 ) ) → ( ( 𝐼𝑋 ) ⊆ ( 𝐼𝑌 ) ↔ 𝑋 𝑌 ) )
12 simpl1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( 𝑋 𝑊 ∧ ¬ 𝑌 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
13 simpl2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( 𝑋 𝑊 ∧ ¬ 𝑌 𝑊 ) ) → 𝑋𝐵 )
14 simprl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( 𝑋 𝑊 ∧ ¬ 𝑌 𝑊 ) ) → 𝑋 𝑊 )
15 simpl3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( 𝑋 𝑊 ∧ ¬ 𝑌 𝑊 ) ) → 𝑌𝐵 )
16 simprr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( 𝑋 𝑊 ∧ ¬ 𝑌 𝑊 ) ) → ¬ 𝑌 𝑊 )
17 1 2 3 4 dihord5a ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑋 𝑊 ) ∧ ( 𝑌𝐵 ∧ ¬ 𝑌 𝑊 ) ) ∧ ( 𝐼𝑋 ) ⊆ ( 𝐼𝑌 ) ) → 𝑋 𝑌 )
18 1 2 3 4 dihord5b ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑋 𝑊 ) ∧ ( 𝑌𝐵 ∧ ¬ 𝑌 𝑊 ) ) ∧ 𝑋 𝑌 ) → ( 𝐼𝑋 ) ⊆ ( 𝐼𝑌 ) )
19 17 18 impbida ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑋 𝑊 ) ∧ ( 𝑌𝐵 ∧ ¬ 𝑌 𝑊 ) ) → ( ( 𝐼𝑋 ) ⊆ ( 𝐼𝑌 ) ↔ 𝑋 𝑌 ) )
20 12 13 14 15 16 19 syl122anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( 𝑋 𝑊 ∧ ¬ 𝑌 𝑊 ) ) → ( ( 𝐼𝑋 ) ⊆ ( 𝐼𝑌 ) ↔ 𝑋 𝑌 ) )
21 simpl1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ¬ 𝑋 𝑊𝑌 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
22 simpl2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ¬ 𝑋 𝑊𝑌 𝑊 ) ) → 𝑋𝐵 )
23 simprl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ¬ 𝑋 𝑊𝑌 𝑊 ) ) → ¬ 𝑋 𝑊 )
24 simpl3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ¬ 𝑋 𝑊𝑌 𝑊 ) ) → 𝑌𝐵 )
25 simprr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ¬ 𝑋 𝑊𝑌 𝑊 ) ) → 𝑌 𝑊 )
26 1 2 3 4 dihord6a ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ ( 𝑌𝐵𝑌 𝑊 ) ) ∧ ( 𝐼𝑋 ) ⊆ ( 𝐼𝑌 ) ) → 𝑋 𝑌 )
27 1 2 3 4 dihord6b ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ ( 𝑌𝐵𝑌 𝑊 ) ) ∧ 𝑋 𝑌 ) → ( 𝐼𝑋 ) ⊆ ( 𝐼𝑌 ) )
28 26 27 impbida ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ ( 𝑌𝐵𝑌 𝑊 ) ) → ( ( 𝐼𝑋 ) ⊆ ( 𝐼𝑌 ) ↔ 𝑋 𝑌 ) )
29 21 22 23 24 25 28 syl122anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ¬ 𝑋 𝑊𝑌 𝑊 ) ) → ( ( 𝐼𝑋 ) ⊆ ( 𝐼𝑌 ) ↔ 𝑋 𝑌 ) )
30 simpl1 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ¬ 𝑋 𝑊 ∧ ¬ 𝑌 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
31 simpl2 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ¬ 𝑋 𝑊 ∧ ¬ 𝑌 𝑊 ) ) → 𝑋𝐵 )
32 simprl ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ¬ 𝑋 𝑊 ∧ ¬ 𝑌 𝑊 ) ) → ¬ 𝑋 𝑊 )
33 simpl3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ¬ 𝑋 𝑊 ∧ ¬ 𝑌 𝑊 ) ) → 𝑌𝐵 )
34 simprr ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ¬ 𝑋 𝑊 ∧ ¬ 𝑌 𝑊 ) ) → ¬ 𝑌 𝑊 )
35 1 2 3 4 dihord4 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵 ∧ ¬ 𝑋 𝑊 ) ∧ ( 𝑌𝐵 ∧ ¬ 𝑌 𝑊 ) ) → ( ( 𝐼𝑋 ) ⊆ ( 𝐼𝑌 ) ↔ 𝑋 𝑌 ) )
36 30 31 32 33 34 35 syl122anc ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) ∧ ( ¬ 𝑋 𝑊 ∧ ¬ 𝑌 𝑊 ) ) → ( ( 𝐼𝑋 ) ⊆ ( 𝐼𝑌 ) ↔ 𝑋 𝑌 ) )
37 11 20 29 36 4casesdan ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝐵𝑌𝐵 ) → ( ( 𝐼𝑋 ) ⊆ ( 𝐼𝑌 ) ↔ 𝑋 𝑌 ) )