Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pmodl42N Structured version   Visualization version   GIF version
Theorem pmodl42N 38420
Description: Lemma derived from modular law. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.)
Hypotheses
Ref Expression
pmodl42.s 𝑆 = (PSubSpβ€˜πΎ)
pmodl42.p + = (+π‘ƒβ€˜πΎ)
Assertion
Ref Expression
pmodl42N (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ (((𝑋 + π‘Œ) + 𝑍) ∩ ((𝑋 + π‘Œ) + π‘Š)) = ((𝑋 + π‘Œ) + ((𝑋 + 𝑍) ∩ (π‘Œ + π‘Š))))
Proof of Theorem pmodl42N
StepHypRef Expression
1 simpl1 1191 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ 𝐾 ∈ HL)
2 simpl3 1193 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ π‘Œ ∈ 𝑆)
3 eqid 2731 . . . . . . 7 (Atomsβ€˜πΎ) = (Atomsβ€˜πΎ)
4 pmodl42.s . . . . . . 7 𝑆 = (PSubSpβ€˜πΎ)
53, 4psubssat 38323 . . . . . 6 ((𝐾 ∈ HL ∧ π‘Œ ∈ 𝑆) β†’ π‘Œ βŠ† (Atomsβ€˜πΎ))
61, 2, 5syl2anc 584 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ π‘Œ βŠ† (Atomsβ€˜πΎ))
7 simpl2 1192 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ 𝑋 ∈ 𝑆)
83, 4psubssat 38323 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆) β†’ 𝑋 βŠ† (Atomsβ€˜πΎ))
91, 7, 8syl2anc 584 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ 𝑋 βŠ† (Atomsβ€˜πΎ))
10 simprl 769 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ 𝑍 ∈ 𝑆)
113, 4psubssat 38323 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑍 ∈ 𝑆) β†’ 𝑍 βŠ† (Atomsβ€˜πΎ))
121, 10, 11syl2anc 584 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ 𝑍 βŠ† (Atomsβ€˜πΎ))
13 pmodl42.p . . . . . . 7 + = (+π‘ƒβ€˜πΎ)
143, 13paddssat 38383 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑋 βŠ† (Atomsβ€˜πΎ) ∧ 𝑍 βŠ† (Atomsβ€˜πΎ)) β†’ (𝑋 + 𝑍) βŠ† (Atomsβ€˜πΎ))
151, 9, 12, 14syl3anc 1371 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ (𝑋 + 𝑍) βŠ† (Atomsβ€˜πΎ))
16 simprr 771 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ π‘Š ∈ 𝑆)
174, 13paddclN 38411 . . . . . 6 ((𝐾 ∈ HL ∧ π‘Œ ∈ 𝑆 ∧ π‘Š ∈ 𝑆) β†’ (π‘Œ + π‘Š) ∈ 𝑆)
181, 2, 16, 17syl3anc 1371 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ (π‘Œ + π‘Š) ∈ 𝑆)
193, 4psubssat 38323 . . . . . . 7 ((𝐾 ∈ HL ∧ π‘Š ∈ 𝑆) β†’ π‘Š βŠ† (Atomsβ€˜πΎ))
201, 16, 19syl2anc 584 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ π‘Š βŠ† (Atomsβ€˜πΎ))
213, 13sspadd1 38384 . . . . . 6 ((𝐾 ∈ HL ∧ π‘Œ βŠ† (Atomsβ€˜πΎ) ∧ π‘Š βŠ† (Atomsβ€˜πΎ)) β†’ π‘Œ βŠ† (π‘Œ + π‘Š))
221, 6, 20, 21syl3anc 1371 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ π‘Œ βŠ† (π‘Œ + π‘Š))
233, 4, 13pmod1i 38417 . . . . . 6 ((𝐾 ∈ HL ∧ (π‘Œ βŠ† (Atomsβ€˜πΎ) ∧ (𝑋 + 𝑍) βŠ† (Atomsβ€˜πΎ) ∧ (π‘Œ + π‘Š) ∈ 𝑆)) β†’ (π‘Œ βŠ† (π‘Œ + π‘Š) β†’ ((π‘Œ + (𝑋 + 𝑍)) ∩ (π‘Œ + π‘Š)) = (π‘Œ + ((𝑋 + 𝑍) ∩ (π‘Œ + π‘Š)))))
24233impia 1117 . . . . 5 ((𝐾 ∈ HL ∧ (π‘Œ βŠ† (Atomsβ€˜πΎ) ∧ (𝑋 + 𝑍) βŠ† (Atomsβ€˜πΎ) ∧ (π‘Œ + π‘Š) ∈ 𝑆) ∧ π‘Œ βŠ† (π‘Œ + π‘Š)) β†’ ((π‘Œ + (𝑋 + 𝑍)) ∩ (π‘Œ + π‘Š)) = (π‘Œ + ((𝑋 + 𝑍) ∩ (π‘Œ + π‘Š))))
251, 6, 15, 18, 22, 24syl131anc 1383 . . . 4 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ ((π‘Œ + (𝑋 + 𝑍)) ∩ (π‘Œ + π‘Š)) = (π‘Œ + ((𝑋 + 𝑍) ∩ (π‘Œ + π‘Š))))
26 incom 4181 . . . 4 ((π‘Œ + (𝑋 + 𝑍)) ∩ (π‘Œ + π‘Š)) = ((π‘Œ + π‘Š) ∩ (π‘Œ + (𝑋 + 𝑍)))
2725, 26eqtr3di 2786 . . 3 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ (π‘Œ + ((𝑋 + 𝑍) ∩ (π‘Œ + π‘Š))) = ((π‘Œ + π‘Š) ∩ (π‘Œ + (𝑋 + 𝑍))))
2827oveq2d 7393 . 2 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ (𝑋 + (π‘Œ + ((𝑋 + 𝑍) ∩ (π‘Œ + π‘Š)))) = (𝑋 + ((π‘Œ + π‘Š) ∩ (π‘Œ + (𝑋 + 𝑍)))))
29 ssinss1 4217 . . . 4 ((𝑋 + 𝑍) βŠ† (Atomsβ€˜πΎ) β†’ ((𝑋 + 𝑍) ∩ (π‘Œ + π‘Š)) βŠ† (Atomsβ€˜πΎ))
3015, 29syl 17 . . 3 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ ((𝑋 + 𝑍) ∩ (π‘Œ + π‘Š)) βŠ† (Atomsβ€˜πΎ))
313, 13paddass 38407 . . 3 ((𝐾 ∈ HL ∧ (𝑋 βŠ† (Atomsβ€˜πΎ) ∧ π‘Œ βŠ† (Atomsβ€˜πΎ) ∧ ((𝑋 + 𝑍) ∩ (π‘Œ + π‘Š)) βŠ† (Atomsβ€˜πΎ))) β†’ ((𝑋 + π‘Œ) + ((𝑋 + 𝑍) ∩ (π‘Œ + π‘Š))) = (𝑋 + (π‘Œ + ((𝑋 + 𝑍) ∩ (π‘Œ + π‘Š)))))
321, 9, 6, 30, 31syl13anc 1372 . 2 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ ((𝑋 + π‘Œ) + ((𝑋 + 𝑍) ∩ (π‘Œ + π‘Š))) = (𝑋 + (π‘Œ + ((𝑋 + 𝑍) ∩ (π‘Œ + π‘Š)))))
333, 13paddass 38407 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑋 βŠ† (Atomsβ€˜πΎ) ∧ π‘Œ βŠ† (Atomsβ€˜πΎ) ∧ 𝑍 βŠ† (Atomsβ€˜πΎ))) β†’ ((𝑋 + π‘Œ) + 𝑍) = (𝑋 + (π‘Œ + 𝑍)))
341, 9, 6, 12, 33syl13anc 1372 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ ((𝑋 + π‘Œ) + 𝑍) = (𝑋 + (π‘Œ + 𝑍)))
353, 13padd12N 38408 . . . . . . 7 ((𝐾 ∈ HL ∧ (𝑋 βŠ† (Atomsβ€˜πΎ) ∧ π‘Œ βŠ† (Atomsβ€˜πΎ) ∧ 𝑍 βŠ† (Atomsβ€˜πΎ))) β†’ (𝑋 + (π‘Œ + 𝑍)) = (π‘Œ + (𝑋 + 𝑍)))
361, 9, 6, 12, 35syl13anc 1372 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ (𝑋 + (π‘Œ + 𝑍)) = (π‘Œ + (𝑋 + 𝑍)))
3734, 36eqtrd 2771 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ ((𝑋 + π‘Œ) + 𝑍) = (π‘Œ + (𝑋 + 𝑍)))
383, 13paddass 38407 . . . . . 6 ((𝐾 ∈ HL ∧ (𝑋 βŠ† (Atomsβ€˜πΎ) ∧ π‘Œ βŠ† (Atomsβ€˜πΎ) ∧ π‘Š βŠ† (Atomsβ€˜πΎ))) β†’ ((𝑋 + π‘Œ) + π‘Š) = (𝑋 + (π‘Œ + π‘Š)))
391, 9, 6, 20, 38syl13anc 1372 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ ((𝑋 + π‘Œ) + π‘Š) = (𝑋 + (π‘Œ + π‘Š)))
4037, 39ineq12d 4193 . . . 4 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ (((𝑋 + π‘Œ) + 𝑍) ∩ ((𝑋 + π‘Œ) + π‘Š)) = ((π‘Œ + (𝑋 + 𝑍)) ∩ (𝑋 + (π‘Œ + π‘Š))))
41 incom 4181 . . . 4 ((π‘Œ + (𝑋 + 𝑍)) ∩ (𝑋 + (π‘Œ + π‘Š))) = ((𝑋 + (π‘Œ + π‘Š)) ∩ (π‘Œ + (𝑋 + 𝑍)))
4240, 41eqtrdi 2787 . . 3 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ (((𝑋 + π‘Œ) + 𝑍) ∩ ((𝑋 + π‘Œ) + π‘Š)) = ((𝑋 + (π‘Œ + π‘Š)) ∩ (π‘Œ + (𝑋 + 𝑍))))
433, 4psubssat 38323 . . . . 5 ((𝐾 ∈ HL ∧ (π‘Œ + π‘Š) ∈ 𝑆) β†’ (π‘Œ + π‘Š) βŠ† (Atomsβ€˜πΎ))
441, 18, 43syl2anc 584 . . . 4 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ (π‘Œ + π‘Š) βŠ† (Atomsβ€˜πΎ))
454, 13paddclN 38411 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑍 ∈ 𝑆) β†’ (𝑋 + 𝑍) ∈ 𝑆)
461, 7, 10, 45syl3anc 1371 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ (𝑋 + 𝑍) ∈ 𝑆)
474, 13paddclN 38411 . . . . 5 ((𝐾 ∈ HL ∧ π‘Œ ∈ 𝑆 ∧ (𝑋 + 𝑍) ∈ 𝑆) β†’ (π‘Œ + (𝑋 + 𝑍)) ∈ 𝑆)
481, 2, 46, 47syl3anc 1371 . . . 4 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ (π‘Œ + (𝑋 + 𝑍)) ∈ 𝑆)
493, 13sspadd1 38384 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑋 βŠ† (Atomsβ€˜πΎ) ∧ 𝑍 βŠ† (Atomsβ€˜πΎ)) β†’ 𝑋 βŠ† (𝑋 + 𝑍))
501, 9, 12, 49syl3anc 1371 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ 𝑋 βŠ† (𝑋 + 𝑍))
513, 13sspadd2 38385 . . . . . 6 ((𝐾 ∈ HL ∧ (𝑋 + 𝑍) βŠ† (Atomsβ€˜πΎ) ∧ π‘Œ βŠ† (Atomsβ€˜πΎ)) β†’ (𝑋 + 𝑍) βŠ† (π‘Œ + (𝑋 + 𝑍)))
521, 15, 6, 51syl3anc 1371 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ (𝑋 + 𝑍) βŠ† (π‘Œ + (𝑋 + 𝑍)))
5350, 52sstrd 3972 . . . 4 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ 𝑋 βŠ† (π‘Œ + (𝑋 + 𝑍)))
543, 4, 13pmod1i 38417 . . . . 5 ((𝐾 ∈ HL ∧ (𝑋 βŠ† (Atomsβ€˜πΎ) ∧ (π‘Œ + π‘Š) βŠ† (Atomsβ€˜πΎ) ∧ (π‘Œ + (𝑋 + 𝑍)) ∈ 𝑆)) β†’ (𝑋 βŠ† (π‘Œ + (𝑋 + 𝑍)) β†’ ((𝑋 + (π‘Œ + π‘Š)) ∩ (π‘Œ + (𝑋 + 𝑍))) = (𝑋 + ((π‘Œ + π‘Š) ∩ (π‘Œ + (𝑋 + 𝑍))))))
55543impia 1117 . . . 4 ((𝐾 ∈ HL ∧ (𝑋 βŠ† (Atomsβ€˜πΎ) ∧ (π‘Œ + π‘Š) βŠ† (Atomsβ€˜πΎ) ∧ (π‘Œ + (𝑋 + 𝑍)) ∈ 𝑆) ∧ 𝑋 βŠ† (π‘Œ + (𝑋 + 𝑍))) β†’ ((𝑋 + (π‘Œ + π‘Š)) ∩ (π‘Œ + (𝑋 + 𝑍))) = (𝑋 + ((π‘Œ + π‘Š) ∩ (π‘Œ + (𝑋 + 𝑍)))))
561, 9, 44, 48, 53, 55syl131anc 1383 . . 3 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ ((𝑋 + (π‘Œ + π‘Š)) ∩ (π‘Œ + (𝑋 + 𝑍))) = (𝑋 + ((π‘Œ + π‘Š) ∩ (π‘Œ + (𝑋 + 𝑍)))))
5742, 56eqtrd 2771 . 2 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ (((𝑋 + π‘Œ) + 𝑍) ∩ ((𝑋 + π‘Œ) + π‘Š)) = (𝑋 + ((π‘Œ + π‘Š) ∩ (π‘Œ + (𝑋 + 𝑍)))))
5828, 32, 573eqtr4rd 2782 1 (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ π‘Œ ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ π‘Š ∈ 𝑆)) β†’ (((𝑋 + π‘Œ) + 𝑍) ∩ ((𝑋 + π‘Œ) + π‘Š)) = ((𝑋 + π‘Œ) + ((𝑋 + 𝑍) ∩ (π‘Œ + π‘Š))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   ∩ cin 3927   βŠ† wss 3928  β€˜cfv 6516  (class class class)co 7377  Atomscatm 37831  HLchlt 37918  PSubSpcpsubsp 38065  +𝑃cpadd 38364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5262  ax-sep 5276  ax-nul 5283  ax-pow 5340  ax-pr 5404  ax-un 7692
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3365  df-rab 3419  df-v 3461  df-sbc 3758  df-csb 3874  df-dif 3931  df-un 3933  df-in 3935  df-ss 3945  df-nul 4303  df-if 4507  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4886  df-iun 4976  df-br 5126  df-opab 5188  df-mpt 5209  df-id 5551  df-xp 5659  df-rel 5660  df-cnv 5661  df-co 5662  df-dm 5663  df-rn 5664  df-res 5665  df-ima 5666  df-iota 6468  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-riota 7333  df-ov 7380  df-oprab 7381  df-mpo 7382  df-1st 7941  df-2nd 7942  df-proset 18213  df-poset 18231  df-plt 18248  df-lub 18264  df-glb 18265  df-join 18266  df-meet 18267  df-p0 18343  df-lat 18350  df-clat 18417  df-oposet 37744  df-ol 37746  df-oml 37747  df-covers 37834  df-ats 37835  df-atl 37866  df-cvlat 37890  df-hlat 37919  df-psubsp 38072  df-padd 38365
This theorem is referenced by:  pl42lem4N  38551
  Copyright terms: Public domain W3C validator