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

Theorem islvol5 39056
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 2727 . . 3 (LPlanes‘𝐾) = (LPlanes‘𝐾)
6 islvol5.v . . 3 𝑉 = (LVols‘𝐾)
71, 2, 3, 4, 5, 6islvol3 39053 . 2 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (𝑋𝑉 ↔ ∃𝑦 ∈ (LPlanes‘𝐾)∃𝑠𝐴𝑠 𝑦𝑋 = (𝑦 𝑠))))
8 df-rex 3067 . . 3 (∃𝑦 ∈ (LPlanes‘𝐾)∃𝑠𝐴𝑠 𝑦𝑋 = (𝑦 𝑠)) ↔ ∃𝑦(𝑦 ∈ (LPlanes‘𝐾) ∧ ∃𝑠𝐴𝑠 𝑦𝑋 = (𝑦 𝑠))))
9 r19.41v 3184 . . . . . . . . . . 11 (∃𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ (∃𝑠𝐴 (𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
10 df-3an 1086 . . . . . . . . . . . . 13 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟)) ↔ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ 𝑦 = ((𝑝 𝑞) 𝑟)))
1110anbi2i 621 . . . . . . . . . . . 12 ((∃𝑠𝐴 (𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ (∃𝑠𝐴 (𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
12 an13 645 . . . . . . . . . . . 12 ((∃𝑠𝐴 (𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ (𝑦 = ((𝑝 𝑞) 𝑟) ∧ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ ∃𝑠𝐴 (𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))))))
1311, 12bitri 274 . . . . . . . . . . 11 ((∃𝑠𝐴 (𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ (𝑦 = ((𝑝 𝑞) 𝑟) ∧ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ ∃𝑠𝐴 (𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))))))
149, 13bitri 274 . . . . . . . . . 10 (∃𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ (𝑦 = ((𝑝 𝑞) 𝑟) ∧ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ ∃𝑠𝐴 (𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))))))
1514exbii 1842 . . . . . . . . 9 (∃𝑦𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑦(𝑦 = ((𝑝 𝑞) 𝑟) ∧ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ ∃𝑠𝐴 (𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))))))
16 ovex 7457 . . . . . . . . . 10 ((𝑝 𝑞) 𝑟) ∈ V
17 an12 643 . . . . . . . . . . . . 13 (((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ (𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠)))) ↔ (𝑦𝐵 ∧ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠)))))
18 eleq1 2816 . . . . . . . . . . . . . 14 (𝑦 = ((𝑝 𝑞) 𝑟) → (𝑦𝐵 ↔ ((𝑝 𝑞) 𝑟) ∈ 𝐵))
19 breq2 5154 . . . . . . . . . . . . . . . . . 18 (𝑦 = ((𝑝 𝑞) 𝑟) → (𝑠 𝑦𝑠 ((𝑝 𝑞) 𝑟)))
2019notbid 317 . . . . . . . . . . . . . . . . 17 (𝑦 = ((𝑝 𝑞) 𝑟) → (¬ 𝑠 𝑦 ↔ ¬ 𝑠 ((𝑝 𝑞) 𝑟)))
21 oveq1 7431 . . . . . . . . . . . . . . . . . 18 (𝑦 = ((𝑝 𝑞) 𝑟) → (𝑦 𝑠) = (((𝑝 𝑞) 𝑟) 𝑠))
2221eqeq2d 2738 . . . . . . . . . . . . . . . . 17 (𝑦 = ((𝑝 𝑞) 𝑟) → (𝑋 = (𝑦 𝑠) ↔ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠)))
2320, 22anbi12d 630 . . . . . . . . . . . . . . . 16 (𝑦 = ((𝑝 𝑞) 𝑟) → ((¬ 𝑠 𝑦𝑋 = (𝑦 𝑠)) ↔ (¬ 𝑠 ((𝑝 𝑞) 𝑟) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠))))
2423anbi2d 628 . . . . . . . . . . . . . . 15 (𝑦 = ((𝑝 𝑞) 𝑟) → (((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ↔ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ (¬ 𝑠 ((𝑝 𝑞) 𝑟) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠)))))
25 anass 467 . . . . . . . . . . . . . . . 16 ((((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠)) ↔ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ (¬ 𝑠 ((𝑝 𝑞) 𝑟) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠))))
26 df-3an 1086 . . . . . . . . . . . . . . . . . 18 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ↔ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)))
2726bicomi 223 . . . . . . . . . . . . . . . . 17 (((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ↔ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)))
2827anbi1i 622 . . . . . . . . . . . . . . . 16 ((((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠)) ↔ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠)))
2925, 28bitr3i 276 . . . . . . . . . . . . . . 15 (((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ (¬ 𝑠 ((𝑝 𝑞) 𝑟) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠))) ↔ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠)))
3024, 29bitrdi 286 . . . . . . . . . . . . . 14 (𝑦 = ((𝑝 𝑞) 𝑟) → (((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ↔ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠))))
3118, 30anbi12d 630 . . . . . . . . . . . . 13 (𝑦 = ((𝑝 𝑞) 𝑟) → ((𝑦𝐵 ∧ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠)))) ↔ (((𝑝 𝑞) 𝑟) ∈ 𝐵 ∧ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠)))))
3217, 31bitrid 282 . . . . . . . . . . . 12 (𝑦 = ((𝑝 𝑞) 𝑟) → (((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ (𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠)))) ↔ (((𝑝 𝑞) 𝑟) ∈ 𝐵 ∧ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠)))))
3332rexbidv 3174 . . . . . . . . . . 11 (𝑦 = ((𝑝 𝑞) 𝑟) → (∃𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ (𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠)))) ↔ ∃𝑠𝐴 (((𝑝 𝑞) 𝑟) ∈ 𝐵 ∧ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠)))))
34 r19.42v 3186 . . . . . . . . . . 11 (∃𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ (𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠)))) ↔ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ ∃𝑠𝐴 (𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠)))))
35 r19.42v 3186 . . . . . . . . . . 11 (∃𝑠𝐴 (((𝑝 𝑞) 𝑟) ∈ 𝐵 ∧ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠))) ↔ (((𝑝 𝑞) 𝑟) ∈ 𝐵 ∧ ∃𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠))))
3633, 34, 353bitr3g 312 . . . . . . . . . 10 (𝑦 = ((𝑝 𝑞) 𝑟) → (((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ ∃𝑠𝐴 (𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠)))) ↔ (((𝑝 𝑞) 𝑟) ∈ 𝐵 ∧ ∃𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠)))))
3716, 36ceqsexv 3523 . . . . . . . . 9 (∃𝑦(𝑦 = ((𝑝 𝑞) 𝑟) ∧ ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞)) ∧ ∃𝑠𝐴 (𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))))) ↔ (((𝑝 𝑞) 𝑟) ∈ 𝐵 ∧ ∃𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠))))
3815, 37bitri 274 . . . . . . . 8 (∃𝑦𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ (((𝑝 𝑞) 𝑟) ∈ 𝐵 ∧ ∃𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠))))
39 hllat 38839 . . . . . . . . . . 11 (𝐾 ∈ HL → 𝐾 ∈ Lat)
4039ad3antrrr 728 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ (𝑝𝐴𝑞𝐴)) ∧ 𝑟𝐴) → 𝐾 ∈ Lat)
41 simplll 773 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ (𝑝𝐴𝑞𝐴)) ∧ 𝑟𝐴) → 𝐾 ∈ HL)
42 simplrl 775 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ (𝑝𝐴𝑞𝐴)) ∧ 𝑟𝐴) → 𝑝𝐴)
43 simplrr 776 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ (𝑝𝐴𝑞𝐴)) ∧ 𝑟𝐴) → 𝑞𝐴)
441, 3, 4hlatjcl 38843 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ 𝑝𝐴𝑞𝐴) → (𝑝 𝑞) ∈ 𝐵)
4541, 42, 43, 44syl3anc 1368 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ (𝑝𝐴𝑞𝐴)) ∧ 𝑟𝐴) → (𝑝 𝑞) ∈ 𝐵)
461, 4atbase 38765 . . . . . . . . . . 11 (𝑟𝐴𝑟𝐵)
4746adantl 480 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ (𝑝𝐴𝑞𝐴)) ∧ 𝑟𝐴) → 𝑟𝐵)
481, 3latjcl 18436 . . . . . . . . . 10 ((𝐾 ∈ Lat ∧ (𝑝 𝑞) ∈ 𝐵𝑟𝐵) → ((𝑝 𝑞) 𝑟) ∈ 𝐵)
4940, 45, 47, 48syl3anc 1368 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ (𝑝𝐴𝑞𝐴)) ∧ 𝑟𝐴) → ((𝑝 𝑞) 𝑟) ∈ 𝐵)
5049biantrurd 531 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ (𝑝𝐴𝑞𝐴)) ∧ 𝑟𝐴) → (∃𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠)) ↔ (((𝑝 𝑞) 𝑟) ∈ 𝐵 ∧ ∃𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠)))))
5138, 50bitr4id 289 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ (𝑝𝐴𝑞𝐴)) ∧ 𝑟𝐴) → (∃𝑦𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠))))
5251rexbidva 3172 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ (𝑝𝐴𝑞𝐴)) → (∃𝑟𝐴𝑦𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑟𝐴𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠))))
53522rexbidva 3213 . . . . 5 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (∃𝑝𝐴𝑞𝐴𝑟𝐴𝑦𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠))))
54 rexcom4 3281 . . . . . . . . 9 (∃𝑟𝐴𝑦𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑦𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
5554rexbii 3090 . . . . . . . 8 (∃𝑞𝐴𝑟𝐴𝑦𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑞𝐴𝑦𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
56 rexcom4 3281 . . . . . . . 8 (∃𝑞𝐴𝑦𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑦𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
5755, 56bitri 274 . . . . . . 7 (∃𝑞𝐴𝑟𝐴𝑦𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑦𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
5857rexbii 3090 . . . . . 6 (∃𝑝𝐴𝑞𝐴𝑟𝐴𝑦𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑝𝐴𝑦𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
59 rexcom4 3281 . . . . . 6 (∃𝑝𝐴𝑦𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑦𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
6058, 59bitri 274 . . . . 5 (∃𝑝𝐴𝑞𝐴𝑟𝐴𝑦𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑦𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
6153, 60bitr3di 285 . . . 4 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (∃𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠)) ↔ ∃𝑦𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟)))))
62 rexcom 3283 . . . . . . . . . . 11 (∃𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑠𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
6362rexbii 3090 . . . . . . . . . 10 (∃𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑞𝐴𝑠𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
64 rexcom 3283 . . . . . . . . . 10 (∃𝑞𝐴𝑠𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑠𝐴𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
6563, 64bitri 274 . . . . . . . . 9 (∃𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑠𝐴𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
6665rexbii 3090 . . . . . . . 8 (∃𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑝𝐴𝑠𝐴𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
67 rexcom 3283 . . . . . . . 8 (∃𝑝𝐴𝑠𝐴𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑠𝐴𝑝𝐴𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
6866, 67bitri 274 . . . . . . 7 (∃𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑠𝐴𝑝𝐴𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
691, 2, 3, 4, 5islpln2 39013 . . . . . . . . . . 11 (𝐾 ∈ HL → (𝑦 ∈ (LPlanes‘𝐾) ↔ (𝑦𝐵 ∧ ∃𝑝𝐴𝑞𝐴𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟)))))
7069adantr 479 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (𝑦 ∈ (LPlanes‘𝐾) ↔ (𝑦𝐵 ∧ ∃𝑝𝐴𝑞𝐴𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟)))))
7170anbi1d 629 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑋𝐵) → ((𝑦 ∈ (LPlanes‘𝐾) ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ↔ ((𝑦𝐵 ∧ ∃𝑝𝐴𝑞𝐴𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠)))))
72 r19.42v 3186 . . . . . . . . . 10 (∃𝑝𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ ∃𝑞𝐴𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ ∃𝑝𝐴𝑞𝐴𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
73 r19.42v 3186 . . . . . . . . . . . . 13 (∃𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ ∃𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
7473rexbii 3090 . . . . . . . . . . . 12 (∃𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑞𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ ∃𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
75 r19.42v 3186 . . . . . . . . . . . 12 (∃𝑞𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ ∃𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ ∃𝑞𝐴𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
7674, 75bitri 274 . . . . . . . . . . 11 (∃𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ ∃𝑞𝐴𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
7776rexbii 3090 . . . . . . . . . 10 (∃𝑝𝐴𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑝𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ ∃𝑞𝐴𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
78 an32 644 . . . . . . . . . 10 (((𝑦𝐵 ∧ ∃𝑝𝐴𝑞𝐴𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ↔ ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ ∃𝑝𝐴𝑞𝐴𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
7972, 77, 783bitr4ri 303 . . . . . . . . 9 (((𝑦𝐵 ∧ ∃𝑝𝐴𝑞𝐴𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ↔ ∃𝑝𝐴𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))))
8071, 79bitrdi 286 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑋𝐵) → ((𝑦 ∈ (LPlanes‘𝐾) ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ↔ ∃𝑝𝐴𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟)))))
8180rexbidv 3174 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (∃𝑠𝐴 (𝑦 ∈ (LPlanes‘𝐾) ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ↔ ∃𝑠𝐴𝑝𝐴𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟)))))
8268, 81bitr4id 289 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (∃𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑠𝐴 (𝑦 ∈ (LPlanes‘𝐾) ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠)))))
83 r19.42v 3186 . . . . . 6 (∃𝑠𝐴 (𝑦 ∈ (LPlanes‘𝐾) ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ↔ (𝑦 ∈ (LPlanes‘𝐾) ∧ ∃𝑠𝐴𝑠 𝑦𝑋 = (𝑦 𝑠))))
8482, 83bitrdi 286 . . . . 5 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (∃𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ (𝑦 ∈ (LPlanes‘𝐾) ∧ ∃𝑠𝐴𝑠 𝑦𝑋 = (𝑦 𝑠)))))
8584exbidv 1916 . . . 4 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (∃𝑦𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑦𝐵 ∧ (¬ 𝑠 𝑦𝑋 = (𝑦 𝑠))) ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑦 = ((𝑝 𝑞) 𝑟))) ↔ ∃𝑦(𝑦 ∈ (LPlanes‘𝐾) ∧ ∃𝑠𝐴𝑠 𝑦𝑋 = (𝑦 𝑠)))))
8661, 85bitrd 278 . . 3 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (∃𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠)) ↔ ∃𝑦(𝑦 ∈ (LPlanes‘𝐾) ∧ ∃𝑠𝐴𝑠 𝑦𝑋 = (𝑦 𝑠)))))
878, 86bitr4id 289 . 2 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (∃𝑦 ∈ (LPlanes‘𝐾)∃𝑠𝐴𝑠 𝑦𝑋 = (𝑦 𝑠)) ↔ ∃𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠))))
887, 87bitrd 278 1 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (𝑋𝑉 ↔ ∃𝑝𝐴𝑞𝐴𝑟𝐴𝑠𝐴 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ ¬ 𝑠 ((𝑝 𝑞) 𝑟)) ∧ 𝑋 = (((𝑝 𝑞) 𝑟) 𝑠))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  w3a 1084   = wceq 1533  wex 1773  wcel 2098  wne 2936  wrex 3066   class class class wbr 5150  cfv 6551  (class class class)co 7424  Basecbs 17185  lecple 17245  joincjn 18308  Latclat 18428  Atomscatm 38739  HLchlt 38826  LPlanesclpl 38969  LVolsclvol 38970
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2698  ax-rep 5287  ax-sep 5301  ax-nul 5308  ax-pow 5367  ax-pr 5431  ax-un 7744
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2937  df-ral 3058  df-rex 3067  df-rmo 3372  df-reu 3373  df-rab 3429  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4325  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4911  df-iun 5000  df-br 5151  df-opab 5213  df-mpt 5234  df-id 5578  df-xp 5686  df-rel 5687  df-cnv 5688  df-co 5689  df-dm 5690  df-rn 5691  df-res 5692  df-ima 5693  df-iota 6503  df-fun 6553  df-fn 6554  df-f 6555  df-f1 6556  df-fo 6557  df-f1o 6558  df-fv 6559  df-riota 7380  df-ov 7427  df-oprab 7428  df-proset 18292  df-poset 18310  df-plt 18327  df-lub 18343  df-glb 18344  df-join 18345  df-meet 18346  df-p0 18422  df-lat 18429  df-clat 18496  df-oposet 38652  df-ol 38654  df-oml 38655  df-covers 38742  df-ats 38743  df-atl 38774  df-cvlat 38798  df-hlat 38827  df-llines 38975  df-lplanes 38976  df-lvols 38977
This theorem is referenced by:  islvol2  39057  lvoli2  39058
  Copyright terms: Public domain W3C validator