Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dihord5apre Structured version   Visualization version   GIF version

Theorem dihord5apre 37150
Description: Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.)
Hypotheses
Ref Expression
dihord5apre.b 𝐵 = (Base‘𝐾)
dihord5apre.l = (le‘𝐾)
dihord5apre.h 𝐻 = (LHyp‘𝐾)
dihord5apre.j = (join‘𝐾)
dihord5apre.m = (meet‘𝐾)
dihord5apre.a 𝐴 = (Atoms‘𝐾)
dihord5apre.u 𝑈 = ((DVecH‘𝐾)‘𝑊)
dihord5apre.s = (LSSum‘𝑈)
dihord5apre.i 𝐼 = ((DIsoH‘𝐾)‘𝑊)
Assertion
Ref Expression
dihord5apre ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌)) → 𝑋 𝑌)

Proof of Theorem dihord5apre
Dummy variable 𝑟 is distinct from all other variables.
StepHypRef Expression
1 simpl1 1242 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
2 simpl3 1246 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌)) → (𝑌𝐵 ∧ ¬ 𝑌 𝑊))
3 dihord5apre.b . . . 4 𝐵 = (Base‘𝐾)
4 dihord5apre.l . . . 4 = (le‘𝐾)
5 dihord5apre.j . . . 4 = (join‘𝐾)
6 dihord5apre.m . . . 4 = (meet‘𝐾)
7 dihord5apre.a . . . 4 𝐴 = (Atoms‘𝐾)
8 dihord5apre.h . . . 4 𝐻 = (LHyp‘𝐾)
93, 4, 5, 6, 7, 8lhpmcvr2 35912 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) → ∃𝑟𝐴𝑟 𝑊 ∧ (𝑟 (𝑌 𝑊)) = 𝑌))
101, 2, 9syl2anc 579 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌)) → ∃𝑟𝐴𝑟 𝑊 ∧ (𝑟 (𝑌 𝑊)) = 𝑌))
11 simp11l 1383 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → 𝐾 ∈ HL)
1211hllatd 35252 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → 𝐾 ∈ Lat)
13 simp12l 1385 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → 𝑋𝐵)
14 simp3ll 1325 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → 𝑟𝐴)
153, 7atbase 35177 . . . . . . . . 9 (𝑟𝐴𝑟𝐵)
1614, 15syl 17 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → 𝑟𝐵)
173, 5latjcl 17318 . . . . . . . 8 ((𝐾 ∈ Lat ∧ 𝑟𝐵𝑋𝐵) → (𝑟 𝑋) ∈ 𝐵)
1812, 16, 13, 17syl3anc 1490 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝑟 𝑋) ∈ 𝐵)
19 simp13l 1387 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → 𝑌𝐵)
203, 4, 5latlej2 17328 . . . . . . . 8 ((𝐾 ∈ Lat ∧ 𝑟𝐵𝑋𝐵) → 𝑋 (𝑟 𝑋))
2112, 16, 13, 20syl3anc 1490 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → 𝑋 (𝑟 𝑋))
22 simp11 1260 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
23 simp3lr 1326 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → ¬ 𝑟 𝑊)
243, 4, 5latlej1 17327 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ 𝑟𝐵𝑋𝐵) → 𝑟 (𝑟 𝑋))
2512, 16, 13, 24syl3anc 1490 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → 𝑟 (𝑟 𝑋))
26 simp11r 1384 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → 𝑊𝐻)
273, 8lhpbase 35886 . . . . . . . . . . . . . 14 (𝑊𝐻𝑊𝐵)
2826, 27syl 17 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → 𝑊𝐵)
293, 4lattr 17323 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ (𝑟𝐵 ∧ (𝑟 𝑋) ∈ 𝐵𝑊𝐵)) → ((𝑟 (𝑟 𝑋) ∧ (𝑟 𝑋) 𝑊) → 𝑟 𝑊))
3012, 16, 18, 28, 29syl13anc 1491 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → ((𝑟 (𝑟 𝑋) ∧ (𝑟 𝑋) 𝑊) → 𝑟 𝑊))
3125, 30mpand 686 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → ((𝑟 𝑋) 𝑊𝑟 𝑊))
3223, 31mtod 189 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → ¬ (𝑟 𝑋) 𝑊)
33 simp3l 1258 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝑟𝐴 ∧ ¬ 𝑟 𝑊))
34 simp12 1261 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝑋𝐵𝑋 𝑊))
353, 4, 5, 6, 7, 8lhple 35930 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑋𝐵𝑋 𝑊)) → ((𝑟 𝑋) 𝑊) = 𝑋)
3622, 33, 34, 35syl3anc 1490 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → ((𝑟 𝑋) 𝑊) = 𝑋)
3736oveq2d 6857 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝑟 ((𝑟 𝑋) 𝑊)) = (𝑟 𝑋))
38 dihord5apre.i . . . . . . . . . . 11 𝐼 = ((DIsoH‘𝐾)‘𝑊)
39 eqid 2764 . . . . . . . . . . 11 ((DIsoB‘𝐾)‘𝑊) = ((DIsoB‘𝐾)‘𝑊)
40 eqid 2764 . . . . . . . . . . 11 ((DIsoC‘𝐾)‘𝑊) = ((DIsoC‘𝐾)‘𝑊)
41 dihord5apre.u . . . . . . . . . . 11 𝑈 = ((DVecH‘𝐾)‘𝑊)
42 dihord5apre.s . . . . . . . . . . 11 = (LSSum‘𝑈)
433, 4, 5, 6, 7, 8, 38, 39, 40, 41, 42dihvalcq 37124 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑟 𝑋) ∈ 𝐵 ∧ ¬ (𝑟 𝑋) 𝑊) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 ((𝑟 𝑋) 𝑊)) = (𝑟 𝑋))) → (𝐼‘(𝑟 𝑋)) = ((((DIsoC‘𝐾)‘𝑊)‘𝑟) (((DIsoB‘𝐾)‘𝑊)‘((𝑟 𝑋) 𝑊))))
4422, 18, 32, 33, 37, 43syl122anc 1498 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝐼‘(𝑟 𝑋)) = ((((DIsoC‘𝐾)‘𝑊)‘𝑟) (((DIsoB‘𝐾)‘𝑊)‘((𝑟 𝑋) 𝑊))))
458, 41, 22dvhlmod 36998 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → 𝑈 ∈ LMod)
46 eqid 2764 . . . . . . . . . . . . . . 15 (LSubSp‘𝑈) = (LSubSp‘𝑈)
4746lsssssubg 19229 . . . . . . . . . . . . . 14 (𝑈 ∈ LMod → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈))
4845, 47syl 17 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈))
494, 7, 8, 41, 40, 46diclss 37081 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑟𝐴 ∧ ¬ 𝑟 𝑊)) → (((DIsoC‘𝐾)‘𝑊)‘𝑟) ∈ (LSubSp‘𝑈))
5022, 33, 49syl2anc 579 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (((DIsoC‘𝐾)‘𝑊)‘𝑟) ∈ (LSubSp‘𝑈))
5148, 50sseldd 3761 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (((DIsoC‘𝐾)‘𝑊)‘𝑟) ∈ (SubGrp‘𝑈))
523, 6latmcl 17319 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ 𝑌𝐵𝑊𝐵) → (𝑌 𝑊) ∈ 𝐵)
5312, 19, 28, 52syl3anc 1490 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝑌 𝑊) ∈ 𝐵)
543, 4, 6latmle2 17344 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ 𝑌𝐵𝑊𝐵) → (𝑌 𝑊) 𝑊)
5512, 19, 28, 54syl3anc 1490 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝑌 𝑊) 𝑊)
563, 4, 8, 41, 39, 46diblss 37058 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑌 𝑊) ∈ 𝐵 ∧ (𝑌 𝑊) 𝑊)) → (((DIsoB‘𝐾)‘𝑊)‘(𝑌 𝑊)) ∈ (LSubSp‘𝑈))
5722, 53, 55, 56syl12anc 865 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (((DIsoB‘𝐾)‘𝑊)‘(𝑌 𝑊)) ∈ (LSubSp‘𝑈))
5848, 57sseldd 3761 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (((DIsoB‘𝐾)‘𝑊)‘(𝑌 𝑊)) ∈ (SubGrp‘𝑈))
5942lsmub1 18336 . . . . . . . . . . . 12 (((((DIsoC‘𝐾)‘𝑊)‘𝑟) ∈ (SubGrp‘𝑈) ∧ (((DIsoB‘𝐾)‘𝑊)‘(𝑌 𝑊)) ∈ (SubGrp‘𝑈)) → (((DIsoC‘𝐾)‘𝑊)‘𝑟) ⊆ ((((DIsoC‘𝐾)‘𝑊)‘𝑟) (((DIsoB‘𝐾)‘𝑊)‘(𝑌 𝑊))))
6051, 58, 59syl2anc 579 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (((DIsoC‘𝐾)‘𝑊)‘𝑟) ⊆ ((((DIsoC‘𝐾)‘𝑊)‘𝑟) (((DIsoB‘𝐾)‘𝑊)‘(𝑌 𝑊))))
61 simp13 1262 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝑌𝐵 ∧ ¬ 𝑌 𝑊))
62 simp3r 1259 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝑟 (𝑌 𝑊)) = 𝑌)
633, 4, 5, 6, 7, 8, 38, 39, 40, 41, 42dihvalcq 37124 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝐼𝑌) = ((((DIsoC‘𝐾)‘𝑊)‘𝑟) (((DIsoB‘𝐾)‘𝑊)‘(𝑌 𝑊))))
6422, 61, 33, 62, 63syl112anc 1493 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝐼𝑌) = ((((DIsoC‘𝐾)‘𝑊)‘𝑟) (((DIsoB‘𝐾)‘𝑊)‘(𝑌 𝑊))))
6560, 64sseqtr4d 3801 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (((DIsoC‘𝐾)‘𝑊)‘𝑟) ⊆ (𝐼𝑌))
6636fveq2d 6378 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (((DIsoB‘𝐾)‘𝑊)‘((𝑟 𝑋) 𝑊)) = (((DIsoB‘𝐾)‘𝑊)‘𝑋))
673, 4, 8, 38, 39dihvalb 37125 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) → (𝐼𝑋) = (((DIsoB‘𝐾)‘𝑊)‘𝑋))
6822, 34, 67syl2anc 579 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝐼𝑋) = (((DIsoB‘𝐾)‘𝑊)‘𝑋))
6966, 68eqtr4d 2801 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (((DIsoB‘𝐾)‘𝑊)‘((𝑟 𝑋) 𝑊)) = (𝐼𝑋))
70 simp2 1167 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝐼𝑋) ⊆ (𝐼𝑌))
7169, 70eqsstrd 3798 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (((DIsoB‘𝐾)‘𝑊)‘((𝑟 𝑋) 𝑊)) ⊆ (𝐼𝑌))
723, 6latmcl 17319 . . . . . . . . . . . . . 14 ((𝐾 ∈ Lat ∧ (𝑟 𝑋) ∈ 𝐵𝑊𝐵) → ((𝑟 𝑋) 𝑊) ∈ 𝐵)
7312, 18, 28, 72syl3anc 1490 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → ((𝑟 𝑋) 𝑊) ∈ 𝐵)
743, 4, 6latmle2 17344 . . . . . . . . . . . . . 14 ((𝐾 ∈ Lat ∧ (𝑟 𝑋) ∈ 𝐵𝑊𝐵) → ((𝑟 𝑋) 𝑊) 𝑊)
7512, 18, 28, 74syl3anc 1490 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → ((𝑟 𝑋) 𝑊) 𝑊)
763, 4, 8, 41, 39, 46diblss 37058 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (((𝑟 𝑋) 𝑊) ∈ 𝐵 ∧ ((𝑟 𝑋) 𝑊) 𝑊)) → (((DIsoB‘𝐾)‘𝑊)‘((𝑟 𝑋) 𝑊)) ∈ (LSubSp‘𝑈))
7722, 73, 75, 76syl12anc 865 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (((DIsoB‘𝐾)‘𝑊)‘((𝑟 𝑋) 𝑊)) ∈ (LSubSp‘𝑈))
7848, 77sseldd 3761 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (((DIsoB‘𝐾)‘𝑊)‘((𝑟 𝑋) 𝑊)) ∈ (SubGrp‘𝑈))
793, 8, 38, 41, 46dihlss 37138 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑌𝐵) → (𝐼𝑌) ∈ (LSubSp‘𝑈))
8022, 19, 79syl2anc 579 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝐼𝑌) ∈ (LSubSp‘𝑈))
8148, 80sseldd 3761 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝐼𝑌) ∈ (SubGrp‘𝑈))
8242lsmlub 18343 . . . . . . . . . . 11 (((((DIsoC‘𝐾)‘𝑊)‘𝑟) ∈ (SubGrp‘𝑈) ∧ (((DIsoB‘𝐾)‘𝑊)‘((𝑟 𝑋) 𝑊)) ∈ (SubGrp‘𝑈) ∧ (𝐼𝑌) ∈ (SubGrp‘𝑈)) → (((((DIsoC‘𝐾)‘𝑊)‘𝑟) ⊆ (𝐼𝑌) ∧ (((DIsoB‘𝐾)‘𝑊)‘((𝑟 𝑋) 𝑊)) ⊆ (𝐼𝑌)) ↔ ((((DIsoC‘𝐾)‘𝑊)‘𝑟) (((DIsoB‘𝐾)‘𝑊)‘((𝑟 𝑋) 𝑊))) ⊆ (𝐼𝑌)))
8351, 78, 81, 82syl3anc 1490 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (((((DIsoC‘𝐾)‘𝑊)‘𝑟) ⊆ (𝐼𝑌) ∧ (((DIsoB‘𝐾)‘𝑊)‘((𝑟 𝑋) 𝑊)) ⊆ (𝐼𝑌)) ↔ ((((DIsoC‘𝐾)‘𝑊)‘𝑟) (((DIsoB‘𝐾)‘𝑊)‘((𝑟 𝑋) 𝑊))) ⊆ (𝐼𝑌)))
8465, 71, 83mpbi2and 703 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → ((((DIsoC‘𝐾)‘𝑊)‘𝑟) (((DIsoB‘𝐾)‘𝑊)‘((𝑟 𝑋) 𝑊))) ⊆ (𝐼𝑌))
8544, 84eqsstrd 3798 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝐼‘(𝑟 𝑋)) ⊆ (𝐼𝑌))
863, 4, 8, 38dihord4 37146 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑟 𝑋) ∈ 𝐵 ∧ ¬ (𝑟 𝑋) 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) → ((𝐼‘(𝑟 𝑋)) ⊆ (𝐼𝑌) ↔ (𝑟 𝑋) 𝑌))
8722, 18, 32, 61, 86syl121anc 1494 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → ((𝐼‘(𝑟 𝑋)) ⊆ (𝐼𝑌) ↔ (𝑟 𝑋) 𝑌))
8885, 87mpbid 223 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝑟 𝑋) 𝑌)
893, 4, 12, 13, 18, 19, 21, 88lattrd 17325 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → 𝑋 𝑌)
90893expia 1150 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌)) → (((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌) → 𝑋 𝑌))
9190exp4c 423 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌)) → (𝑟𝐴 → (¬ 𝑟 𝑊 → ((𝑟 (𝑌 𝑊)) = 𝑌𝑋 𝑌))))
9291imp4a 413 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌)) → (𝑟𝐴 → ((¬ 𝑟 𝑊 ∧ (𝑟 (𝑌 𝑊)) = 𝑌) → 𝑋 𝑌)))
9392rexlimdv 3176 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌)) → (∃𝑟𝐴𝑟 𝑊 ∧ (𝑟 (𝑌 𝑊)) = 𝑌) → 𝑋 𝑌))
9410, 93mpd 15 1 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌)) → 𝑋 𝑌)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1107   = wceq 1652  wcel 2155  wrex 3055  wss 3731   class class class wbr 4808  cfv 6067  (class class class)co 6841  Basecbs 16131  lecple 16222  joincjn 17211  meetcmee 17212  Latclat 17312  SubGrpcsubg 17853  LSSumclsm 18314  LModclmod 19131  LSubSpclss 19200  Atomscatm 35151  HLchlt 35238  LHypclh 35872  DVecHcdvh 36966  DIsoBcdib 37026  DIsoCcdic 37060  DIsoHcdih 37116
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-rep 4929  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146  ax-cnex 10244  ax-resscn 10245  ax-1cn 10246  ax-icn 10247  ax-addcl 10248  ax-addrcl 10249  ax-mulcl 10250  ax-mulrcl 10251  ax-mulcom 10252  ax-addass 10253  ax-mulass 10254  ax-distr 10255  ax-i2m1 10256  ax-1ne0 10257  ax-1rid 10258  ax-rnegex 10259  ax-rrecex 10260  ax-cnre 10261  ax-pre-lttri 10262  ax-pre-lttrn 10263  ax-pre-ltadd 10264  ax-pre-mulgt0 10265  ax-riotaBAD 34841
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-pss 3747  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-tp 4338  df-op 4340  df-uni 4594  df-int 4633  df-iun 4677  df-iin 4678  df-br 4809  df-opab 4871  df-mpt 4888  df-tr 4911  df-id 5184  df-eprel 5189  df-po 5197  df-so 5198  df-fr 5235  df-we 5237  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-pred 5864  df-ord 5910  df-on 5911  df-lim 5912  df-suc 5913  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-riota 6802  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-om 7263  df-1st 7365  df-2nd 7366  df-tpos 7554  df-undef 7601  df-wrecs 7609  df-recs 7671  df-rdg 7709  df-1o 7763  df-oadd 7767  df-er 7946  df-map 8061  df-en 8160  df-dom 8161  df-sdom 8162  df-fin 8163  df-pnf 10329  df-mnf 10330  df-xr 10331  df-ltxr 10332  df-le 10333  df-sub 10521  df-neg 10522  df-nn 11274  df-2 11334  df-3 11335  df-4 11336  df-5 11337  df-6 11338  df-n0 11538  df-z 11624  df-uz 11886  df-fz 12533  df-struct 16133  df-ndx 16134  df-slot 16135  df-base 16137  df-sets 16138  df-ress 16139  df-plusg 16228  df-mulr 16229  df-sca 16231  df-vsca 16232  df-0g 16369  df-proset 17195  df-poset 17213  df-plt 17225  df-lub 17241  df-glb 17242  df-join 17243  df-meet 17244  df-p0 17306  df-p1 17307  df-lat 17313  df-clat 17375  df-mgm 17509  df-sgrp 17551  df-mnd 17562  df-submnd 17603  df-grp 17693  df-minusg 17694  df-sbg 17695  df-subg 17856  df-cntz 18014  df-lsm 18316  df-cmn 18460  df-abl 18461  df-mgp 18756  df-ur 18768  df-ring 18815  df-oppr 18889  df-dvdsr 18907  df-unit 18908  df-invr 18938  df-dvr 18949  df-drng 19017  df-lmod 19133  df-lss 19201  df-lsp 19243  df-lvec 19374  df-oposet 35064  df-ol 35066  df-oml 35067  df-covers 35154  df-ats 35155  df-atl 35186  df-cvlat 35210  df-hlat 35239  df-llines 35386  df-lplanes 35387  df-lvols 35388  df-lines 35389  df-psubsp 35391  df-pmap 35392  df-padd 35684  df-lhyp 35876  df-laut 35877  df-ldil 35992  df-ltrn 35993  df-trl 36047  df-tendo 36643  df-edring 36645  df-disoa 36917  df-dvech 36967  df-dib 37027  df-dic 37061  df-dih 37117
This theorem is referenced by:  dihord5a  37151
  Copyright terms: Public domain W3C validator