Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  llncvrlpln2 Structured version   Visualization version   GIF version
Theorem llncvrlpln2 38731
Description: A lattice line under a lattice plane is covered by it. (Contributed by NM, 24-Jun-2012.)
Hypotheses
Ref Expression
llncvrlpln2.l ≀ = (leβ€˜πΎ)
llncvrlpln2.c 𝐢 = ( β‹– β€˜πΎ)
llncvrlpln2.n 𝑁 = (LLinesβ€˜πΎ)
llncvrlpln2.p 𝑃 = (LPlanesβ€˜πΎ)
Assertion
Ref Expression
llncvrlpln2 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋 ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ)
Proof of Theorem llncvrlpln2
Dummy variables π‘ž 𝑝 π‘Ÿ 𝑠 𝑑 𝑒 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 483 . . 3 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋 ≀ π‘Œ) β†’ 𝑋 ≀ π‘Œ)
2 simpl1 1189 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋 ≀ π‘Œ) β†’ 𝐾 ∈ HL)
3 simpl3 1191 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋 ≀ π‘Œ) β†’ π‘Œ ∈ 𝑃)
4 llncvrlpln2.n . . . . . 6 𝑁 = (LLinesβ€˜πΎ)
5 llncvrlpln2.p . . . . . 6 𝑃 = (LPlanesβ€˜πΎ)
64, 5lplnnelln 38720 . . . . 5 ((𝐾 ∈ HL ∧ π‘Œ ∈ 𝑃) β†’ Β¬ π‘Œ ∈ 𝑁)
72, 3, 6syl2anc 582 . . . 4 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋 ≀ π‘Œ) β†’ Β¬ π‘Œ ∈ 𝑁)
8 simpl2 1190 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋 ≀ π‘Œ) β†’ 𝑋 ∈ 𝑁)
9 eleq1 2819 . . . . . 6 (𝑋 = π‘Œ β†’ (𝑋 ∈ 𝑁 ↔ π‘Œ ∈ 𝑁))
108, 9syl5ibcom 244 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋 ≀ π‘Œ) β†’ (𝑋 = π‘Œ β†’ π‘Œ ∈ 𝑁))
1110necon3bd 2952 . . . 4 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋 ≀ π‘Œ) β†’ (Β¬ π‘Œ ∈ 𝑁 β†’ 𝑋 β‰  π‘Œ))
127, 11mpd 15 . . 3 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋 ≀ π‘Œ) β†’ 𝑋 β‰  π‘Œ)
13 llncvrlpln2.l . . . . 5 ≀ = (leβ€˜πΎ)
14 eqid 2730 . . . . 5 (ltβ€˜πΎ) = (ltβ€˜πΎ)
1513, 14pltval 18289 . . . 4 ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) β†’ (𝑋(ltβ€˜πΎ)π‘Œ ↔ (𝑋 ≀ π‘Œ ∧ 𝑋 β‰  π‘Œ)))
1615adantr 479 . . 3 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋 ≀ π‘Œ) β†’ (𝑋(ltβ€˜πΎ)π‘Œ ↔ (𝑋 ≀ π‘Œ ∧ 𝑋 β‰  π‘Œ)))
171, 12, 16mpbir2and 709 . 2 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋 ≀ π‘Œ) β†’ 𝑋(ltβ€˜πΎ)π‘Œ)
18 simpl1 1189 . . . 4 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋(ltβ€˜πΎ)π‘Œ) β†’ 𝐾 ∈ HL)
19 simpl2 1190 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋(ltβ€˜πΎ)π‘Œ) β†’ 𝑋 ∈ 𝑁)
20 eqid 2730 . . . . . 6 (Baseβ€˜πΎ) = (Baseβ€˜πΎ)
2120, 4llnbase 38683 . . . . 5 (𝑋 ∈ 𝑁 β†’ 𝑋 ∈ (Baseβ€˜πΎ))
2219, 21syl 17 . . . 4 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋(ltβ€˜πΎ)π‘Œ) β†’ 𝑋 ∈ (Baseβ€˜πΎ))
23 simpl3 1191 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋(ltβ€˜πΎ)π‘Œ) β†’ π‘Œ ∈ 𝑃)
2420, 5lplnbase 38708 . . . . 5 (π‘Œ ∈ 𝑃 β†’ π‘Œ ∈ (Baseβ€˜πΎ))
2523, 24syl 17 . . . 4 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋(ltβ€˜πΎ)π‘Œ) β†’ π‘Œ ∈ (Baseβ€˜πΎ))
26 simpr 483 . . . 4 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋(ltβ€˜πΎ)π‘Œ) β†’ 𝑋(ltβ€˜πΎ)π‘Œ)
27 eqid 2730 . . . . 5 (joinβ€˜πΎ) = (joinβ€˜πΎ)
28 llncvrlpln2.c . . . . 5 𝐢 = ( β‹– β€˜πΎ)
29 eqid 2730 . . . . 5 (Atomsβ€˜πΎ) = (Atomsβ€˜πΎ)
3020, 13, 14, 27, 28, 29hlrelat3 38586 . . . 4 (((𝐾 ∈ HL ∧ 𝑋 ∈ (Baseβ€˜πΎ) ∧ π‘Œ ∈ (Baseβ€˜πΎ)) ∧ 𝑋(ltβ€˜πΎ)π‘Œ) β†’ βˆƒπ‘Ÿ ∈ (Atomsβ€˜πΎ)(𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ))
3118, 22, 25, 26, 30syl31anc 1371 . . 3 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋(ltβ€˜πΎ)π‘Œ) β†’ βˆƒπ‘Ÿ ∈ (Atomsβ€˜πΎ)(𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ))
3220, 13, 27, 29, 5islpln2 38710 . . . . . . . 8 (𝐾 ∈ HL β†’ (π‘Œ ∈ 𝑃 ↔ (π‘Œ ∈ (Baseβ€˜πΎ) ∧ βˆƒπ‘  ∈ (Atomsβ€˜πΎ)βˆƒπ‘‘ ∈ (Atomsβ€˜πΎ)βˆƒπ‘’ ∈ (Atomsβ€˜πΎ)(𝑠 β‰  𝑑 ∧ Β¬ 𝑒 ≀ (𝑠(joinβ€˜πΎ)𝑑) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒)))))
3332adantr 479 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁) β†’ (π‘Œ ∈ 𝑃 ↔ (π‘Œ ∈ (Baseβ€˜πΎ) ∧ βˆƒπ‘  ∈ (Atomsβ€˜πΎ)βˆƒπ‘‘ ∈ (Atomsβ€˜πΎ)βˆƒπ‘’ ∈ (Atomsβ€˜πΎ)(𝑠 β‰  𝑑 ∧ Β¬ 𝑒 ≀ (𝑠(joinβ€˜πΎ)𝑑) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒)))))
34 simp3 1136 . . . . . . . . . . 11 ((𝑠 β‰  𝑑 ∧ Β¬ 𝑒 ≀ (𝑠(joinβ€˜πΎ)𝑑) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒)) β†’ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒))
3520, 27, 29, 4islln2 38685 . . . . . . . . . . . . 13 (𝐾 ∈ HL β†’ (𝑋 ∈ 𝑁 ↔ (𝑋 ∈ (Baseβ€˜πΎ) ∧ βˆƒπ‘ ∈ (Atomsβ€˜πΎ)βˆƒπ‘ž ∈ (Atomsβ€˜πΎ)(𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)))))
36 simp3l 1199 . . . . . . . . . . . . . . . . . . . 20 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ 𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ))
37 simp3r 1200 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)
38 simp12r 1285 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž))
3938oveq1d 7426 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ (𝑋(joinβ€˜πΎ)π‘Ÿ) = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))
40 simp22 1205 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒))
4137, 39, 403brtr3d 5178 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ) ≀ ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒))
42 simp111 1300 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ 𝐾 ∈ HL)
43 simp112 1301 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ 𝑝 ∈ (Atomsβ€˜πΎ))
44 simp113 1302 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ π‘ž ∈ (Atomsβ€˜πΎ))
45 simp23 1206 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ π‘Ÿ ∈ (Atomsβ€˜πΎ))
4643, 44, 453jca 1126 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ (𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)))
47 simp13l 1286 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ 𝑠 ∈ (Atomsβ€˜πΎ))
48 simp13r 1287 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ 𝑑 ∈ (Atomsβ€˜πΎ))
49 simp21 1204 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ 𝑒 ∈ (Atomsβ€˜πΎ))
5047, 48, 493jca 1126 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)))
5136, 38, 393brtr3d 5178 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ (𝑝(joinβ€˜πΎ)π‘ž)𝐢((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))
5220, 27, 29hlatjcl 38540 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) β†’ (𝑝(joinβ€˜πΎ)π‘ž) ∈ (Baseβ€˜πΎ))
5342, 43, 44, 52syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ (𝑝(joinβ€˜πΎ)π‘ž) ∈ (Baseβ€˜πΎ))
5420, 13, 27, 28, 29cvr1 38584 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐾 ∈ HL ∧ (𝑝(joinβ€˜πΎ)π‘ž) ∈ (Baseβ€˜πΎ) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) β†’ (Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ↔ (𝑝(joinβ€˜πΎ)π‘ž)𝐢((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ)))
5542, 53, 45, 54syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ (Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ↔ (𝑝(joinβ€˜πΎ)π‘ž)𝐢((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ)))
5651, 55mpbird 256 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž))
57 simp12l 1284 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ 𝑝 β‰  π‘ž)
5813, 27, 293at 38664 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐾 ∈ HL ∧ (𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ))) ∧ (Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑝 β‰  π‘ž)) β†’ (((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ) ≀ ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ↔ ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ) = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒)))
5942, 46, 50, 56, 57, 58syl32anc 1376 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ (((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ) ≀ ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ↔ ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ) = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒)))
6041, 59mpbid 231 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ) = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒))
6160, 39, 403eqtr4d 2780 . . . . . . . . . . . . . . . . . . . 20 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ (𝑋(joinβ€˜πΎ)π‘Ÿ) = π‘Œ)
6236, 61breqtrd 5173 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ π‘‹πΆπ‘Œ)
63623exp 1117 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) β†’ ((𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ)))
64633expd 1351 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) β†’ (𝑒 ∈ (Atomsβ€˜πΎ) β†’ (π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) β†’ (π‘Ÿ ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ)))))
65643exp 1117 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) β†’ ((𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) β†’ ((𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ)) β†’ (𝑒 ∈ (Atomsβ€˜πΎ) β†’ (π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) β†’ (π‘Ÿ ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ)))))))
66653expib 1120 . . . . . . . . . . . . . . 15 (𝐾 ∈ HL β†’ ((𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) β†’ ((𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) β†’ ((𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ)) β†’ (𝑒 ∈ (Atomsβ€˜πΎ) β†’ (π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) β†’ (π‘Ÿ ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ))))))))
6766rexlimdvv 3208 . . . . . . . . . . . . . 14 (𝐾 ∈ HL β†’ (βˆƒπ‘ ∈ (Atomsβ€˜πΎ)βˆƒπ‘ž ∈ (Atomsβ€˜πΎ)(𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) β†’ ((𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ)) β†’ (𝑒 ∈ (Atomsβ€˜πΎ) β†’ (π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) β†’ (π‘Ÿ ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ)))))))
6867adantld 489 . . . . . . . . . . . . 13 (𝐾 ∈ HL β†’ ((𝑋 ∈ (Baseβ€˜πΎ) ∧ βˆƒπ‘ ∈ (Atomsβ€˜πΎ)βˆƒπ‘ž ∈ (Atomsβ€˜πΎ)(𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž))) β†’ ((𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ)) β†’ (𝑒 ∈ (Atomsβ€˜πΎ) β†’ (π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) β†’ (π‘Ÿ ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ)))))))
6935, 68sylbid 239 . . . . . . . . . . . 12 (𝐾 ∈ HL β†’ (𝑋 ∈ 𝑁 β†’ ((𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ)) β†’ (𝑒 ∈ (Atomsβ€˜πΎ) β†’ (π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) β†’ (π‘Ÿ ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ)))))))
7069imp31 416 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) β†’ (𝑒 ∈ (Atomsβ€˜πΎ) β†’ (π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) β†’ (π‘Ÿ ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ)))))
7134, 70syl7 74 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) β†’ (𝑒 ∈ (Atomsβ€˜πΎ) β†’ ((𝑠 β‰  𝑑 ∧ Β¬ 𝑒 ≀ (𝑠(joinβ€˜πΎ)𝑑) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒)) β†’ (π‘Ÿ ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ)))))
7271rexlimdv 3151 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) β†’ (βˆƒπ‘’ ∈ (Atomsβ€˜πΎ)(𝑠 β‰  𝑑 ∧ Β¬ 𝑒 ≀ (𝑠(joinβ€˜πΎ)𝑑) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒)) β†’ (π‘Ÿ ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ))))
7372rexlimdvva 3209 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁) β†’ (βˆƒπ‘  ∈ (Atomsβ€˜πΎ)βˆƒπ‘‘ ∈ (Atomsβ€˜πΎ)βˆƒπ‘’ ∈ (Atomsβ€˜πΎ)(𝑠 β‰  𝑑 ∧ Β¬ 𝑒 ≀ (𝑠(joinβ€˜πΎ)𝑑) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒)) β†’ (π‘Ÿ ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ))))
7473adantld 489 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁) β†’ ((π‘Œ ∈ (Baseβ€˜πΎ) ∧ βˆƒπ‘  ∈ (Atomsβ€˜πΎ)βˆƒπ‘‘ ∈ (Atomsβ€˜πΎ)βˆƒπ‘’ ∈ (Atomsβ€˜πΎ)(𝑠 β‰  𝑑 ∧ Β¬ 𝑒 ≀ (𝑠(joinβ€˜πΎ)𝑑) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒))) β†’ (π‘Ÿ ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ))))
7533, 74sylbid 239 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁) β†’ (π‘Œ ∈ 𝑃 β†’ (π‘Ÿ ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ))))
76753impia 1115 . . . . 5 ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) β†’ (π‘Ÿ ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ)))
7776rexlimdv 3151 . . . 4 ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) β†’ (βˆƒπ‘Ÿ ∈ (Atomsβ€˜πΎ)(𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ))
7877imp 405 . . 3 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ βˆƒπ‘Ÿ ∈ (Atomsβ€˜πΎ)(𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ π‘‹πΆπ‘Œ)
7931, 78syldan 589 . 2 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋(ltβ€˜πΎ)π‘Œ) β†’ π‘‹πΆπ‘Œ)
8017, 79syldan 589 1 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋 ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104   β‰  wne 2938  βˆƒwrex 3068   class class class wbr 5147  β€˜cfv 6542  (class class class)co 7411  Basecbs 17148  lecple 17208  ltcplt 18265  joincjn 18268   β‹– ccvr 38435  Atomscatm 38436  HLchlt 38523  LLinesclln 38665  LPlanesclpl 38666
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-proset 18252  df-poset 18270  df-plt 18287  df-lub 18303  df-glb 18304  df-join 18305  df-meet 18306  df-p0 18382  df-lat 18389  df-clat 18456  df-oposet 38349  df-ol 38351  df-oml 38352  df-covers 38439  df-ats 38440  df-atl 38471  df-cvlat 38495  df-hlat 38524  df-llines 38672  df-lplanes 38673
This theorem is referenced by:  llncvrlpln  38732  2llnmj  38734  lplncmp  38736  lplnexatN  38737  2llnm2N  38742  2lplnmj  38796
  Copyright terms: Public domain W3C validator