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 40974
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 1188 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
2 simpl3 1190 . . 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 39736 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) → ∃𝑟𝐴𝑟 𝑊 ∧ (𝑟 (𝑌 𝑊)) = 𝑌))
101, 2, 9syl2anc 582 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌)) → ∃𝑟𝐴𝑟 𝑊 ∧ (𝑟 (𝑌 𝑊)) = 𝑌))
11 simp11l 1281 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → 𝐾 ∈ HL)
1211hllatd 39075 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → 𝐾 ∈ Lat)
13 simp12l 1283 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → 𝑋𝐵)
14 simp3ll 1241 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → 𝑟𝐴)
153, 7atbase 39000 . . . . . . . . 9 (𝑟𝐴𝑟𝐵)
1614, 15syl 17 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → 𝑟𝐵)
173, 5latjcl 18459 . . . . . . . 8 ((𝐾 ∈ Lat ∧ 𝑟𝐵𝑋𝐵) → (𝑟 𝑋) ∈ 𝐵)
1812, 16, 13, 17syl3anc 1368 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝑟 𝑋) ∈ 𝐵)
19 simp13l 1285 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → 𝑌𝐵)
203, 4, 5latlej2 18469 . . . . . . . 8 ((𝐾 ∈ Lat ∧ 𝑟𝐵𝑋𝐵) → 𝑋 (𝑟 𝑋))
2112, 16, 13, 20syl3anc 1368 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → 𝑋 (𝑟 𝑋))
22 simp11 1200 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
23 simp3lr 1242 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → ¬ 𝑟 𝑊)
243, 4, 5latlej1 18468 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ 𝑟𝐵𝑋𝐵) → 𝑟 (𝑟 𝑋))
2512, 16, 13, 24syl3anc 1368 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → 𝑟 (𝑟 𝑋))
26 simp11r 1282 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → 𝑊𝐻)
273, 8lhpbase 39710 . . . . . . . . . . . . . 14 (𝑊𝐻𝑊𝐵)
2826, 27syl 17 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → 𝑊𝐵)
293, 4lattr 18464 . . . . . . . . . . . . 13 ((𝐾 ∈ Lat ∧ (𝑟𝐵 ∧ (𝑟 𝑋) ∈ 𝐵𝑊𝐵)) → ((𝑟 (𝑟 𝑋) ∧ (𝑟 𝑋) 𝑊) → 𝑟 𝑊))
3012, 16, 18, 28, 29syl13anc 1369 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → ((𝑟 (𝑟 𝑋) ∧ (𝑟 𝑋) 𝑊) → 𝑟 𝑊))
3125, 30mpand 693 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → ((𝑟 𝑋) 𝑊𝑟 𝑊))
3223, 31mtod 197 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → ¬ (𝑟 𝑋) 𝑊)
33 simp3l 1198 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝑟𝐴 ∧ ¬ 𝑟 𝑊))
34 simp12 1201 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝑋𝐵𝑋 𝑊))
353, 4, 5, 6, 7, 8lhple 39754 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑋𝐵𝑋 𝑊)) → ((𝑟 𝑋) 𝑊) = 𝑋)
3622, 33, 34, 35syl3anc 1368 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → ((𝑟 𝑋) 𝑊) = 𝑋)
3736oveq2d 7432 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝑟 ((𝑟 𝑋) 𝑊)) = (𝑟 𝑋))
38 dihord5apre.i . . . . . . . . . . 11 𝐼 = ((DIsoH‘𝐾)‘𝑊)
39 eqid 2726 . . . . . . . . . . 11 ((DIsoB‘𝐾)‘𝑊) = ((DIsoB‘𝐾)‘𝑊)
40 eqid 2726 . . . . . . . . . . 11 ((DIsoC‘𝐾)‘𝑊) = ((DIsoC‘𝐾)‘𝑊)
41 dihord5apre.u . . . . . . . . . . 11 𝑈 = ((DVecH‘𝐾)‘𝑊)
42 dihord5apre.s . . . . . . . . . . 11 = (LSSum‘𝑈)
433, 4, 5, 6, 7, 8, 38, 39, 40, 41, 42dihvalcq 40948 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑟 𝑋) ∈ 𝐵 ∧ ¬ (𝑟 𝑋) 𝑊) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 ((𝑟 𝑋) 𝑊)) = (𝑟 𝑋))) → (𝐼‘(𝑟 𝑋)) = ((((DIsoC‘𝐾)‘𝑊)‘𝑟) (((DIsoB‘𝐾)‘𝑊)‘((𝑟 𝑋) 𝑊))))
4422, 18, 32, 33, 37, 43syl122anc 1376 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝐼‘(𝑟 𝑋)) = ((((DIsoC‘𝐾)‘𝑊)‘𝑟) (((DIsoB‘𝐾)‘𝑊)‘((𝑟 𝑋) 𝑊))))
458, 41, 22dvhlmod 40822 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → 𝑈 ∈ LMod)
46 eqid 2726 . . . . . . . . . . . . . . 15 (LSubSp‘𝑈) = (LSubSp‘𝑈)
4746lsssssubg 20931 . . . . . . . . . . . . . 14 (𝑈 ∈ LMod → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈))
4845, 47syl 17 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈))
494, 7, 8, 41, 40, 46diclss 40905 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑟𝐴 ∧ ¬ 𝑟 𝑊)) → (((DIsoC‘𝐾)‘𝑊)‘𝑟) ∈ (LSubSp‘𝑈))
5022, 33, 49syl2anc 582 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (((DIsoC‘𝐾)‘𝑊)‘𝑟) ∈ (LSubSp‘𝑈))
5148, 50sseldd 3979 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (((DIsoC‘𝐾)‘𝑊)‘𝑟) ∈ (SubGrp‘𝑈))
523, 6latmcl 18460 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ 𝑌𝐵𝑊𝐵) → (𝑌 𝑊) ∈ 𝐵)
5312, 19, 28, 52syl3anc 1368 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝑌 𝑊) ∈ 𝐵)
543, 4, 6latmle2 18485 . . . . . . . . . . . . . . 15 ((𝐾 ∈ Lat ∧ 𝑌𝐵𝑊𝐵) → (𝑌 𝑊) 𝑊)
5512, 19, 28, 54syl3anc 1368 . . . . . . . . . . . . . 14 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝑌 𝑊) 𝑊)
563, 4, 8, 41, 39, 46diblss 40882 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑌 𝑊) ∈ 𝐵 ∧ (𝑌 𝑊) 𝑊)) → (((DIsoB‘𝐾)‘𝑊)‘(𝑌 𝑊)) ∈ (LSubSp‘𝑈))
5722, 53, 55, 56syl12anc 835 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (((DIsoB‘𝐾)‘𝑊)‘(𝑌 𝑊)) ∈ (LSubSp‘𝑈))
5848, 57sseldd 3979 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (((DIsoB‘𝐾)‘𝑊)‘(𝑌 𝑊)) ∈ (SubGrp‘𝑈))
5942lsmub1 19651 . . . . . . . . . . . 12 (((((DIsoC‘𝐾)‘𝑊)‘𝑟) ∈ (SubGrp‘𝑈) ∧ (((DIsoB‘𝐾)‘𝑊)‘(𝑌 𝑊)) ∈ (SubGrp‘𝑈)) → (((DIsoC‘𝐾)‘𝑊)‘𝑟) ⊆ ((((DIsoC‘𝐾)‘𝑊)‘𝑟) (((DIsoB‘𝐾)‘𝑊)‘(𝑌 𝑊))))
6051, 58, 59syl2anc 582 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (((DIsoC‘𝐾)‘𝑊)‘𝑟) ⊆ ((((DIsoC‘𝐾)‘𝑊)‘𝑟) (((DIsoB‘𝐾)‘𝑊)‘(𝑌 𝑊))))
61 simp13 1202 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝑌𝐵 ∧ ¬ 𝑌 𝑊))
62 simp3r 1199 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝑟 (𝑌 𝑊)) = 𝑌)
633, 4, 5, 6, 7, 8, 38, 39, 40, 41, 42dihvalcq 40948 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝐼𝑌) = ((((DIsoC‘𝐾)‘𝑊)‘𝑟) (((DIsoB‘𝐾)‘𝑊)‘(𝑌 𝑊))))
6422, 61, 33, 62, 63syl112anc 1371 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝐼𝑌) = ((((DIsoC‘𝐾)‘𝑊)‘𝑟) (((DIsoB‘𝐾)‘𝑊)‘(𝑌 𝑊))))
6560, 64sseqtrrd 4020 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (((DIsoC‘𝐾)‘𝑊)‘𝑟) ⊆ (𝐼𝑌))
6636fveq2d 6897 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (((DIsoB‘𝐾)‘𝑊)‘((𝑟 𝑋) 𝑊)) = (((DIsoB‘𝐾)‘𝑊)‘𝑋))
673, 4, 8, 38, 39dihvalb 40949 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊)) → (𝐼𝑋) = (((DIsoB‘𝐾)‘𝑊)‘𝑋))
6822, 34, 67syl2anc 582 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝐼𝑋) = (((DIsoB‘𝐾)‘𝑊)‘𝑋))
6966, 68eqtr4d 2769 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (((DIsoB‘𝐾)‘𝑊)‘((𝑟 𝑋) 𝑊)) = (𝐼𝑋))
70 simp2 1134 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝐼𝑋) ⊆ (𝐼𝑌))
7169, 70eqsstrd 4017 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (((DIsoB‘𝐾)‘𝑊)‘((𝑟 𝑋) 𝑊)) ⊆ (𝐼𝑌))
723, 6latmcl 18460 . . . . . . . . . . . . . 14 ((𝐾 ∈ Lat ∧ (𝑟 𝑋) ∈ 𝐵𝑊𝐵) → ((𝑟 𝑋) 𝑊) ∈ 𝐵)
7312, 18, 28, 72syl3anc 1368 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → ((𝑟 𝑋) 𝑊) ∈ 𝐵)
743, 4, 6latmle2 18485 . . . . . . . . . . . . . 14 ((𝐾 ∈ Lat ∧ (𝑟 𝑋) ∈ 𝐵𝑊𝐵) → ((𝑟 𝑋) 𝑊) 𝑊)
7512, 18, 28, 74syl3anc 1368 . . . . . . . . . . . . 13 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → ((𝑟 𝑋) 𝑊) 𝑊)
763, 4, 8, 41, 39, 46diblss 40882 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (((𝑟 𝑋) 𝑊) ∈ 𝐵 ∧ ((𝑟 𝑋) 𝑊) 𝑊)) → (((DIsoB‘𝐾)‘𝑊)‘((𝑟 𝑋) 𝑊)) ∈ (LSubSp‘𝑈))
7722, 73, 75, 76syl12anc 835 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (((DIsoB‘𝐾)‘𝑊)‘((𝑟 𝑋) 𝑊)) ∈ (LSubSp‘𝑈))
7848, 77sseldd 3979 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (((DIsoB‘𝐾)‘𝑊)‘((𝑟 𝑋) 𝑊)) ∈ (SubGrp‘𝑈))
793, 8, 38, 41, 46dihlss 40962 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑌𝐵) → (𝐼𝑌) ∈ (LSubSp‘𝑈))
8022, 19, 79syl2anc 582 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝐼𝑌) ∈ (LSubSp‘𝑈))
8148, 80sseldd 3979 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝐼𝑌) ∈ (SubGrp‘𝑈))
8242lsmlub 19658 . . . . . . . . . . 11 (((((DIsoC‘𝐾)‘𝑊)‘𝑟) ∈ (SubGrp‘𝑈) ∧ (((DIsoB‘𝐾)‘𝑊)‘((𝑟 𝑋) 𝑊)) ∈ (SubGrp‘𝑈) ∧ (𝐼𝑌) ∈ (SubGrp‘𝑈)) → (((((DIsoC‘𝐾)‘𝑊)‘𝑟) ⊆ (𝐼𝑌) ∧ (((DIsoB‘𝐾)‘𝑊)‘((𝑟 𝑋) 𝑊)) ⊆ (𝐼𝑌)) ↔ ((((DIsoC‘𝐾)‘𝑊)‘𝑟) (((DIsoB‘𝐾)‘𝑊)‘((𝑟 𝑋) 𝑊))) ⊆ (𝐼𝑌)))
8351, 78, 81, 82syl3anc 1368 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (((((DIsoC‘𝐾)‘𝑊)‘𝑟) ⊆ (𝐼𝑌) ∧ (((DIsoB‘𝐾)‘𝑊)‘((𝑟 𝑋) 𝑊)) ⊆ (𝐼𝑌)) ↔ ((((DIsoC‘𝐾)‘𝑊)‘𝑟) (((DIsoB‘𝐾)‘𝑊)‘((𝑟 𝑋) 𝑊))) ⊆ (𝐼𝑌)))
8465, 71, 83mpbi2and 710 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → ((((DIsoC‘𝐾)‘𝑊)‘𝑟) (((DIsoB‘𝐾)‘𝑊)‘((𝑟 𝑋) 𝑊))) ⊆ (𝐼𝑌))
8544, 84eqsstrd 4017 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝐼‘(𝑟 𝑋)) ⊆ (𝐼𝑌))
863, 4, 8, 38dihord4 40970 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑟 𝑋) ∈ 𝐵 ∧ ¬ (𝑟 𝑋) 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) → ((𝐼‘(𝑟 𝑋)) ⊆ (𝐼𝑌) ↔ (𝑟 𝑋) 𝑌))
8722, 18, 32, 61, 86syl121anc 1372 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → ((𝐼‘(𝑟 𝑋)) ⊆ (𝐼𝑌) ↔ (𝑟 𝑋) 𝑌))
8885, 87mpbid 231 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → (𝑟 𝑋) 𝑌)
893, 4, 12, 13, 18, 19, 21, 88lattrd 18466 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌) ∧ ((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌)) → 𝑋 𝑌)
90893expia 1118 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌)) → (((𝑟𝐴 ∧ ¬ 𝑟 𝑊) ∧ (𝑟 (𝑌 𝑊)) = 𝑌) → 𝑋 𝑌))
9190exp4c 431 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌)) → (𝑟𝐴 → (¬ 𝑟 𝑊 → ((𝑟 (𝑌 𝑊)) = 𝑌𝑋 𝑌))))
9291imp4a 421 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌)) → (𝑟𝐴 → ((¬ 𝑟 𝑊 ∧ (𝑟 (𝑌 𝑊)) = 𝑌) → 𝑋 𝑌)))
9392rexlimdv 3143 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌)) → (∃𝑟𝐴𝑟 𝑊 ∧ (𝑟 (𝑌 𝑊)) = 𝑌) → 𝑋 𝑌))
9410, 93mpd 15 1 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑋𝐵𝑋 𝑊) ∧ (𝑌𝐵 ∧ ¬ 𝑌 𝑊)) ∧ (𝐼𝑋) ⊆ (𝐼𝑌)) → 𝑋 𝑌)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  w3a 1084   = wceq 1534  wcel 2099  wrex 3060  wss 3946   class class class wbr 5145  cfv 6546  (class class class)co 7416  Basecbs 17208  lecple 17268  joincjn 18331  meetcmee 18332  Latclat 18451  SubGrpcsubg 19110  LSSumclsm 19628  LModclmod 20832  LSubSpclss 20904  Atomscatm 38974  HLchlt 39061  LHypclh 39696  DVecHcdvh 40790  DIsoBcdib 40850  DIsoCcdic 40884  DIsoHcdih 40940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5282  ax-sep 5296  ax-nul 5303  ax-pow 5361  ax-pr 5425  ax-un 7738  ax-cnex 11205  ax-resscn 11206  ax-1cn 11207  ax-icn 11208  ax-addcl 11209  ax-addrcl 11210  ax-mulcl 11211  ax-mulrcl 11212  ax-mulcom 11213  ax-addass 11214  ax-mulass 11215  ax-distr 11216  ax-i2m1 11217  ax-1ne0 11218  ax-1rid 11219  ax-rnegex 11220  ax-rrecex 11221  ax-cnre 11222  ax-pre-lttri 11223  ax-pre-lttrn 11224  ax-pre-ltadd 11225  ax-pre-mulgt0 11226  ax-riotaBAD 38664
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4323  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4906  df-int 4947  df-iun 4995  df-iin 4996  df-br 5146  df-opab 5208  df-mpt 5229  df-tr 5263  df-id 5572  df-eprel 5578  df-po 5586  df-so 5587  df-fr 5629  df-we 5631  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-pred 6304  df-ord 6371  df-on 6372  df-lim 6373  df-suc 6374  df-iota 6498  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-riota 7372  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7869  df-1st 7995  df-2nd 7996  df-tpos 8233  df-undef 8280  df-frecs 8288  df-wrecs 8319  df-recs 8393  df-rdg 8432  df-1o 8488  df-er 8726  df-map 8849  df-en 8967  df-dom 8968  df-sdom 8969  df-fin 8970  df-pnf 11291  df-mnf 11292  df-xr 11293  df-ltxr 11294  df-le 11295  df-sub 11487  df-neg 11488  df-nn 12259  df-2 12321  df-3 12322  df-4 12323  df-5 12324  df-6 12325  df-n0 12519  df-z 12605  df-uz 12869  df-fz 13533  df-struct 17144  df-sets 17161  df-slot 17179  df-ndx 17191  df-base 17209  df-ress 17238  df-plusg 17274  df-mulr 17275  df-sca 17277  df-vsca 17278  df-0g 17451  df-proset 18315  df-poset 18333  df-plt 18350  df-lub 18366  df-glb 18367  df-join 18368  df-meet 18369  df-p0 18445  df-p1 18446  df-lat 18452  df-clat 18519  df-mgm 18628  df-sgrp 18707  df-mnd 18723  df-submnd 18769  df-grp 18926  df-minusg 18927  df-sbg 18928  df-subg 19113  df-cntz 19307  df-lsm 19630  df-cmn 19776  df-abl 19777  df-mgp 20114  df-rng 20132  df-ur 20161  df-ring 20214  df-oppr 20312  df-dvdsr 20335  df-unit 20336  df-invr 20366  df-dvr 20379  df-drng 20705  df-lmod 20834  df-lss 20905  df-lsp 20945  df-lvec 21077  df-oposet 38887  df-ol 38889  df-oml 38890  df-covers 38977  df-ats 38978  df-atl 39009  df-cvlat 39033  df-hlat 39062  df-llines 39210  df-lplanes 39211  df-lvols 39212  df-lines 39213  df-psubsp 39215  df-pmap 39216  df-padd 39508  df-lhyp 39700  df-laut 39701  df-ldil 39816  df-ltrn 39817  df-trl 39871  df-tendo 40467  df-edring 40469  df-disoa 40741  df-dvech 40791  df-dib 40851  df-dic 40885  df-dih 40941
This theorem is referenced by:  dihord5a  40975
  Copyright terms: Public domain W3C validator