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

Theorem cdlemg46 37349
Description: Part of proof of Lemma G of [Crawley] p. 116, seventh line of third paragraph on p. 117: "hf and f have different traces." (Contributed by NM, 5-Jun-2013.)
Hypotheses
Ref Expression
cdlemg46.b 𝐵 = (Base‘𝐾)
cdlemg46.h 𝐻 = (LHyp‘𝐾)
cdlemg46.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
cdlemg46.r 𝑅 = ((trL‘𝐾)‘𝑊)
Assertion
Ref Expression
cdlemg46 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → (𝑅‘(𝐹)) ≠ (𝑅𝐹))
Distinct variable groups:   ,𝐹   ,𝐻   ,𝐾   𝑅,   𝑇,   ,𝑊
Allowed substitution hint:   𝐵()

Proof of Theorem cdlemg46
StepHypRef Expression
1 simpl1l 1205 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) ∧ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → 𝐾 ∈ HL)
2 simp1 1117 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
3 simp2r 1181 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → 𝑇)
4 simp32 1191 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → ≠ ( I ↾ 𝐵))
5 cdlemg46.b . . . . . 6 𝐵 = (Base‘𝐾)
6 eqid 2773 . . . . . 6 (Atoms‘𝐾) = (Atoms‘𝐾)
7 cdlemg46.h . . . . . 6 𝐻 = (LHyp‘𝐾)
8 cdlemg46.t . . . . . 6 𝑇 = ((LTrn‘𝐾)‘𝑊)
9 cdlemg46.r . . . . . 6 𝑅 = ((trL‘𝐾)‘𝑊)
105, 6, 7, 8, 9trlnidat 36787 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑇 ≠ ( I ↾ 𝐵)) → (𝑅) ∈ (Atoms‘𝐾))
112, 3, 4, 10syl3anc 1352 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → (𝑅) ∈ (Atoms‘𝐾))
1211adantr 473 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) ∧ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → (𝑅) ∈ (Atoms‘𝐾))
13 simp2l 1180 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → 𝐹𝑇)
14 simp31 1190 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → 𝐹 ≠ ( I ↾ 𝐵))
155, 6, 7, 8, 9trlnidat 36787 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵)) → (𝑅𝐹) ∈ (Atoms‘𝐾))
162, 13, 14, 15syl3anc 1352 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → (𝑅𝐹) ∈ (Atoms‘𝐾))
1716adantr 473 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) ∧ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → (𝑅𝐹) ∈ (Atoms‘𝐾))
18 simpl33 1237 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) ∧ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → (𝑅) ≠ (𝑅𝐹))
19 simpr 477 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) ∧ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → (𝑅‘(𝐹)) ∈ (Atoms‘𝐾))
207, 8ltrnco 37333 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑇𝐹𝑇) → (𝐹) ∈ 𝑇)
212, 3, 13, 20syl3anc 1352 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → (𝐹) ∈ 𝑇)
227, 8ltrncnv 36760 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) → 𝐹𝑇)
232, 13, 22syl2anc 576 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → 𝐹𝑇)
24 eqid 2773 . . . . . . . 8 (le‘𝐾) = (le‘𝐾)
25 eqid 2773 . . . . . . . 8 (join‘𝐾) = (join‘𝐾)
2624, 25, 7, 8, 9trlco 37341 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹) ∈ 𝑇𝐹𝑇) → (𝑅‘((𝐹) ∘ 𝐹))(le‘𝐾)((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹)))
272, 21, 23, 26syl3anc 1352 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → (𝑅‘((𝐹) ∘ 𝐹))(le‘𝐾)((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹)))
28 coass 5955 . . . . . . . 8 ((𝐹) ∘ 𝐹) = ( ∘ (𝐹𝐹))
295, 7, 8ltrn1o 36738 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) → 𝐹:𝐵1-1-onto𝐵)
302, 13, 29syl2anc 576 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → 𝐹:𝐵1-1-onto𝐵)
31 f1ococnv2 6468 . . . . . . . . . . 11 (𝐹:𝐵1-1-onto𝐵 → (𝐹𝐹) = ( I ↾ 𝐵))
3230, 31syl 17 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → (𝐹𝐹) = ( I ↾ 𝐵))
3332coeq2d 5580 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → ( ∘ (𝐹𝐹)) = ( ∘ ( I ↾ 𝐵)))
345, 7, 8ltrn1o 36738 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑇) → :𝐵1-1-onto𝐵)
352, 3, 34syl2anc 576 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → :𝐵1-1-onto𝐵)
36 f1of 6442 . . . . . . . . . 10 (:𝐵1-1-onto𝐵:𝐵𝐵)
37 fcoi1 6379 . . . . . . . . . 10 (:𝐵𝐵 → ( ∘ ( I ↾ 𝐵)) = )
3835, 36, 373syl 18 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → ( ∘ ( I ↾ 𝐵)) = )
3933, 38eqtrd 2809 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → ( ∘ (𝐹𝐹)) = )
4028, 39syl5eq 2821 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → ((𝐹) ∘ 𝐹) = )
4140fveq2d 6501 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → (𝑅‘((𝐹) ∘ 𝐹)) = (𝑅))
427, 8, 9trlcnv 36779 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐹𝑇) → (𝑅𝐹) = (𝑅𝐹))
432, 13, 42syl2anc 576 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → (𝑅𝐹) = (𝑅𝐹))
4443oveq2d 6991 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → ((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹)) = ((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹)))
4527, 41, 443brtr3d 4957 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → (𝑅)(le‘𝐾)((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹)))
4645adantr 473 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) ∧ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → (𝑅)(le‘𝐾)((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹)))
4724, 25, 6hlatlej2 35990 . . . . 5 ((𝐾 ∈ HL ∧ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾) ∧ (𝑅𝐹) ∈ (Atoms‘𝐾)) → (𝑅𝐹)(le‘𝐾)((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹)))
481, 19, 17, 47syl3anc 1352 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) ∧ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → (𝑅𝐹)(le‘𝐾)((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹)))
491hllatd 35978 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) ∧ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → 𝐾 ∈ Lat)
505, 6atbase 35903 . . . . . 6 ((𝑅) ∈ (Atoms‘𝐾) → (𝑅) ∈ 𝐵)
5112, 50syl 17 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) ∧ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → (𝑅) ∈ 𝐵)
525, 6atbase 35903 . . . . . 6 ((𝑅𝐹) ∈ (Atoms‘𝐾) → (𝑅𝐹) ∈ 𝐵)
5317, 52syl 17 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) ∧ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → (𝑅𝐹) ∈ 𝐵)
545, 25, 6hlatjcl 35981 . . . . . 6 ((𝐾 ∈ HL ∧ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾) ∧ (𝑅𝐹) ∈ (Atoms‘𝐾)) → ((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹)) ∈ 𝐵)
551, 19, 17, 54syl3anc 1352 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) ∧ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → ((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹)) ∈ 𝐵)
565, 24, 25latjle12 17543 . . . . 5 ((𝐾 ∈ Lat ∧ ((𝑅) ∈ 𝐵 ∧ (𝑅𝐹) ∈ 𝐵 ∧ ((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹)) ∈ 𝐵)) → (((𝑅)(le‘𝐾)((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹)) ∧ (𝑅𝐹)(le‘𝐾)((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹))) ↔ ((𝑅)(join‘𝐾)(𝑅𝐹))(le‘𝐾)((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹))))
5749, 51, 53, 55, 56syl13anc 1353 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) ∧ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → (((𝑅)(le‘𝐾)((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹)) ∧ (𝑅𝐹)(le‘𝐾)((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹))) ↔ ((𝑅)(join‘𝐾)(𝑅𝐹))(le‘𝐾)((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹))))
5846, 48, 57mpbi2and 700 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) ∧ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → ((𝑅)(join‘𝐾)(𝑅𝐹))(le‘𝐾)((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹)))
5924, 25, 62atjlej 36093 . . 3 ((𝐾 ∈ HL ∧ ((𝑅) ∈ (Atoms‘𝐾) ∧ (𝑅𝐹) ∈ (Atoms‘𝐾) ∧ (𝑅) ≠ (𝑅𝐹)) ∧ ((𝑅‘(𝐹)) ∈ (Atoms‘𝐾) ∧ (𝑅𝐹) ∈ (Atoms‘𝐾) ∧ ((𝑅)(join‘𝐾)(𝑅𝐹))(le‘𝐾)((𝑅‘(𝐹))(join‘𝐾)(𝑅𝐹)))) → (𝑅‘(𝐹)) ≠ (𝑅𝐹))
601, 12, 17, 18, 19, 17, 58, 59syl133anc 1374 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) ∧ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → (𝑅‘(𝐹)) ≠ (𝑅𝐹))
61 nelne2 3061 . . . 4 (((𝑅𝐹) ∈ (Atoms‘𝐾) ∧ ¬ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → (𝑅𝐹) ≠ (𝑅‘(𝐹)))
6261necomd 3017 . . 3 (((𝑅𝐹) ∈ (Atoms‘𝐾) ∧ ¬ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → (𝑅‘(𝐹)) ≠ (𝑅𝐹))
6316, 62sylan 572 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) ∧ ¬ (𝑅‘(𝐹)) ∈ (Atoms‘𝐾)) → (𝑅‘(𝐹)) ≠ (𝑅𝐹))
6460, 63pm2.61dan 801 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐹𝑇𝑇) ∧ (𝐹 ≠ ( I ↾ 𝐵) ∧ ≠ ( I ↾ 𝐵) ∧ (𝑅) ≠ (𝑅𝐹))) → (𝑅‘(𝐹)) ≠ (𝑅𝐹))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 387  w3a 1069   = wceq 1508  wcel 2051  wne 2962   class class class wbr 4926   I cid 5308  ccnv 5403  cres 5406  ccom 5408  wf 6182  1-1-ontowf1o 6185  cfv 6186  (class class class)co 6975  Basecbs 16338  lecple 16427  joincjn 17425  Latclat 17526  Atomscatm 35877  HLchlt 35964  LHypclh 36598  LTrncltrn 36715  trLctrl 36772
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-rep 5046  ax-sep 5057  ax-nul 5064  ax-pow 5116  ax-pr 5183  ax-un 7278  ax-riotaBAD 35567
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ne 2963  df-ral 3088  df-rex 3089  df-reu 3090  df-rmo 3091  df-rab 3092  df-v 3412  df-sbc 3677  df-csb 3782  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-nul 4174  df-if 4346  df-pw 4419  df-sn 4437  df-pr 4439  df-op 4443  df-uni 4710  df-iun 4791  df-iin 4792  df-br 4927  df-opab 4989  df-mpt 5006  df-id 5309  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-riota 6936  df-ov 6978  df-oprab 6979  df-mpo 6980  df-1st 7500  df-2nd 7501  df-undef 7741  df-map 8207  df-proset 17409  df-poset 17427  df-plt 17439  df-lub 17455  df-glb 17456  df-join 17457  df-meet 17458  df-p0 17520  df-p1 17521  df-lat 17527  df-clat 17589  df-oposet 35790  df-ol 35792  df-oml 35793  df-covers 35880  df-ats 35881  df-atl 35912  df-cvlat 35936  df-hlat 35965  df-llines 36112  df-lplanes 36113  df-lvols 36114  df-lines 36115  df-psubsp 36117  df-pmap 36118  df-padd 36410  df-lhyp 36602  df-laut 36603  df-ldil 36718  df-ltrn 36719  df-trl 36773
This theorem is referenced by:  cdlemg47  37350
  Copyright terms: Public domain W3C validator