Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  lplncvrlvol2 Structured version   Visualization version   GIF version
Theorem lplncvrlvol2 39025
Description: A lattice line under a lattice plane is covered by it. (Contributed by NM, 12-Jul-2012.)
Hypotheses
Ref Expression
lplncvrlvol2.l ≀ = (leβ€˜πΎ)
lplncvrlvol2.c 𝐢 = ( β‹– β€˜πΎ)
lplncvrlvol2.p 𝑃 = (LPlanesβ€˜πΎ)
lplncvrlvol2.v 𝑉 = (LVolsβ€˜πΎ)
Assertion
Ref Expression
lplncvrlvol2 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ π‘Œ ∈ 𝑉) ∧ 𝑋 ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ)
Proof of Theorem lplncvrlvol2
Dummy variables π‘ž 𝑝 π‘Ÿ 𝑠 𝑑 𝑒 𝑣 𝑀 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 484 . . 3 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ π‘Œ ∈ 𝑉) ∧ 𝑋 ≀ π‘Œ) β†’ 𝑋 ≀ π‘Œ)
2 simpl1 1189 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ π‘Œ ∈ 𝑉) ∧ 𝑋 ≀ π‘Œ) β†’ 𝐾 ∈ HL)
3 simpl3 1191 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ π‘Œ ∈ 𝑉) ∧ 𝑋 ≀ π‘Œ) β†’ π‘Œ ∈ 𝑉)
4 lplncvrlvol2.p . . . . . 6 𝑃 = (LPlanesβ€˜πΎ)
5 lplncvrlvol2.v . . . . . 6 𝑉 = (LVolsβ€˜πΎ)
64, 5lvolnelpln 39000 . . . . 5 ((𝐾 ∈ HL ∧ π‘Œ ∈ 𝑉) β†’ Β¬ π‘Œ ∈ 𝑃)
72, 3, 6syl2anc 583 . . . 4 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ π‘Œ ∈ 𝑉) ∧ 𝑋 ≀ π‘Œ) β†’ Β¬ π‘Œ ∈ 𝑃)
8 simpl2 1190 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ π‘Œ ∈ 𝑉) ∧ 𝑋 ≀ π‘Œ) β†’ 𝑋 ∈ 𝑃)
9 eleq1 2816 . . . . . 6 (𝑋 = π‘Œ β†’ (𝑋 ∈ 𝑃 ↔ π‘Œ ∈ 𝑃))
108, 9syl5ibcom 244 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ π‘Œ ∈ 𝑉) ∧ 𝑋 ≀ π‘Œ) β†’ (𝑋 = π‘Œ β†’ π‘Œ ∈ 𝑃))
1110necon3bd 2949 . . . 4 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ π‘Œ ∈ 𝑉) ∧ 𝑋 ≀ π‘Œ) β†’ (Β¬ π‘Œ ∈ 𝑃 β†’ 𝑋 β‰  π‘Œ))
127, 11mpd 15 . . 3 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ π‘Œ ∈ 𝑉) ∧ 𝑋 ≀ π‘Œ) β†’ 𝑋 β‰  π‘Œ)
13 lplncvrlvol2.l . . . . 5 ≀ = (leβ€˜πΎ)
14 eqid 2727 . . . . 5 (ltβ€˜πΎ) = (ltβ€˜πΎ)
1513, 14pltval 18315 . . . 4 ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ π‘Œ ∈ 𝑉) β†’ (𝑋(ltβ€˜πΎ)π‘Œ ↔ (𝑋 ≀ π‘Œ ∧ 𝑋 β‰  π‘Œ)))
1615adantr 480 . . 3 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ π‘Œ ∈ 𝑉) ∧ 𝑋 ≀ π‘Œ) β†’ (𝑋(ltβ€˜πΎ)π‘Œ ↔ (𝑋 ≀ π‘Œ ∧ 𝑋 β‰  π‘Œ)))
171, 12, 16mpbir2and 712 . 2 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ π‘Œ ∈ 𝑉) ∧ 𝑋 ≀ π‘Œ) β†’ 𝑋(ltβ€˜πΎ)π‘Œ)
18 simpl1 1189 . . . 4 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ π‘Œ ∈ 𝑉) ∧ 𝑋(ltβ€˜πΎ)π‘Œ) β†’ 𝐾 ∈ HL)
19 simpl2 1190 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ π‘Œ ∈ 𝑉) ∧ 𝑋(ltβ€˜πΎ)π‘Œ) β†’ 𝑋 ∈ 𝑃)
20 eqid 2727 . . . . . 6 (Baseβ€˜πΎ) = (Baseβ€˜πΎ)
2120, 4lplnbase 38944 . . . . 5 (𝑋 ∈ 𝑃 β†’ 𝑋 ∈ (Baseβ€˜πΎ))
2219, 21syl 17 . . . 4 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ π‘Œ ∈ 𝑉) ∧ 𝑋(ltβ€˜πΎ)π‘Œ) β†’ 𝑋 ∈ (Baseβ€˜πΎ))
23 simpl3 1191 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ π‘Œ ∈ 𝑉) ∧ 𝑋(ltβ€˜πΎ)π‘Œ) β†’ π‘Œ ∈ 𝑉)
2420, 5lvolbase 38988 . . . . 5 (π‘Œ ∈ 𝑉 β†’ π‘Œ ∈ (Baseβ€˜πΎ))
2523, 24syl 17 . . . 4 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ π‘Œ ∈ 𝑉) ∧ 𝑋(ltβ€˜πΎ)π‘Œ) β†’ π‘Œ ∈ (Baseβ€˜πΎ))
26 simpr 484 . . . 4 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ π‘Œ ∈ 𝑉) ∧ 𝑋(ltβ€˜πΎ)π‘Œ) β†’ 𝑋(ltβ€˜πΎ)π‘Œ)
27 eqid 2727 . . . . 5 (joinβ€˜πΎ) = (joinβ€˜πΎ)
28 lplncvrlvol2.c . . . . 5 𝐢 = ( β‹– β€˜πΎ)
29 eqid 2727 . . . . 5 (Atomsβ€˜πΎ) = (Atomsβ€˜πΎ)
3020, 13, 14, 27, 28, 29hlrelat3 38822 . . . 4 (((𝐾 ∈ HL ∧ 𝑋 ∈ (Baseβ€˜πΎ) ∧ π‘Œ ∈ (Baseβ€˜πΎ)) ∧ 𝑋(ltβ€˜πΎ)π‘Œ) β†’ βˆƒπ‘  ∈ (Atomsβ€˜πΎ)(𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ))
3118, 22, 25, 26, 30syl31anc 1371 . . 3 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ π‘Œ ∈ 𝑉) ∧ 𝑋(ltβ€˜πΎ)π‘Œ) β†’ βˆƒπ‘  ∈ (Atomsβ€˜πΎ)(𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ))
3220, 13, 27, 29, 5islvol2 38990 . . . . . . . 8 (𝐾 ∈ HL β†’ (π‘Œ ∈ 𝑉 ↔ (π‘Œ ∈ (Baseβ€˜πΎ) ∧ βˆƒπ‘‘ ∈ (Atomsβ€˜πΎ)βˆƒπ‘’ ∈ (Atomsβ€˜πΎ)βˆƒπ‘£ ∈ (Atomsβ€˜πΎ)βˆƒπ‘€ ∈ (Atomsβ€˜πΎ)((𝑑 β‰  𝑒 ∧ Β¬ 𝑣 ≀ (𝑑(joinβ€˜πΎ)𝑒) ∧ Β¬ 𝑀 ≀ ((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)))))
3332adantr 480 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃) β†’ (π‘Œ ∈ 𝑉 ↔ (π‘Œ ∈ (Baseβ€˜πΎ) ∧ βˆƒπ‘‘ ∈ (Atomsβ€˜πΎ)βˆƒπ‘’ ∈ (Atomsβ€˜πΎ)βˆƒπ‘£ ∈ (Atomsβ€˜πΎ)βˆƒπ‘€ ∈ (Atomsβ€˜πΎ)((𝑑 β‰  𝑒 ∧ Β¬ 𝑣 ≀ (𝑑(joinβ€˜πΎ)𝑒) ∧ Β¬ 𝑀 ≀ ((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)))))
34 simpr 484 . . . . . . . . . . 11 (((𝑑 β‰  𝑒 ∧ Β¬ 𝑣 ≀ (𝑑(joinβ€˜πΎ)𝑒) ∧ Β¬ 𝑀 ≀ ((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) β†’ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀))
3520, 13, 27, 29, 4islpln2 38946 . . . . . . . . . . . . 13 (𝐾 ∈ HL β†’ (𝑋 ∈ 𝑃 ↔ (𝑋 ∈ (Baseβ€˜πΎ) ∧ βˆƒπ‘ ∈ (Atomsβ€˜πΎ)βˆƒπ‘ž ∈ (Atomsβ€˜πΎ)βˆƒπ‘Ÿ ∈ (Atomsβ€˜πΎ)(𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ)))))
36 simp3rl 1244 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) ∧ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) ∧ (𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ))) β†’ 𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠))
37 simp3rr 1245 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) ∧ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) ∧ (𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ))) β†’ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ)
38 simp133 1308 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) ∧ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) ∧ (𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ))) β†’ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))
3938oveq1d 7429 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) ∧ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) ∧ (𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ))) β†’ (𝑋(joinβ€˜πΎ)𝑠) = (((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ)(joinβ€˜πΎ)𝑠))
40 simp23 1206 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) ∧ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) ∧ (𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ))) β†’ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀))
4137, 39, 403brtr3d 5173 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) ∧ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) ∧ (𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ))) β†’ (((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ)(joinβ€˜πΎ)𝑠) ≀ (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀))
42 simp11 1201 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) ∧ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) ∧ (𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ))) β†’ (𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)))
43 simp12 1202 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) ∧ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) ∧ (𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ))) β†’ π‘Ÿ ∈ (Atomsβ€˜πΎ))
44 simp3l 1199 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) ∧ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) ∧ (𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ))) β†’ 𝑠 ∈ (Atomsβ€˜πΎ))
45 simp21l 1288 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) ∧ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) ∧ (𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ))) β†’ 𝑑 ∈ (Atomsβ€˜πΎ))
4643, 44, 453jca 1126 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) ∧ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) ∧ (𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ))) β†’ (π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ 𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ)))
47 simp21r 1289 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) ∧ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) ∧ (𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ))) β†’ 𝑒 ∈ (Atomsβ€˜πΎ))
48 simp22l 1290 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) ∧ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) ∧ (𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ))) β†’ 𝑣 ∈ (Atomsβ€˜πΎ))
49 simp22r 1291 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) ∧ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) ∧ (𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ))) β†’ 𝑀 ∈ (Atomsβ€˜πΎ))
5047, 48, 493jca 1126 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) ∧ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) ∧ (𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ))) β†’ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ 𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)))
51 simp131 1306 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) ∧ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) ∧ (𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ))) β†’ 𝑝 β‰  π‘ž)
52 simp132 1307 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) ∧ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) ∧ (𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ))) β†’ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž))
5336, 38, 393brtr3d 5173 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) ∧ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) ∧ (𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ))) β†’ ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ)𝐢(((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ)(joinβ€˜πΎ)𝑠))
54 simp111 1300 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) ∧ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) ∧ (𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ))) β†’ 𝐾 ∈ HL)
5554hllatd 38773 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) ∧ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) ∧ (𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ))) β†’ 𝐾 ∈ Lat)
5620, 27, 29hlatjcl 38776 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) β†’ (𝑝(joinβ€˜πΎ)π‘ž) ∈ (Baseβ€˜πΎ))
5742, 56syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) ∧ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) ∧ (𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ))) β†’ (𝑝(joinβ€˜πΎ)π‘ž) ∈ (Baseβ€˜πΎ))
5820, 29atbase 38698 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (π‘Ÿ ∈ (Atomsβ€˜πΎ) β†’ π‘Ÿ ∈ (Baseβ€˜πΎ))
5943, 58syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) ∧ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) ∧ (𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ))) β†’ π‘Ÿ ∈ (Baseβ€˜πΎ))
6020, 27latjcl 18422 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐾 ∈ Lat ∧ (𝑝(joinβ€˜πΎ)π‘ž) ∈ (Baseβ€˜πΎ) ∧ π‘Ÿ ∈ (Baseβ€˜πΎ)) β†’ ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ) ∈ (Baseβ€˜πΎ))
6155, 57, 59, 60syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) ∧ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) ∧ (𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ))) β†’ ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ) ∈ (Baseβ€˜πΎ))
6220, 13, 27, 28, 29cvr1 38820 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐾 ∈ HL ∧ ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ) ∈ (Baseβ€˜πΎ) ∧ 𝑠 ∈ (Atomsβ€˜πΎ)) β†’ (Β¬ 𝑠 ≀ ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ) ↔ ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ)𝐢(((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ)(joinβ€˜πΎ)𝑠)))
6354, 61, 44, 62syl3anc 1369 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) ∧ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) ∧ (𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ))) β†’ (Β¬ 𝑠 ≀ ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ) ↔ ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ)𝐢(((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ)(joinβ€˜πΎ)𝑠)))
6453, 63mpbird 257 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) ∧ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) ∧ (𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ))) β†’ Β¬ 𝑠 ≀ ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))
6513, 27, 294at2 39024 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ (π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ 𝑠 ∈ (Atomsβ€˜πΎ) ∧ 𝑑 ∈ (Atomsβ€˜πΎ)) ∧ (𝑒 ∈ (Atomsβ€˜πΎ) ∧ 𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ))) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ Β¬ 𝑠 ≀ ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) β†’ ((((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ)(joinβ€˜πΎ)𝑠) ≀ (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀) ↔ (((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ)(joinβ€˜πΎ)𝑠) = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)))
6642, 46, 50, 51, 52, 64, 65syl33anc 1383 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) ∧ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) ∧ (𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ))) β†’ ((((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ)(joinβ€˜πΎ)𝑠) ≀ (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀) ↔ (((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ)(joinβ€˜πΎ)𝑠) = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)))
6741, 66mpbid 231 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) ∧ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) ∧ (𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ))) β†’ (((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ)(joinβ€˜πΎ)𝑠) = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀))
6867, 39, 403eqtr4d 2777 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) ∧ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) ∧ (𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ))) β†’ (𝑋(joinβ€˜πΎ)𝑠) = π‘Œ)
6936, 68breqtrd 5168 . . . . . . . . . . . . . . . . . . . 20 ((((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) ∧ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) ∧ (𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) ∧ (𝑠 ∈ (Atomsβ€˜πΎ) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ))) β†’ π‘‹πΆπ‘Œ)
70693exp 1117 . . . . . . . . . . . . . . . . . . 19 (((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) β†’ (((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) ∧ (𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) β†’ ((𝑠 ∈ (Atomsβ€˜πΎ) ∧ (𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ)) β†’ π‘‹πΆπ‘Œ)))
7170exp4a 431 . . . . . . . . . . . . . . . . . 18 (((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) β†’ (((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) ∧ (𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) β†’ (𝑠 ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ))))
72713expd 1351 . . . . . . . . . . . . . . . . 17 (((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) ∧ π‘Ÿ ∈ (Atomsβ€˜πΎ) ∧ (𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) β†’ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) β†’ ((𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) β†’ (π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀) β†’ (𝑠 ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ))))))
7372rexlimdv3a 3154 . . . . . . . . . . . . . . . 16 ((𝐾 ∈ HL ∧ 𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) β†’ (βˆƒπ‘Ÿ ∈ (Atomsβ€˜πΎ)(𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ)) β†’ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) β†’ ((𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) β†’ (π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀) β†’ (𝑠 ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ)))))))
74733expib 1120 . . . . . . . . . . . . . . 15 (𝐾 ∈ HL β†’ ((𝑝 ∈ (Atomsβ€˜πΎ) ∧ π‘ž ∈ (Atomsβ€˜πΎ)) β†’ (βˆƒπ‘Ÿ ∈ (Atomsβ€˜πΎ)(𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ)) β†’ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) β†’ ((𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) β†’ (π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀) β†’ (𝑠 ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ))))))))
7574rexlimdvv 3205 . . . . . . . . . . . . . 14 (𝐾 ∈ HL β†’ (βˆƒπ‘ ∈ (Atomsβ€˜πΎ)βˆƒπ‘ž ∈ (Atomsβ€˜πΎ)βˆƒπ‘Ÿ ∈ (Atomsβ€˜πΎ)(𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ)) β†’ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) β†’ ((𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) β†’ (π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀) β†’ (𝑠 ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ)))))))
7675adantld 490 . . . . . . . . . . . . 13 (𝐾 ∈ HL β†’ ((𝑋 ∈ (Baseβ€˜πΎ) ∧ βˆƒπ‘ ∈ (Atomsβ€˜πΎ)βˆƒπ‘ž ∈ (Atomsβ€˜πΎ)βˆƒπ‘Ÿ ∈ (Atomsβ€˜πΎ)(𝑝 β‰  π‘ž ∧ Β¬ π‘Ÿ ≀ (𝑝(joinβ€˜πΎ)π‘ž) ∧ 𝑋 = ((𝑝(joinβ€˜πΎ)π‘ž)(joinβ€˜πΎ)π‘Ÿ))) β†’ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) β†’ ((𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) β†’ (π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀) β†’ (𝑠 ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ)))))))
7735, 76sylbid 239 . . . . . . . . . . . 12 (𝐾 ∈ HL β†’ (𝑋 ∈ 𝑃 β†’ ((𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ)) β†’ ((𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) β†’ (π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀) β†’ (𝑠 ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ)))))))
7877imp31 417 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃) ∧ (𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ))) β†’ ((𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) β†’ (π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀) β†’ (𝑠 ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ)))))
7934, 78syl7 74 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃) ∧ (𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ))) β†’ ((𝑣 ∈ (Atomsβ€˜πΎ) ∧ 𝑀 ∈ (Atomsβ€˜πΎ)) β†’ (((𝑑 β‰  𝑒 ∧ Β¬ 𝑣 ≀ (𝑑(joinβ€˜πΎ)𝑒) ∧ Β¬ 𝑀 ≀ ((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) β†’ (𝑠 ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ)))))
8079rexlimdvv 3205 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃) ∧ (𝑑 ∈ (Atomsβ€˜πΎ) ∧ 𝑒 ∈ (Atomsβ€˜πΎ))) β†’ (βˆƒπ‘£ ∈ (Atomsβ€˜πΎ)βˆƒπ‘€ ∈ (Atomsβ€˜πΎ)((𝑑 β‰  𝑒 ∧ Β¬ 𝑣 ≀ (𝑑(joinβ€˜πΎ)𝑒) ∧ Β¬ 𝑀 ≀ ((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) β†’ (𝑠 ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ))))
8180rexlimdvva 3206 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃) β†’ (βˆƒπ‘‘ ∈ (Atomsβ€˜πΎ)βˆƒπ‘’ ∈ (Atomsβ€˜πΎ)βˆƒπ‘£ ∈ (Atomsβ€˜πΎ)βˆƒπ‘€ ∈ (Atomsβ€˜πΎ)((𝑑 β‰  𝑒 ∧ Β¬ 𝑣 ≀ (𝑑(joinβ€˜πΎ)𝑒) ∧ Β¬ 𝑀 ≀ ((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀)) β†’ (𝑠 ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ))))
8281adantld 490 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃) β†’ ((π‘Œ ∈ (Baseβ€˜πΎ) ∧ βˆƒπ‘‘ ∈ (Atomsβ€˜πΎ)βˆƒπ‘’ ∈ (Atomsβ€˜πΎ)βˆƒπ‘£ ∈ (Atomsβ€˜πΎ)βˆƒπ‘€ ∈ (Atomsβ€˜πΎ)((𝑑 β‰  𝑒 ∧ Β¬ 𝑣 ≀ (𝑑(joinβ€˜πΎ)𝑒) ∧ Β¬ 𝑀 ≀ ((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)) ∧ π‘Œ = (((𝑑(joinβ€˜πΎ)𝑒)(joinβ€˜πΎ)𝑣)(joinβ€˜πΎ)𝑀))) β†’ (𝑠 ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ))))
8333, 82sylbid 239 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃) β†’ (π‘Œ ∈ 𝑉 β†’ (𝑠 ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ))))
84833impia 1115 . . . . 5 ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ π‘Œ ∈ 𝑉) β†’ (𝑠 ∈ (Atomsβ€˜πΎ) β†’ ((𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ)))
8584rexlimdv 3148 . . . 4 ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ π‘Œ ∈ 𝑉) β†’ (βˆƒπ‘  ∈ (Atomsβ€˜πΎ)(𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ))
8685imp 406 . . 3 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ π‘Œ ∈ 𝑉) ∧ βˆƒπ‘  ∈ (Atomsβ€˜πΎ)(𝑋𝐢(𝑋(joinβ€˜πΎ)𝑠) ∧ (𝑋(joinβ€˜πΎ)𝑠) ≀ π‘Œ)) β†’ π‘‹πΆπ‘Œ)
8731, 86syldan 590 . 2 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ π‘Œ ∈ 𝑉) ∧ 𝑋(ltβ€˜πΎ)π‘Œ) β†’ π‘‹πΆπ‘Œ)
8817, 87syldan 590 1 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ π‘Œ ∈ 𝑉) ∧ 𝑋 ≀ π‘Œ) β†’ π‘‹πΆπ‘Œ)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1534   ∈ wcel 2099   β‰  wne 2935  βˆƒwrex 3065   class class class wbr 5142  β€˜cfv 6542  (class class class)co 7414  Basecbs 17171  lecple 17231  ltcplt 18291  joincjn 18294  Latclat 18414   β‹– ccvr 38671  Atomscatm 38672  HLchlt 38759  LPlanesclpl 38902  LVolsclvol 38903
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  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 7370  df-ov 7417  df-oprab 7418  df-proset 18278  df-poset 18296  df-plt 18313  df-lub 18329  df-glb 18330  df-join 18331  df-meet 18332  df-p0 18408  df-lat 18415  df-clat 18482  df-oposet 38585  df-ol 38587  df-oml 38588  df-covers 38675  df-ats 38676  df-atl 38707  df-cvlat 38731  df-hlat 38760  df-llines 38908  df-lplanes 38909  df-lvols 38910
This theorem is referenced by:  lplncvrlvol  39026  lvolcmp  39027  2lplnm2N  39031  2lplnmj  39032
  Copyright terms: Public domain W3C validator