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

Theorem cdlemf1 36449
Description: Part of Lemma F in [Crawley] p. 116. TODO: should this or part of it become a stand-alone theorem? (Contributed by NM, 12-Apr-2013.)
Hypotheses
Ref Expression
cdlemf1.l = (le‘𝐾)
cdlemf1.j = (join‘𝐾)
cdlemf1.a 𝐴 = (Atoms‘𝐾)
cdlemf1.h 𝐻 = (LHyp‘𝐾)
Assertion
Ref Expression
cdlemf1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ∃𝑞𝐴 (𝑃𝑞 ∧ ¬ 𝑞 𝑊𝑈 (𝑃 𝑞)))
Distinct variable groups:   𝐴,𝑞   𝐻,𝑞   𝐾,𝑞   ,𝑞   𝑃,𝑞   𝑈,𝑞   𝑊,𝑞
Allowed substitution hint:   (𝑞)

Proof of Theorem cdlemf1
StepHypRef Expression
1 simp1l 1254 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝐾 ∈ HL)
2 simp3l 1258 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑃𝐴)
3 simp2l 1256 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑈𝐴)
4 simp2r 1257 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑈 𝑊)
5 simp3r 1259 . . . 4 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ¬ 𝑃 𝑊)
6 nbrne2 4828 . . . . 5 ((𝑈 𝑊 ∧ ¬ 𝑃 𝑊) → 𝑈𝑃)
76necomd 2991 . . . 4 ((𝑈 𝑊 ∧ ¬ 𝑃 𝑊) → 𝑃𝑈)
84, 5, 7syl2anc 579 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → 𝑃𝑈)
9 cdlemf1.l . . . 4 = (le‘𝐾)
10 cdlemf1.j . . . 4 = (join‘𝐾)
11 cdlemf1.a . . . 4 𝐴 = (Atoms‘𝐾)
129, 10, 11hlsupr 35274 . . 3 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑈𝐴) ∧ 𝑃𝑈) → ∃𝑞𝐴 (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈)))
131, 2, 3, 8, 12syl31anc 1492 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → ∃𝑞𝐴 (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈)))
14 simp31 1266 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑞𝐴 ∧ (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈))) → 𝑞𝑃)
1514necomd 2991 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑞𝐴 ∧ (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈))) → 𝑃𝑞)
16 simp13r 1388 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑞𝐴 ∧ (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈))) → ¬ 𝑃 𝑊)
17 simp12r 1386 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑞𝐴 ∧ (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈))) → 𝑈 𝑊)
18 simp11l 1383 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑞𝐴 ∧ (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈))) → 𝐾 ∈ HL)
1918hllatd 35252 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑞𝐴 ∧ (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈))) → 𝐾 ∈ Lat)
20 eqid 2764 . . . . . . . . . . . 12 (Base‘𝐾) = (Base‘𝐾)
2120, 11atbase 35177 . . . . . . . . . . 11 (𝑞𝐴𝑞 ∈ (Base‘𝐾))
22213ad2ant2 1164 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑞𝐴 ∧ (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈))) → 𝑞 ∈ (Base‘𝐾))
23 simp12l 1385 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑞𝐴 ∧ (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈))) → 𝑈𝐴)
2420, 11atbase 35177 . . . . . . . . . . 11 (𝑈𝐴𝑈 ∈ (Base‘𝐾))
2523, 24syl 17 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑞𝐴 ∧ (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈))) → 𝑈 ∈ (Base‘𝐾))
26 simp11r 1384 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑞𝐴 ∧ (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈))) → 𝑊𝐻)
27 cdlemf1.h . . . . . . . . . . . 12 𝐻 = (LHyp‘𝐾)
2820, 27lhpbase 35886 . . . . . . . . . . 11 (𝑊𝐻𝑊 ∈ (Base‘𝐾))
2926, 28syl 17 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑞𝐴 ∧ (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈))) → 𝑊 ∈ (Base‘𝐾))
3020, 9, 10latjle12 17329 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝑞 ∈ (Base‘𝐾) ∧ 𝑈 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑞 𝑊𝑈 𝑊) ↔ (𝑞 𝑈) 𝑊))
3119, 22, 25, 29, 30syl13anc 1491 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑞𝐴 ∧ (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈))) → ((𝑞 𝑊𝑈 𝑊) ↔ (𝑞 𝑈) 𝑊))
3231biimpd 220 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑞𝐴 ∧ (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈))) → ((𝑞 𝑊𝑈 𝑊) → (𝑞 𝑈) 𝑊))
3317, 32mpan2d 685 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑞𝐴 ∧ (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈))) → (𝑞 𝑊 → (𝑞 𝑈) 𝑊))
34 simp33 1268 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑞𝐴 ∧ (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈))) → 𝑞 (𝑃 𝑈))
35 hlcvl 35247 . . . . . . . . . . 11 (𝐾 ∈ HL → 𝐾 ∈ CvLat)
3618, 35syl 17 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑞𝐴 ∧ (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈))) → 𝐾 ∈ CvLat)
37 simp2 1167 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑞𝐴 ∧ (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈))) → 𝑞𝐴)
38 simp13l 1387 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑞𝐴 ∧ (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈))) → 𝑃𝐴)
39 simp32 1267 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑞𝐴 ∧ (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈))) → 𝑞𝑈)
409, 10, 11cvlatexch2 35225 . . . . . . . . . 10 ((𝐾 ∈ CvLat ∧ (𝑞𝐴𝑃𝐴𝑈𝐴) ∧ 𝑞𝑈) → (𝑞 (𝑃 𝑈) → 𝑃 (𝑞 𝑈)))
4136, 37, 38, 23, 39, 40syl131anc 1502 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑞𝐴 ∧ (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈))) → (𝑞 (𝑃 𝑈) → 𝑃 (𝑞 𝑈)))
4234, 41mpd 15 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑞𝐴 ∧ (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈))) → 𝑃 (𝑞 𝑈))
4320, 11atbase 35177 . . . . . . . . . 10 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
4438, 43syl 17 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑞𝐴 ∧ (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈))) → 𝑃 ∈ (Base‘𝐾))
4520, 10, 11hlatjcl 35255 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑞𝐴𝑈𝐴) → (𝑞 𝑈) ∈ (Base‘𝐾))
4618, 37, 23, 45syl3anc 1490 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑞𝐴 ∧ (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈))) → (𝑞 𝑈) ∈ (Base‘𝐾))
4720, 9lattr 17323 . . . . . . . . 9 ((𝐾 ∈ Lat ∧ (𝑃 ∈ (Base‘𝐾) ∧ (𝑞 𝑈) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑃 (𝑞 𝑈) ∧ (𝑞 𝑈) 𝑊) → 𝑃 𝑊))
4819, 44, 46, 29, 47syl13anc 1491 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑞𝐴 ∧ (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈))) → ((𝑃 (𝑞 𝑈) ∧ (𝑞 𝑈) 𝑊) → 𝑃 𝑊))
4942, 48mpand 686 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑞𝐴 ∧ (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈))) → ((𝑞 𝑈) 𝑊𝑃 𝑊))
5033, 49syld 47 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑞𝐴 ∧ (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈))) → (𝑞 𝑊𝑃 𝑊))
5116, 50mtod 189 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑞𝐴 ∧ (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈))) → ¬ 𝑞 𝑊)
529, 10, 11cvlatexch1 35224 . . . . . . 7 ((𝐾 ∈ CvLat ∧ (𝑞𝐴𝑈𝐴𝑃𝐴) ∧ 𝑞𝑃) → (𝑞 (𝑃 𝑈) → 𝑈 (𝑃 𝑞)))
5336, 37, 23, 38, 14, 52syl131anc 1502 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑞𝐴 ∧ (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈))) → (𝑞 (𝑃 𝑈) → 𝑈 (𝑃 𝑞)))
5434, 53mpd 15 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑞𝐴 ∧ (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈))) → 𝑈 (𝑃 𝑞))
5515, 51, 543jca 1158 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) ∧ 𝑞𝐴 ∧ (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈))) → (𝑃𝑞 ∧ ¬ 𝑞 𝑊𝑈 (𝑃 𝑞)))
56553exp 1148 . . 3 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (𝑞𝐴 → ((𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈)) → (𝑃𝑞 ∧ ¬ 𝑞 𝑊𝑈 (𝑃 𝑞)))))
5756reximdvai 3160 . 2 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑈𝐴𝑈 𝑊) ∧ (𝑃𝐴 ∧ ¬ 𝑃 𝑊)) → (∃𝑞𝐴 (𝑞𝑃𝑞𝑈𝑞 (𝑃 𝑈)) → ∃𝑞𝐴 (𝑃𝑞 ∧ ¬ 𝑞 𝑊𝑈 (𝑃 𝑞))))
5813, 57mpd 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  wne 2936  wrex 3055   class class class wbr 4808  cfv 6067  (class class class)co 6841  Basecbs 16131  lecple 16222  joincjn 17211  Latclat 17312  Atomscatm 35151  CvLatclc 35153  HLchlt 35238  LHypclh 35872
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
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  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-ral 3059  df-rex 3060  df-reu 3061  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-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-op 4340  df-uni 4594  df-iun 4677  df-br 4809  df-opab 4871  df-mpt 4888  df-id 5184  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-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-proset 17195  df-poset 17213  df-plt 17225  df-lub 17241  df-glb 17242  df-join 17243  df-meet 17244  df-p0 17306  df-lat 17313  df-covers 35154  df-ats 35155  df-atl 35186  df-cvlat 35210  df-hlat 35239  df-lhyp 35876
This theorem is referenced by:  cdlemf2  36450  cdlemg5  36493
  Copyright terms: Public domain W3C validator