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

Theorem islvol5 34380
 Description: The predicate "is a 3-dim lattice volume" in terms of atoms. (Contributed by NM, 1-Jul-2012.)
Hypotheses
Ref Expression
islvol5.b 𝐵 = (Base‘𝐾)
islvol5.l = (le‘𝐾)
islvol5.j = (join‘𝐾)
islvol5.a 𝐴 = (Atoms‘𝐾)
islvol5.v 𝑉 = (LVols‘𝐾)
Assertion
Ref Expression
islvol5 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (𝑋𝑉 ↔ ∃𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠))))
Distinct variable groups:   𝑞,𝑝,𝑟,𝑠,𝐴   𝐵,𝑝,𝑞,𝑟,𝑠   ,𝑝,𝑞,𝑟,𝑠   𝐾,𝑝,𝑞,𝑟,𝑠   ,𝑝,𝑞,𝑟,𝑠   𝑋,𝑝,𝑞,𝑟,𝑠
Allowed substitution hints:   𝑉(𝑠,𝑟,𝑞,𝑝)

Proof of Theorem islvol5
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 islvol5.b . . 3 𝐵 = (Base‘𝐾)
2 islvol5.l . . 3 = (le‘𝐾)
3 islvol5.j . . 3 = (join‘𝐾)
4 islvol5.a . . 3 𝐴 = (Atoms‘𝐾)
5 eqid 2621 . . 3 (LPlanes‘𝐾) = (LPlanes‘𝐾)
6 islvol5.v . . 3 𝑉 = (LVols‘𝐾)
71, 2, 3, 4, 5, 6islvol3 34377 . 2 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (𝑋𝑉 ↔ ∃𝑦 ∈ (LPlanes‘𝐾)∃𝑠𝐴𝑠 𝑦𝑋 = (𝑦 𝑠))))
8 rexcom4 3214 . . . . . . . . 9 (∃𝑟𝐴𝑦𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑦𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
98rexbii 3035 . . . . . . . 8 (∃𝑞𝐴𝑟𝐴𝑦𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑞𝐴𝑦𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
10 rexcom4 3214 . . . . . . . 8 (∃𝑞𝐴𝑦𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑦𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
119, 10bitri 264 . . . . . . 7 (∃𝑞𝐴𝑟𝐴𝑦𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑦𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
1211rexbii 3035 . . . . . 6 (∃𝑝𝐴𝑞𝐴𝑟𝐴𝑦𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑝𝐴𝑦𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
13 rexcom4 3214 . . . . . 6 (∃𝑝𝐴𝑦𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑦𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
1412, 13bitri 264 . . . . 5 (∃𝑝𝐴𝑞𝐴𝑟𝐴𝑦𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑦𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
15 hllat 34165 . . . . . . . . . . 11 (𝐾 ∈ HL → 𝐾 ∈ Lat)
1615ad3antrrr 765 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ (𝑝𝐴𝑞𝐴)) ∧ 𝑟𝐴) → 𝐾 ∈ Lat)
17 simplll 797 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ (𝑝𝐴𝑞𝐴)) ∧ 𝑟𝐴) → 𝐾 ∈ HL)
18 simplrl 799 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ (𝑝𝐴𝑞𝐴)) ∧ 𝑟𝐴) → 𝑝𝐴)
19 simplrr 800 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ (𝑝𝐴𝑞𝐴)) ∧ 𝑟𝐴) → 𝑞𝐴)
201, 3, 4hlatjcl 34168 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ 𝑝𝐴𝑞𝐴) → (𝑝 𝑞) ∈ 𝐵)
2117, 18, 19, 20syl3anc 1323 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ (𝑝𝐴𝑞𝐴)) ∧ 𝑟𝐴) → (𝑝 𝑞) ∈ 𝐵)
221, 4atbase 34091 . . . . . . . . . . 11 (𝑟𝐴𝑟𝐵)
2322adantl 482 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ (𝑝𝐴𝑞𝐴)) ∧ 𝑟𝐴) → 𝑟𝐵)
241, 3latjcl 16983 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝑝 𝑞) ∈ 𝐵𝑟𝐵) → ((𝑝 𝑞) 𝑟) ∈ 𝐵)
2516, 21, 23, 24syl3anc 1323 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ (𝑝𝐴𝑞𝐴)) ∧ 𝑟𝐴) → ((𝑝 𝑞) 𝑟) ∈ 𝐵)
2625biantrurd 529 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ (𝑝𝐴𝑞𝐴)) ∧ 𝑟𝐴) → (∃𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠)) ↔ (((𝑝 𝑞) 𝑟) ∈ 𝐵 ∧ ∃𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠)))))
27 r19.41v 3082 . . . . . . . . . . 11 (∃𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ (∃𝑠𝐴 (𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
28 df-3an 1038 . . . . . . . . . . . . 13 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟)) ↔ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ 𝑦 = ((𝑝 𝑞) 𝑟)))
2928anbi2i 729 . . . . . . . . . . . 12 ((∃𝑠𝐴 (𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ (∃𝑠𝐴 (𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
30 an13 839 . . . . . . . . . . . 12 ((∃𝑠𝐴 (𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ (𝑦 = ((𝑝 𝑞) 𝑟) ∧ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ ∃𝑠𝐴 (𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))))))
3129, 30bitri 264 . . . . . . . . . . 11 ((∃𝑠𝐴 (𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ (𝑦 = ((𝑝 𝑞) 𝑟) ∧ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ ∃𝑠𝐴 (𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))))))
3227, 31bitri 264 . . . . . . . . . 10 (∃𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ (𝑦 = ((𝑝 𝑞) 𝑟) ∧ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ ∃𝑠𝐴 (𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))))))
3332exbii 1771 . . . . . . . . 9 (∃𝑦𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑦(𝑦 = ((𝑝 𝑞) 𝑟) ∧ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ ∃𝑠𝐴 (𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))))))
34 ovex 6638 . . . . . . . . . 10 ((𝑝 𝑞) 𝑟) ∈ V
35 an12 837 . . . . . . . . . . . . 13 (((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ (𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠)))) ↔ (𝑦𝐵 ∧ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠)))))
36 eleq1 2686 . . . . . . . . . . . . . 14 (𝑦 = ((𝑝 𝑞) 𝑟) → (𝑦𝐵 ↔ ((𝑝 𝑞) 𝑟) ∈ 𝐵))
37 breq2 4622 . . . . . . . . . . . . . . . . . 18 (𝑦 = ((𝑝 𝑞) 𝑟) → (𝑠 𝑦𝑠 ((𝑝 𝑞) 𝑟)))
3837notbid 308 . . . . . . . . . . . . . . . . 17 (𝑦 = ((𝑝 𝑞) 𝑟) → (¬ 𝑠 𝑦 ↔ ¬ 𝑠 ((𝑝 𝑞) 𝑟)))
39 oveq1 6617 . . . . . . . . . . . . . . . . . 18 (𝑦 = ((𝑝 𝑞) 𝑟) → (𝑦 𝑠) = (((𝑝 𝑞) 𝑟) 𝑠))
4039eqeq2d 2631 . . . . . . . . . . . . . . . . 17 (𝑦 = ((𝑝 𝑞) 𝑟) → (𝑋 = (𝑦 𝑠) ↔ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠)))
4138, 40anbi12d 746 . . . . . . . . . . . . . . . 16 (𝑦 = ((𝑝 𝑞) 𝑟) → ((¬ 𝑠 𝑦𝑋 = (𝑦 𝑠)) ↔ (¬ 𝑠 ((𝑝 𝑞) 𝑟) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠))))
4241anbi2d 739 . . . . . . . . . . . . . . 15 (𝑦 = ((𝑝 𝑞) 𝑟) → (((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ↔ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ (¬ 𝑠 ((𝑝 𝑞) 𝑟) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠)))))
43 anass 680 . . . . . . . . . . . . . . . 16 ((((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠)) ↔ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ (¬ 𝑠 ((𝑝 𝑞) 𝑟) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠))))
44 df-3an 1038 . . . . . . . . . . . . . . . . . 18 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ↔ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)))
4544bicomi 214 . . . . . . . . . . . . . . . . 17 (((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ↔ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)))
4645anbi1i 730 . . . . . . . . . . . . . . . 16 ((((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠)) ↔ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠)))
4743, 46bitr3i 266 . . . . . . . . . . . . . . 15 (((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ (¬ 𝑠 ((𝑝 𝑞) 𝑟) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠))) ↔ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠)))
4842, 47syl6bb 276 . . . . . . . . . . . . . 14 (𝑦 = ((𝑝 𝑞) 𝑟) → (((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ↔ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠))))
4936, 48anbi12d 746 . . . . . . . . . . . . 13 (𝑦 = ((𝑝 𝑞) 𝑟) → ((𝑦𝐵 ∧ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠)))) ↔ (((𝑝 𝑞) 𝑟) ∈ 𝐵 ∧ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠)))))
5035, 49syl5bb 272 . . . . . . . . . . . 12 (𝑦 = ((𝑝 𝑞) 𝑟) → (((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ (𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠)))) ↔ (((𝑝 𝑞) 𝑟) ∈ 𝐵 ∧ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠)))))
5150rexbidv 3046 . . . . . . . . . . 11 (𝑦 = ((𝑝 𝑞) 𝑟) → (∃𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ (𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠)))) ↔ ∃𝑠𝐴 (((𝑝 𝑞) 𝑟) ∈ 𝐵 ∧ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠)))))
52 r19.42v 3085 . . . . . . . . . . 11 (∃𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ (𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠)))) ↔ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ ∃𝑠𝐴 (𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠)))))
53 r19.42v 3085 . . . . . . . . . . 11 (∃𝑠𝐴 (((𝑝 𝑞) 𝑟) ∈ 𝐵 ∧ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠))) ↔ (((𝑝 𝑞) 𝑟) ∈ 𝐵 ∧ ∃𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠))))
5451, 52, 533bitr3g 302 . . . . . . . . . 10 (𝑦 = ((𝑝 𝑞) 𝑟) → (((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ ∃𝑠𝐴 (𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠)))) ↔ (((𝑝 𝑞) 𝑟) ∈ 𝐵 ∧ ∃𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠)))))
5534, 54ceqsexv 3231 . . . . . . . . 9 (∃𝑦(𝑦 = ((𝑝 𝑞) 𝑟) ∧ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ ∃𝑠𝐴 (𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))))) ↔ (((𝑝 𝑞) 𝑟) ∈ 𝐵 ∧ ∃𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠))))
5633, 55bitri 264 . . . . . . . 8 (∃𝑦𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ (((𝑝 𝑞) 𝑟) ∈ 𝐵 ∧ ∃𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠))))
5726, 56syl6rbbr 279 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ (𝑝𝐴𝑞𝐴)) ∧ 𝑟𝐴) → (∃𝑦𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠))))
5857rexbidva 3043 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ (𝑝𝐴𝑞𝐴)) → (∃𝑟𝐴𝑦𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑟𝐴𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠))))
59582rexbidva 3050 . . . . 5 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (∃𝑝𝐴𝑞𝐴𝑟𝐴𝑦𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠))))
6014, 59syl5rbbr 275 . . . 4 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (∃𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠)) ↔ ∃𝑦𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟)))))
611, 2, 3, 4, 5islpln2 34337 . . . . . . . . . . 11 (𝐾 ∈ HL → (𝑦 ∈ (LPlanes‘𝐾) ↔ (𝑦𝐵 ∧ ∃𝑝𝐴𝑞𝐴𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟)))))
6261adantr 481 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (𝑦 ∈ (LPlanes‘𝐾) ↔ (𝑦𝐵 ∧ ∃𝑝𝐴𝑞𝐴𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟)))))
6362anbi1d 740 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑋𝐵) → ((𝑦 ∈ (LPlanes‘𝐾) ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ↔ ((𝑦𝐵 ∧ ∃𝑝𝐴𝑞𝐴𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠)))))
64 r19.42v 3085 . . . . . . . . . 10 (∃𝑝𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ ∃𝑞𝐴𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ ∃𝑝𝐴𝑞𝐴𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
65 r19.42v 3085 . . . . . . . . . . . . 13 (∃𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ ∃𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
6665rexbii 3035 . . . . . . . . . . . 12 (∃𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑞𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ ∃𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
67 r19.42v 3085 . . . . . . . . . . . 12 (∃𝑞𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ ∃𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ ∃𝑞𝐴𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
6866, 67bitri 264 . . . . . . . . . . 11 (∃𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ ∃𝑞𝐴𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
6968rexbii 3035 . . . . . . . . . 10 (∃𝑝𝐴𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑝𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ ∃𝑞𝐴𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
70 an32 838 . . . . . . . . . 10 (((𝑦𝐵 ∧ ∃𝑝𝐴𝑞𝐴𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ↔ ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ ∃𝑝𝐴𝑞𝐴𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
7164, 69, 703bitr4ri 293 . . . . . . . . 9 (((𝑦𝐵 ∧ ∃𝑝𝐴𝑞𝐴𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ↔ ∃𝑝𝐴𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
7263, 71syl6bb 276 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑋𝐵) → ((𝑦 ∈ (LPlanes‘𝐾) ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ↔ ∃𝑝𝐴𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟)))))
7372rexbidv 3046 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (∃𝑠𝐴 (𝑦 ∈ (LPlanes‘𝐾) ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ↔ ∃𝑠𝐴𝑝𝐴𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟)))))
74 rexcom 3092 . . . . . . . . . . 11 (∃𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑠𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
7574rexbii 3035 . . . . . . . . . 10 (∃𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑞𝐴𝑠𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
76 rexcom 3092 . . . . . . . . . 10 (∃𝑞𝐴𝑠𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑠𝐴𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
7775, 76bitri 264 . . . . . . . . 9 (∃𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑠𝐴𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
7877rexbii 3035 . . . . . . . 8 (∃𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑝𝐴𝑠𝐴𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
79 rexcom 3092 . . . . . . . 8 (∃𝑝𝐴𝑠𝐴𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑠𝐴𝑝𝐴𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
8078, 79bitri 264 . . . . . . 7 (∃𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑠𝐴𝑝𝐴𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
8173, 80syl6rbbr 279 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (∃𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑠𝐴 (𝑦 ∈ (LPlanes‘𝐾) ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠)))))
82 r19.42v 3085 . . . . . 6 (∃𝑠𝐴 (𝑦 ∈ (LPlanes‘𝐾) ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ↔ (𝑦 ∈ (LPlanes‘𝐾) ∧ ∃𝑠𝐴𝑠 𝑦𝑋 = (𝑦 𝑠))))
8381, 82syl6bb 276 . . . . 5 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (∃𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ (𝑦 ∈ (LPlanes‘𝐾) ∧ ∃𝑠𝐴𝑠 𝑦𝑋 = (𝑦 𝑠)))))
8483exbidv 1847 . . . 4 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (∃𝑦𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑦(𝑦 ∈ (LPlanes‘𝐾) ∧ ∃𝑠𝐴𝑠 𝑦𝑋 = (𝑦 𝑠)))))
8560, 84bitrd 268 . . 3 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (∃𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠)) ↔ ∃𝑦(𝑦 ∈ (LPlanes‘𝐾) ∧ ∃𝑠𝐴𝑠 𝑦𝑋 = (𝑦 𝑠)))))
86 df-rex 2913 . . 3 (∃𝑦 ∈ (LPlanes‘𝐾)∃𝑠𝐴𝑠 𝑦𝑋 = (𝑦 𝑠)) ↔ ∃𝑦(𝑦 ∈ (LPlanes‘𝐾) ∧ ∃𝑠𝐴𝑠 𝑦𝑋 = (𝑦 𝑠))))
8785, 86syl6rbbr 279 . 2 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (∃𝑦 ∈ (LPlanes‘𝐾)∃𝑠𝐴𝑠 𝑦𝑋 = (𝑦 𝑠)) ↔ ∃𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠))))
887, 87bitrd 268 1 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (𝑋𝑉 ↔ ∃𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1036   = wceq 1480  ∃wex 1701   ∈ wcel 1987   ≠ wne 2790  ∃wrex 2908   class class class wbr 4618  ‘cfv 5852  (class class class)co 6610  Basecbs 15792  lecple 15880  joincjn 16876  Latclat 16977  Atomscatm 34065  HLchlt 34152  LPlanesclpl 34293  LVolsclvol 34294 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-riota 6571  df-ov 6613  df-oprab 6614  df-preset 16860  df-poset 16878  df-plt 16890  df-lub 16906  df-glb 16907  df-join 16908  df-meet 16909  df-p0 16971  df-lat 16978  df-clat 17040  df-oposet 33978  df-ol 33980  df-oml 33981  df-covers 34068  df-ats 34069  df-atl 34100  df-cvlat 34124  df-hlat 34153  df-llines 34299  df-lplanes 34300  df-lvols 34301 This theorem is referenced by:  islvol2  34381  lvoli2  34382
 Copyright terms: Public domain W3C validator