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

Theorem dih1 40945
Description: The value of isomorphism H at the lattice unity is the set of all vectors. (Contributed by NM, 13-Mar-2014.)
Hypotheses
Ref Expression
dih1.m 1 = (1.‘𝐾)
dih1.h 𝐻 = (LHyp‘𝐾)
dih1.i 𝐼 = ((DIsoH‘𝐾)‘𝑊)
dih1.u 𝑈 = ((DVecH‘𝐾)‘𝑊)
dih1.v 𝑉 = (Base‘𝑈)
Assertion
Ref Expression
dih1 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (𝐼1 ) = 𝑉)

Proof of Theorem dih1
Dummy variables 𝑓 𝑔 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dih1.h . . 3 𝐻 = (LHyp‘𝐾)
2 dih1.i . . 3 𝐼 = ((DIsoH‘𝐾)‘𝑊)
31, 2dihvalrel 40938 . 2 ((𝐾 ∈ HL ∧ 𝑊𝐻) → Rel (𝐼1 ))
4 relxp 5699 . . 3 Rel (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊))
5 eqid 2725 . . . . 5 ((LTrn‘𝐾)‘𝑊) = ((LTrn‘𝐾)‘𝑊)
6 eqid 2725 . . . . 5 ((TEndo‘𝐾)‘𝑊) = ((TEndo‘𝐾)‘𝑊)
7 dih1.u . . . . 5 𝑈 = ((DVecH‘𝐾)‘𝑊)
8 dih1.v . . . . 5 𝑉 = (Base‘𝑈)
91, 5, 6, 7, 8dvhvbase 40746 . . . 4 ((𝐾 ∈ HL ∧ 𝑊𝐻) → 𝑉 = (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊)))
109releqd 5783 . . 3 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (Rel 𝑉 ↔ Rel (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊))))
114, 10mpbiri 257 . 2 ((𝐾 ∈ HL ∧ 𝑊𝐻) → Rel 𝑉)
12 id 22 . 2 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (𝐾 ∈ HL ∧ 𝑊𝐻))
13 hlop 39020 . . . . . . . 8 (𝐾 ∈ HL → 𝐾 ∈ OP)
1413ad2antrr 724 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))) → 𝐾 ∈ OP)
15 simpl 481 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
16 simprl 769 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))) → 𝑓 ∈ ((LTrn‘𝐾)‘𝑊))
17 simprr 771 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))) → 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))
18 eqid 2725 . . . . . . . . . . . . . 14 (le‘𝐾) = (le‘𝐾)
19 eqid 2725 . . . . . . . . . . . . . 14 (oc‘𝐾) = (oc‘𝐾)
20 eqid 2725 . . . . . . . . . . . . . 14 (Atoms‘𝐾) = (Atoms‘𝐾)
2118, 19, 20, 1lhpocnel 39677 . . . . . . . . . . . . 13 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (((oc‘𝐾)‘𝑊) ∈ (Atoms‘𝐾) ∧ ¬ ((oc‘𝐾)‘𝑊)(le‘𝐾)𝑊))
2221adantr 479 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))) → (((oc‘𝐾)‘𝑊) ∈ (Atoms‘𝐾) ∧ ¬ ((oc‘𝐾)‘𝑊)(le‘𝐾)𝑊))
23 eqid 2725 . . . . . . . . . . . . 13 (𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑔‘((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊)) = (𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑔‘((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊))
2418, 20, 1, 5, 23ltrniotacl 40238 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (((oc‘𝐾)‘𝑊) ∈ (Atoms‘𝐾) ∧ ¬ ((oc‘𝐾)‘𝑊)(le‘𝐾)𝑊) ∧ (((oc‘𝐾)‘𝑊) ∈ (Atoms‘𝐾) ∧ ¬ ((oc‘𝐾)‘𝑊)(le‘𝐾)𝑊)) → (𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑔‘((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊)) ∈ ((LTrn‘𝐾)‘𝑊))
2515, 22, 22, 24syl3anc 1368 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))) → (𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑔‘((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊)) ∈ ((LTrn‘𝐾)‘𝑊))
261, 5, 6tendocl 40426 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊) ∧ (𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑔‘((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊)) ∈ ((LTrn‘𝐾)‘𝑊)) → (𝑠‘(𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑔‘((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊))) ∈ ((LTrn‘𝐾)‘𝑊))
2715, 17, 25, 26syl3anc 1368 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))) → (𝑠‘(𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑔‘((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊))) ∈ ((LTrn‘𝐾)‘𝑊))
281, 5ltrncnv 39805 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑠‘(𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑔‘((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊))) ∈ ((LTrn‘𝐾)‘𝑊)) → (𝑠‘(𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑔‘((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊))) ∈ ((LTrn‘𝐾)‘𝑊))
2927, 28syldan 589 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))) → (𝑠‘(𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑔‘((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊))) ∈ ((LTrn‘𝐾)‘𝑊))
301, 5ltrnco 40378 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ∧ (𝑠‘(𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑔‘((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊))) ∈ ((LTrn‘𝐾)‘𝑊)) → (𝑓(𝑠‘(𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑔‘((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊)))) ∈ ((LTrn‘𝐾)‘𝑊))
3115, 16, 29, 30syl3anc 1368 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))) → (𝑓(𝑠‘(𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑔‘((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊)))) ∈ ((LTrn‘𝐾)‘𝑊))
32 eqid 2725 . . . . . . . . 9 (Base‘𝐾) = (Base‘𝐾)
33 eqid 2725 . . . . . . . . 9 ((trL‘𝐾)‘𝑊) = ((trL‘𝐾)‘𝑊)
3432, 1, 5, 33trlcl 39823 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓(𝑠‘(𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑔‘((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊)))) ∈ ((LTrn‘𝐾)‘𝑊)) → (((trL‘𝐾)‘𝑊)‘(𝑓(𝑠‘(𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑔‘((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊))))) ∈ (Base‘𝐾))
3531, 34syldan 589 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))) → (((trL‘𝐾)‘𝑊)‘(𝑓(𝑠‘(𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑔‘((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊))))) ∈ (Base‘𝐾))
36 dih1.m . . . . . . . 8 1 = (1.‘𝐾)
3732, 18, 36ople1 38849 . . . . . . 7 ((𝐾 ∈ OP ∧ (((trL‘𝐾)‘𝑊)‘(𝑓(𝑠‘(𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑔‘((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊))))) ∈ (Base‘𝐾)) → (((trL‘𝐾)‘𝑊)‘(𝑓(𝑠‘(𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑔‘((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊)))))(le‘𝐾) 1 )
3814, 35, 37syl2anc 582 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))) → (((trL‘𝐾)‘𝑊)‘(𝑓(𝑠‘(𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑔‘((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊)))))(le‘𝐾) 1 )
3938ex 411 . . . . 5 ((𝐾 ∈ HL ∧ 𝑊𝐻) → ((𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊)) → (((trL‘𝐾)‘𝑊)‘(𝑓(𝑠‘(𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑔‘((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊)))))(le‘𝐾) 1 ))
4039pm4.71d 560 . . . 4 ((𝐾 ∈ HL ∧ 𝑊𝐻) → ((𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊)) ↔ ((𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊)) ∧ (((trL‘𝐾)‘𝑊)‘(𝑓(𝑠‘(𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑔‘((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊)))))(le‘𝐾) 1 )))
419eleq2d 2811 . . . . 5 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (⟨𝑓, 𝑠⟩ ∈ 𝑉 ↔ ⟨𝑓, 𝑠⟩ ∈ (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊))))
42 opelxp 5717 . . . . 5 (⟨𝑓, 𝑠⟩ ∈ (((LTrn‘𝐾)‘𝑊) × ((TEndo‘𝐾)‘𝑊)) ↔ (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊)))
4341, 42bitrdi 286 . . . 4 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (⟨𝑓, 𝑠⟩ ∈ 𝑉 ↔ (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊))))
4413adantr 479 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑊𝐻) → 𝐾 ∈ OP)
4532, 36op1cl 38843 . . . . . 6 (𝐾 ∈ OP → 1 ∈ (Base‘𝐾))
4644, 45syl 17 . . . . 5 ((𝐾 ∈ HL ∧ 𝑊𝐻) → 1 ∈ (Base‘𝐾))
47 hlpos 39024 . . . . . . 7 (𝐾 ∈ HL → 𝐾 ∈ Poset)
4847adantr 479 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑊𝐻) → 𝐾 ∈ Poset)
4932, 1lhpbase 39657 . . . . . . 7 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
5049adantl 480 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑊𝐻) → 𝑊 ∈ (Base‘𝐾))
51 eqid 2725 . . . . . . 7 ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
5236, 51, 1lhp1cvr 39658 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑊𝐻) → 𝑊( ⋖ ‘𝐾) 1 )
5332, 18, 51cvrnle 38938 . . . . . 6 (((𝐾 ∈ Poset ∧ 𝑊 ∈ (Base‘𝐾) ∧ 1 ∈ (Base‘𝐾)) ∧ 𝑊( ⋖ ‘𝐾) 1 ) → ¬ 1 (le‘𝐾)𝑊)
5448, 50, 46, 52, 53syl31anc 1370 . . . . 5 ((𝐾 ∈ HL ∧ 𝑊𝐻) → ¬ 1 (le‘𝐾)𝑊)
55 hlol 39019 . . . . . . . 8 (𝐾 ∈ HL → 𝐾 ∈ OL)
56 eqid 2725 . . . . . . . . 9 (meet‘𝐾) = (meet‘𝐾)
5732, 56, 36olm12 38886 . . . . . . . 8 ((𝐾 ∈ OL ∧ 𝑊 ∈ (Base‘𝐾)) → ( 1 (meet‘𝐾)𝑊) = 𝑊)
5855, 49, 57syl2an 594 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑊𝐻) → ( 1 (meet‘𝐾)𝑊) = 𝑊)
5958oveq2d 7439 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (((oc‘𝐾)‘𝑊)(join‘𝐾)( 1 (meet‘𝐾)𝑊)) = (((oc‘𝐾)‘𝑊)(join‘𝐾)𝑊))
60 hllat 39021 . . . . . . . 8 (𝐾 ∈ HL → 𝐾 ∈ Lat)
6160adantr 479 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑊𝐻) → 𝐾 ∈ Lat)
6232, 19opoccl 38852 . . . . . . . 8 ((𝐾 ∈ OP ∧ 𝑊 ∈ (Base‘𝐾)) → ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾))
6313, 49, 62syl2an 594 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑊𝐻) → ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾))
64 eqid 2725 . . . . . . . 8 (join‘𝐾) = (join‘𝐾)
6532, 64latjcom 18467 . . . . . . 7 ((𝐾 ∈ Lat ∧ ((oc‘𝐾)‘𝑊) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → (((oc‘𝐾)‘𝑊)(join‘𝐾)𝑊) = (𝑊(join‘𝐾)((oc‘𝐾)‘𝑊)))
6661, 63, 50, 65syl3anc 1368 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (((oc‘𝐾)‘𝑊)(join‘𝐾)𝑊) = (𝑊(join‘𝐾)((oc‘𝐾)‘𝑊)))
6732, 19, 64, 36opexmid 38865 . . . . . . 7 ((𝐾 ∈ OP ∧ 𝑊 ∈ (Base‘𝐾)) → (𝑊(join‘𝐾)((oc‘𝐾)‘𝑊)) = 1 )
6813, 49, 67syl2an 594 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (𝑊(join‘𝐾)((oc‘𝐾)‘𝑊)) = 1 )
6959, 66, 683eqtrd 2769 . . . . 5 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (((oc‘𝐾)‘𝑊)(join‘𝐾)( 1 (meet‘𝐾)𝑊)) = 1 )
70 eqid 2725 . . . . . 6 ((oc‘𝐾)‘𝑊) = ((oc‘𝐾)‘𝑊)
71 vex 3465 . . . . . 6 𝑓 ∈ V
72 vex 3465 . . . . . 6 𝑠 ∈ V
7332, 18, 64, 56, 20, 1, 70, 5, 33, 6, 2, 23, 71, 72dihopelvalc 40908 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ( 1 ∈ (Base‘𝐾) ∧ ¬ 1 (le‘𝐾)𝑊) ∧ ((((oc‘𝐾)‘𝑊) ∈ (Atoms‘𝐾) ∧ ¬ ((oc‘𝐾)‘𝑊)(le‘𝐾)𝑊) ∧ (((oc‘𝐾)‘𝑊)(join‘𝐾)( 1 (meet‘𝐾)𝑊)) = 1 )) → (⟨𝑓, 𝑠⟩ ∈ (𝐼1 ) ↔ ((𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊)) ∧ (((trL‘𝐾)‘𝑊)‘(𝑓(𝑠‘(𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑔‘((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊)))))(le‘𝐾) 1 )))
7412, 46, 54, 21, 69, 73syl122anc 1376 . . . 4 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (⟨𝑓, 𝑠⟩ ∈ (𝐼1 ) ↔ ((𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ∧ 𝑠 ∈ ((TEndo‘𝐾)‘𝑊)) ∧ (((trL‘𝐾)‘𝑊)‘(𝑓(𝑠‘(𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑔‘((oc‘𝐾)‘𝑊)) = ((oc‘𝐾)‘𝑊)))))(le‘𝐾) 1 )))
7540, 43, 743bitr4rd 311 . . 3 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (⟨𝑓, 𝑠⟩ ∈ (𝐼1 ) ↔ ⟨𝑓, 𝑠⟩ ∈ 𝑉))
7675eqrelrdv2 5800 . 2 (((Rel (𝐼1 ) ∧ Rel 𝑉) ∧ (𝐾 ∈ HL ∧ 𝑊𝐻)) → (𝐼1 ) = 𝑉)
773, 11, 12, 76syl21anc 836 1 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (𝐼1 ) = 𝑉)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394   = wceq 1533  wcel 2098  cop 4638   class class class wbr 5152   × cxp 5679  ccnv 5680  ccom 5685  Rel wrel 5686  cfv 6553  crio 7378  (class class class)co 7423  Basecbs 17208  lecple 17268  occoc 17269  Posetcpo 18327  joincjn 18331  meetcmee 18332  1.cp1 18444  Latclat 18451  OPcops 38830  OLcol 38832  ccvr 38920  Atomscatm 38921  HLchlt 39008  LHypclh 39643  LTrncltrn 39760  trLctrl 39817  TEndoctendo 40411  DVecHcdvh 40737  DIsoHcdih 40887
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5368  ax-pr 5432  ax-un 7745  ax-cnex 11210  ax-resscn 11211  ax-1cn 11212  ax-icn 11213  ax-addcl 11214  ax-addrcl 11215  ax-mulcl 11216  ax-mulrcl 11217  ax-mulcom 11218  ax-addass 11219  ax-mulass 11220  ax-distr 11221  ax-i2m1 11222  ax-1ne0 11223  ax-1rid 11224  ax-rnegex 11225  ax-rrecex 11226  ax-cnre 11227  ax-pre-lttri 11228  ax-pre-lttrn 11229  ax-pre-ltadd 11230  ax-pre-mulgt0 11231  ax-riotaBAD 38611
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4325  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-tp 4637  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-iin 5003  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5579  df-eprel 5585  df-po 5593  df-so 5594  df-fr 5636  df-we 5638  df-xp 5687  df-rel 5688  df-cnv 5689  df-co 5690  df-dm 5691  df-rn 5692  df-res 5693  df-ima 5694  df-pred 6311  df-ord 6378  df-on 6379  df-lim 6380  df-suc 6381  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7379  df-ov 7426  df-oprab 7427  df-mpo 7428  df-om 7876  df-1st 8002  df-2nd 8003  df-tpos 8240  df-undef 8287  df-frecs 8295  df-wrecs 8326  df-recs 8400  df-rdg 8439  df-1o 8495  df-er 8733  df-map 8856  df-en 8974  df-dom 8975  df-sdom 8976  df-fin 8977  df-pnf 11296  df-mnf 11297  df-xr 11298  df-ltxr 11299  df-le 11300  df-sub 11492  df-neg 11493  df-nn 12260  df-2 12322  df-3 12323  df-4 12324  df-5 12325  df-6 12326  df-n0 12520  df-z 12606  df-uz 12870  df-fz 13534  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 19112  df-cntz 19306  df-lsm 19629  df-cmn 19775  df-abl 19776  df-mgp 20113  df-rng 20131  df-ur 20160  df-ring 20213  df-oppr 20311  df-dvdsr 20334  df-unit 20335  df-invr 20365  df-dvr 20378  df-drng 20666  df-lmod 20785  df-lss 20856  df-lsp 20896  df-lvec 21028  df-oposet 38834  df-ol 38836  df-oml 38837  df-covers 38924  df-ats 38925  df-atl 38956  df-cvlat 38980  df-hlat 39009  df-llines 39157  df-lplanes 39158  df-lvols 39159  df-lines 39160  df-psubsp 39162  df-pmap 39163  df-padd 39455  df-lhyp 39647  df-laut 39648  df-ldil 39763  df-ltrn 39764  df-trl 39818  df-tendo 40414  df-edring 40416  df-disoa 40688  df-dvech 40738  df-dib 40798  df-dic 40832  df-dih 40888
This theorem is referenced by:  dih1rn  40946  dih1cnv  40947  dihglb2  41001  doch0  41017  dochocss  41025
  Copyright terms: Public domain W3C validator