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 37611
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 486 . . 3 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋 ≀ π‘Œ) β†’ 𝑋 ≀ π‘Œ)
2 simpl1 1191 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋 ≀ π‘Œ) β†’ 𝐾 ∈ HL)
3 simpl3 1193 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋 ≀ π‘Œ) β†’ π‘Œ ∈ 𝑃)
4 llncvrlpln2.n . . . . . 6 𝑁 = (LLinesβ€˜πΎ)
5 llncvrlpln2.p . . . . . 6 𝑃 = (LPlanesβ€˜πΎ)
64, 5lplnnelln 37600 . . . . 5 ((𝐾 ∈ HL ∧ π‘Œ ∈ 𝑃) β†’ Β¬ π‘Œ ∈ 𝑁)
72, 3, 6syl2anc 585 . . . 4 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋 ≀ π‘Œ) β†’ Β¬ π‘Œ ∈ 𝑁)
8 simpl2 1192 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋 ≀ π‘Œ) β†’ 𝑋 ∈ 𝑁)
9 eleq1 2824 . . . . . 6 (𝑋 = π‘Œ β†’ (𝑋 ∈ 𝑁 ↔ π‘Œ ∈ 𝑁))
108, 9syl5ibcom 246 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋 ≀ π‘Œ) β†’ (𝑋 = π‘Œ β†’ π‘Œ ∈ 𝑁))
1110necon3bd 2955 . . . 4 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋 ≀ π‘Œ) β†’ (Β¬ π‘Œ ∈ 𝑁 β†’ 𝑋 β‰  π‘Œ))
127, 11mpd 15 . . 3 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋 ≀ π‘Œ) β†’ 𝑋 β‰  π‘Œ)
13 llncvrlpln2.l . . . . 5 ≀ = (leβ€˜πΎ)
14 eqid 2736 . . . . 5 (ltβ€˜πΎ) = (ltβ€˜πΎ)
1513, 14pltval 18092 . . . 4 ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) β†’ (𝑋(ltβ€˜πΎ)π‘Œ ↔ (𝑋 ≀ π‘Œ ∧ 𝑋 β‰  π‘Œ)))
1615adantr 482 . . 3 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋 ≀ π‘Œ) β†’ (𝑋(ltβ€˜πΎ)π‘Œ ↔ (𝑋 ≀ π‘Œ ∧ 𝑋 β‰  π‘Œ)))
171, 12, 16mpbir2and 711 . 2 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋 ≀ π‘Œ) β†’ 𝑋(ltβ€˜πΎ)π‘Œ)
18 simpl1 1191 . . . 4 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋(ltβ€˜πΎ)π‘Œ) β†’ 𝐾 ∈ HL)
19 simpl2 1192 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋(ltβ€˜πΎ)π‘Œ) β†’ 𝑋 ∈ 𝑁)
20 eqid 2736 . . . . . 6 (Baseβ€˜πΎ) = (Baseβ€˜πΎ)
2120, 4llnbase 37563 . . . . 5 (𝑋 ∈ 𝑁 β†’ 𝑋 ∈ (Baseβ€˜πΎ))
2219, 21syl 17 . . . 4 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋(ltβ€˜πΎ)π‘Œ) β†’ 𝑋 ∈ (Baseβ€˜πΎ))
23 simpl3 1193 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋(ltβ€˜πΎ)π‘Œ) β†’ π‘Œ ∈ 𝑃)
2420, 5lplnbase 37588 . . . . 5 (π‘Œ ∈ 𝑃 β†’ π‘Œ ∈ (Baseβ€˜πΎ))
2523, 24syl 17 . . . 4 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋(ltβ€˜πΎ)π‘Œ) β†’ π‘Œ ∈ (Baseβ€˜πΎ))
26 simpr 486 . . . 4 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋(ltβ€˜πΎ)π‘Œ) β†’ 𝑋(ltβ€˜πΎ)π‘Œ)
27 eqid 2736 . . . . 5 (joinβ€˜πΎ) = (joinβ€˜πΎ)
28 llncvrlpln2.c . . . . 5 𝐢 = ( β‹– β€˜πΎ)
29 eqid 2736 . . . . 5 (Atomsβ€˜πΎ) = (Atomsβ€˜πΎ)
3020, 13, 14, 27, 28, 29hlrelat3 37466 . . . 4 (((𝐾 ∈ HL ∧ 𝑋 ∈ (Baseβ€˜πΎ) ∧ π‘Œ ∈ (Baseβ€˜πΎ)) ∧ 𝑋(ltβ€˜πΎ)π‘Œ) β†’ βˆƒπ‘Ÿ ∈ (Atomsβ€˜πΎ)(𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ))
3118, 22, 25, 26, 30syl31anc 1373 . . 3 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋(ltβ€˜πΎ)π‘Œ) β†’ βˆƒπ‘Ÿ ∈ (Atomsβ€˜πΎ)(𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ))
3220, 13, 27, 29, 5islpln2 37590 . . . . . . . 8 (𝐾 ∈ HL β†’ (π‘Œ ∈ 𝑃 ↔ (π‘Œ ∈ (Baseβ€˜πΎ) ∧ βˆƒπ‘  ∈ (Atomsβ€˜πΎ)βˆƒπ‘‘ ∈ (Atomsβ€˜πΎ)βˆƒπ‘’ ∈ (Atomsβ€˜πΎ)(𝑠 β‰  𝑑 ∧ Β¬ 𝑒 ≀ (𝑠(joinβ€˜πΎ)𝑑) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒)))))
3332adantr 482 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁) β†’ (π‘Œ ∈ 𝑃 ↔ (π‘Œ ∈ (Baseβ€˜πΎ) ∧ βˆƒπ‘  ∈ (Atomsβ€˜πΎ)βˆƒπ‘‘ ∈ (Atomsβ€˜πΎ)βˆƒπ‘’ ∈ (Atomsβ€˜πΎ)(𝑠 β‰  𝑑 ∧ Β¬ 𝑒 ≀ (𝑠(joinβ€˜πΎ)𝑑) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒)))))
34 simp3 1138 . . . . . . . . . . 11 ((𝑠 β‰  𝑑 ∧ Β¬ 𝑒 ≀ (𝑠(joinβ€˜πΎ)𝑑) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒)) β†’ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒))
3520, 27, 29, 4islln2 37565 . . . . . . . . . . . . 13 (𝐾 ∈ HL β†’ (𝑋 ∈ 𝑁 ↔ (𝑋 ∈ (Baseβ€˜πΎ) ∧ βˆƒπ‘ ∈ (Atomsβ€˜πΎ)βˆƒπ‘ž ∈ (Atomsβ€˜πΎ)(𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)))))
36 simp3l 1201 . . . . . . . . . . . . . . . . . . . 20 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ 𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ))
37 simp3r 1202 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)
38 simp12r 1287 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž))
3938oveq1d 7319 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ (𝑋(joinβ€˜πΎ)π‘Ÿ) = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))
40 simp22 1207 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒))
4137, 39, 403brtr3d 5113 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ) ≀ ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒))
42 simp111 1302 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ 𝐾 ∈ HL)
43 simp112 1303 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ 𝑝 ∈ (Atomsβ€˜πΎ))
44 simp113 1304 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ π‘ž ∈ (Atomsβ€˜πΎ))
45 simp23 1208 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ π‘Ÿ ∈ (Atomsβ€˜πΎ))
4643, 44, 453jca 1128 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ (𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)))
47 simp13l 1288 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ 𝑠 ∈ (Atomsβ€˜πΎ))
48 simp13r 1289 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ 𝑑 ∈ (Atomsβ€˜πΎ))
49 simp21 1206 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ 𝑒 ∈ (Atomsβ€˜πΎ))
5047, 48, 493jca 1128 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)))
5136, 38, 393brtr3d 5113 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ (𝑝(joinβ€˜πΎ)π‘ž)𝐢((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))
5220, 27, 29hlatjcl 37421 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) β†’ (𝑝(joinβ€˜πΎ)π‘ž) ∈ (Baseβ€˜πΎ))
5342, 43, 44, 52syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ (𝑝(joinβ€˜πΎ)π‘ž) ∈ (Baseβ€˜πΎ))
5420, 13, 27, 28, 29cvr1 37464 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐾 ∈ HL ∧ (𝑝(joinβ€˜πΎ)π‘ž) ∈ (Baseβ€˜πΎ) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) β†’ (Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ↔ (𝑝(joinβ€˜πΎ)π‘ž)𝐢((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ)))
5542, 53, 45, 54syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ (Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ↔ (𝑝(joinβ€˜πΎ)π‘ž)𝐢((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ)))
5651, 55mpbird 258 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž))
57 simp12l 1286 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ 𝑝 β‰  π‘ž)
5813, 27, 293at 37544 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐾 ∈ HL ∧ (𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ))) ∧ (Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑝 β‰  π‘ž)) β†’ (((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ) ≀ ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ↔ ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ) = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒)))
5942, 46, 50, 56, 57, 58syl32anc 1378 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ (((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ) ≀ ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ↔ ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ) = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒)))
6041, 59mpbid 232 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ) = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒))
6160, 39, 403eqtr4d 2786 . . . . . . . . . . . . . . . . . . . 20 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ (𝑋(joinβ€˜πΎ)π‘Ÿ) = π‘Œ)
6236, 61breqtrd 5108 . . . . . . . . . . . . . . . . . . 19 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ π‘‹πΆπ‘Œ)
63623exp 1119 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) β†’ ((𝑒 ∈ (Atomsβ€˜πΎ) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ)) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ)))
64633expd 1353 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) β†’ (𝑒 ∈ (Atomsβ€˜πΎ) β†’ (π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) β†’ (π‘Ÿ ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ)))))
65643exp 1119 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) β†’ ((𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) β†’ ((𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ)) β†’ (𝑒 ∈ (Atomsβ€˜πΎ) β†’ (π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) β†’ (π‘Ÿ ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ)))))))
66653expib 1122 . . . . . . . . . . . . . . 15 (𝐾 ∈ HL β†’ ((𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) β†’ ((𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) β†’ ((𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ)) β†’ (𝑒 ∈ (Atomsβ€˜πΎ) β†’ (π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) β†’ (π‘Ÿ ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ))))))))
6766rexlimdvv 3201 . . . . . . . . . . . . . 14 (𝐾 ∈ HL β†’ (βˆƒπ‘ ∈ (Atomsβ€˜πΎ)βˆƒπ‘ž ∈ (Atomsβ€˜πΎ)(𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž)) β†’ ((𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ)) β†’ (𝑒 ∈ (Atomsβ€˜πΎ) β†’ (π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) β†’ (π‘Ÿ ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ)))))))
6867adantld 492 . . . . . . . . . . . . 13 (𝐾 ∈ HL β†’ ((𝑋 ∈ (Baseβ€˜πΎ) ∧ βˆƒπ‘ ∈ (Atomsβ€˜πΎ)βˆƒπ‘ž ∈ (Atomsβ€˜πΎ)(𝑝 β‰  π‘ž ∧ 𝑋 = (𝑝(joinβ€˜πΎ)π‘ž))) β†’ ((𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ)) β†’ (𝑒 ∈ (Atomsβ€˜πΎ) β†’ (π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) β†’ (π‘Ÿ ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ)))))))
6935, 68sylbid 240 . . . . . . . . . . . 12 (𝐾 ∈ HL β†’ (𝑋 ∈ 𝑁 β†’ ((𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ)) β†’ (𝑒 ∈ (Atomsβ€˜πΎ) β†’ (π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒) β†’ (π‘Ÿ ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ)))))))
7069imp31 419 . . . . . . . . . . 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 3147 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ))) β†’ (βˆƒπ‘’ ∈ (Atomsβ€˜πΎ)(𝑠 β‰  𝑑 ∧ Β¬ 𝑒 ≀ (𝑠(joinβ€˜πΎ)𝑑) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒)) β†’ (π‘Ÿ ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ))))
7372rexlimdvva 3202 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁) β†’ (βˆƒπ‘  ∈ (Atomsβ€˜πΎ)βˆƒπ‘‘ ∈ (Atomsβ€˜πΎ)βˆƒπ‘’ ∈ (Atomsβ€˜πΎ)(𝑠 β‰  𝑑 ∧ Β¬ 𝑒 ≀ (𝑠(joinβ€˜πΎ)𝑑) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒)) β†’ (π‘Ÿ ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ))))
7473adantld 492 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁) β†’ ((π‘Œ ∈ (Baseβ€˜πΎ) ∧ βˆƒπ‘  ∈ (Atomsβ€˜πΎ)βˆƒπ‘‘ ∈ (Atomsβ€˜πΎ)βˆƒπ‘’ ∈ (Atomsβ€˜πΎ)(𝑠 β‰  𝑑 ∧ Β¬ 𝑒 ≀ (𝑠(joinβ€˜πΎ)𝑑) ∧ π‘Œ = ((𝑠(joinβ€˜πΎ)𝑑)(joinβ€˜πΎ)𝑒))) β†’ (π‘Ÿ ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ))))
7533, 74sylbid 240 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁) β†’ (π‘Œ ∈ 𝑃 β†’ (π‘Ÿ ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ))))
76753impia 1117 . . . . 5 ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) β†’ (π‘Ÿ ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ)))
7776rexlimdv 3147 . . . 4 ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) β†’ (βˆƒπ‘Ÿ ∈ (Atomsβ€˜πΎ)(𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ))
7877imp 408 . . 3 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ βˆƒπ‘Ÿ ∈ (Atomsβ€˜πΎ)(𝑋𝐢(𝑋(joinβ€˜πΎ)π‘Ÿ) ∧ (𝑋(joinβ€˜πΎ)π‘Ÿ) ≀ π‘Œ)) β†’ π‘‹πΆπ‘Œ)
7931, 78syldan 592 . 2 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋(ltβ€˜πΎ)π‘Œ) β†’ π‘‹πΆπ‘Œ)
8017, 79syldan 592 1 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ π‘Œ ∈ 𝑃) ∧ 𝑋 ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1087   = wceq 1539   ∈ wcel 2104   β‰  wne 2941  βˆƒwrex 3071   class class class wbr 5082  β€˜cfv 6455  (class class class)co 7304  Basecbs 16954  lecple 17011  ltcplt 18068  joincjn 18071   β‹– ccvr 37316  Atomscatm 37317  HLchlt 37404  LLinesclln 37545  LPlanesclpl 37546
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 2707  ax-rep 5219  ax-sep 5233  ax-nul 5240  ax-pow 5298  ax-pr 5362  ax-un 7617
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3279  df-rab 3280  df-v 3440  df-sbc 3723  df-csb 3839  df-dif 3896  df-un 3898  df-in 3900  df-ss 3910  df-nul 4264  df-if 4467  df-pw 4542  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4846  df-iun 4934  df-br 5083  df-opab 5145  df-mpt 5166  df-id 5497  df-xp 5603  df-rel 5604  df-cnv 5605  df-co 5606  df-dm 5607  df-rn 5608  df-res 5609  df-ima 5610  df-iota 6407  df-fun 6457  df-fn 6458  df-f 6459  df-f1 6460  df-fo 6461  df-f1o 6462  df-fv 6463  df-riota 7261  df-ov 7307  df-oprab 7308  df-proset 18055  df-poset 18073  df-plt 18090  df-lub 18106  df-glb 18107  df-join 18108  df-meet 18109  df-p0 18185  df-lat 18192  df-clat 18259  df-oposet 37230  df-ol 37232  df-oml 37233  df-covers 37320  df-ats 37321  df-atl 37352  df-cvlat 37376  df-hlat 37405  df-llines 37552  df-lplanes 37553
This theorem is referenced by:  llncvrlpln  37612  2llnmj  37614  lplncmp  37616  lplnexatN  37617  2llnm2N  37622  2lplnmj  37676
  Copyright terms: Public domain W3C validator