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

Theorem islpln5 36779
Description: The predicate "is a lattice plane" in terms of atoms. (Contributed by NM, 24-Jun-2012.)
Hypotheses
Ref Expression
islpln5.b 𝐵 = (Base‘𝐾)
islpln5.l = (le‘𝐾)
islpln5.j = (join‘𝐾)
islpln5.a 𝐴 = (Atoms‘𝐾)
islpln5.p 𝑃 = (LPlanes‘𝐾)
Assertion
Ref Expression
islpln5 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (𝑋𝑃 ↔ ∃𝑝𝐴𝑞𝐴𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑋 = ((𝑝 𝑞) 𝑟))))
Distinct variable groups:   𝑞,𝑝,𝑟,𝐴   𝐵,𝑝,𝑞,𝑟   ,𝑝,𝑞,𝑟   𝐾,𝑝,𝑞,𝑟   ,𝑝,𝑞,𝑟   𝑋,𝑝,𝑞,𝑟
Allowed substitution hints:   𝑃(𝑟,𝑞,𝑝)

Proof of Theorem islpln5
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 islpln5.b . . 3 𝐵 = (Base‘𝐾)
2 islpln5.l . . 3 = (le‘𝐾)
3 islpln5.j . . 3 = (join‘𝐾)
4 islpln5.a . . 3 𝐴 = (Atoms‘𝐾)
5 eqid 2824 . . 3 (LLines‘𝐾) = (LLines‘𝐾)
6 islpln5.p . . 3 𝑃 = (LPlanes‘𝐾)
71, 2, 3, 4, 5, 6islpln3 36777 . 2 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (𝑋𝑃 ↔ ∃𝑦 ∈ (LLines‘𝐾)∃𝑟𝐴𝑟 𝑦𝑋 = (𝑦 𝑟))))
8 simpll 766 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ (𝑝𝐴𝑞𝐴)) → 𝐾 ∈ HL)
9 simprl 770 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ (𝑝𝐴𝑞𝐴)) → 𝑝𝐴)
10 simprr 772 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ (𝑝𝐴𝑞𝐴)) → 𝑞𝐴)
111, 3, 4hlatjcl 36611 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑝𝐴𝑞𝐴) → (𝑝 𝑞) ∈ 𝐵)
128, 9, 10, 11syl3anc 1368 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ (𝑝𝐴𝑞𝐴)) → (𝑝 𝑞) ∈ 𝐵)
1312biantrurd 536 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ (𝑝𝐴𝑞𝐴)) → (∃𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑋 = ((𝑝 𝑞) 𝑟)) ↔ ((𝑝 𝑞) ∈ 𝐵 ∧ ∃𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑋 = ((𝑝 𝑞) 𝑟)))))
14 r19.41v 3338 . . . . . . . . . 10 (∃𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞))) ↔ (∃𝑟𝐴 (𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞))))
15 an13 646 . . . . . . . . . 10 ((∃𝑟𝐴 (𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞))) ↔ (𝑦 = (𝑝 𝑞) ∧ (𝑝𝑞 ∧ ∃𝑟𝐴 (𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))))))
1614, 15bitri 278 . . . . . . . . 9 (∃𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞))) ↔ (𝑦 = (𝑝 𝑞) ∧ (𝑝𝑞 ∧ ∃𝑟𝐴 (𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))))))
1716exbii 1849 . . . . . . . 8 (∃𝑦𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞))) ↔ ∃𝑦(𝑦 = (𝑝 𝑞) ∧ (𝑝𝑞 ∧ ∃𝑟𝐴 (𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))))))
18 ovex 7182 . . . . . . . . 9 (𝑝 𝑞) ∈ V
19 an12 644 . . . . . . . . . . . 12 ((𝑝𝑞 ∧ (𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟)))) ↔ (𝑦𝐵 ∧ (𝑝𝑞 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟)))))
20 eleq1 2903 . . . . . . . . . . . . 13 (𝑦 = (𝑝 𝑞) → (𝑦𝐵 ↔ (𝑝 𝑞) ∈ 𝐵))
21 breq2 5056 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝑝 𝑞) → (𝑟 𝑦𝑟 (𝑝 𝑞)))
2221notbid 321 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑝 𝑞) → (¬ 𝑟 𝑦 ↔ ¬ 𝑟 (𝑝 𝑞)))
23 oveq1 7156 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝑝 𝑞) → (𝑦 𝑟) = ((𝑝 𝑞) 𝑟))
2423eqeq2d 2835 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑝 𝑞) → (𝑋 = (𝑦 𝑟) ↔ 𝑋 = ((𝑝 𝑞) 𝑟)))
2522, 24anbi12d 633 . . . . . . . . . . . . . . 15 (𝑦 = (𝑝 𝑞) → ((¬ 𝑟 𝑦𝑋 = (𝑦 𝑟)) ↔ (¬ 𝑟 (𝑝 𝑞) ∧ 𝑋 = ((𝑝 𝑞) 𝑟))))
2625anbi2d 631 . . . . . . . . . . . . . 14 (𝑦 = (𝑝 𝑞) → ((𝑝𝑞 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ↔ (𝑝𝑞 ∧ (¬ 𝑟 (𝑝 𝑞) ∧ 𝑋 = ((𝑝 𝑞) 𝑟)))))
27 3anass 1092 . . . . . . . . . . . . . 14 ((𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑋 = ((𝑝 𝑞) 𝑟)) ↔ (𝑝𝑞 ∧ (¬ 𝑟 (𝑝 𝑞) ∧ 𝑋 = ((𝑝 𝑞) 𝑟))))
2826, 27syl6bbr 292 . . . . . . . . . . . . 13 (𝑦 = (𝑝 𝑞) → ((𝑝𝑞 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ↔ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑋 = ((𝑝 𝑞) 𝑟))))
2920, 28anbi12d 633 . . . . . . . . . . . 12 (𝑦 = (𝑝 𝑞) → ((𝑦𝐵 ∧ (𝑝𝑞 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟)))) ↔ ((𝑝 𝑞) ∈ 𝐵 ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑋 = ((𝑝 𝑞) 𝑟)))))
3019, 29syl5bb 286 . . . . . . . . . . 11 (𝑦 = (𝑝 𝑞) → ((𝑝𝑞 ∧ (𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟)))) ↔ ((𝑝 𝑞) ∈ 𝐵 ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑋 = ((𝑝 𝑞) 𝑟)))))
3130rexbidv 3289 . . . . . . . . . 10 (𝑦 = (𝑝 𝑞) → (∃𝑟𝐴 (𝑝𝑞 ∧ (𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟)))) ↔ ∃𝑟𝐴 ((𝑝 𝑞) ∈ 𝐵 ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑋 = ((𝑝 𝑞) 𝑟)))))
32 r19.42v 3341 . . . . . . . . . 10 (∃𝑟𝐴 (𝑝𝑞 ∧ (𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟)))) ↔ (𝑝𝑞 ∧ ∃𝑟𝐴 (𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟)))))
33 r19.42v 3341 . . . . . . . . . 10 (∃𝑟𝐴 ((𝑝 𝑞) ∈ 𝐵 ∧ (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑋 = ((𝑝 𝑞) 𝑟))) ↔ ((𝑝 𝑞) ∈ 𝐵 ∧ ∃𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑋 = ((𝑝 𝑞) 𝑟))))
3431, 32, 333bitr3g 316 . . . . . . . . 9 (𝑦 = (𝑝 𝑞) → ((𝑝𝑞 ∧ ∃𝑟𝐴 (𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟)))) ↔ ((𝑝 𝑞) ∈ 𝐵 ∧ ∃𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑋 = ((𝑝 𝑞) 𝑟)))))
3518, 34ceqsexv 3527 . . . . . . . 8 (∃𝑦(𝑦 = (𝑝 𝑞) ∧ (𝑝𝑞 ∧ ∃𝑟𝐴 (𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))))) ↔ ((𝑝 𝑞) ∈ 𝐵 ∧ ∃𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑋 = ((𝑝 𝑞) 𝑟))))
3617, 35bitri 278 . . . . . . 7 (∃𝑦𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞))) ↔ ((𝑝 𝑞) ∈ 𝐵 ∧ ∃𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑋 = ((𝑝 𝑞) 𝑟))))
3713, 36syl6rbbr 293 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ (𝑝𝐴𝑞𝐴)) → (∃𝑦𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞))) ↔ ∃𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑋 = ((𝑝 𝑞) 𝑟))))
38372rexbidva 3291 . . . . 5 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (∃𝑝𝐴𝑞𝐴𝑦𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞))) ↔ ∃𝑝𝐴𝑞𝐴𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑋 = ((𝑝 𝑞) 𝑟))))
39 rexcom4 3243 . . . . . . 7 (∃𝑞𝐴𝑦𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞))) ↔ ∃𝑦𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞))))
4039rexbii 3241 . . . . . 6 (∃𝑝𝐴𝑞𝐴𝑦𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞))) ↔ ∃𝑝𝐴𝑦𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞))))
41 rexcom4 3243 . . . . . 6 (∃𝑝𝐴𝑦𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞))) ↔ ∃𝑦𝑝𝐴𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞))))
4240, 41bitri 278 . . . . 5 (∃𝑝𝐴𝑞𝐴𝑦𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞))) ↔ ∃𝑦𝑝𝐴𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞))))
4338, 42bitr3di 289 . . . 4 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (∃𝑝𝐴𝑞𝐴𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑋 = ((𝑝 𝑞) 𝑟)) ↔ ∃𝑦𝑝𝐴𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞)))))
441, 3, 4, 5islln2 36755 . . . . . . . . . . 11 (𝐾 ∈ HL → (𝑦 ∈ (LLines‘𝐾) ↔ (𝑦𝐵 ∧ ∃𝑝𝐴𝑞𝐴 (𝑝𝑞𝑦 = (𝑝 𝑞)))))
4544adantr 484 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (𝑦 ∈ (LLines‘𝐾) ↔ (𝑦𝐵 ∧ ∃𝑝𝐴𝑞𝐴 (𝑝𝑞𝑦 = (𝑝 𝑞)))))
4645anbi1d 632 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑋𝐵) → ((𝑦 ∈ (LLines‘𝐾) ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ↔ ((𝑦𝐵 ∧ ∃𝑝𝐴𝑞𝐴 (𝑝𝑞𝑦 = (𝑝 𝑞))) ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟)))))
47 r19.42v 3341 . . . . . . . . . 10 (∃𝑝𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ ∃𝑞𝐴 (𝑝𝑞𝑦 = (𝑝 𝑞))) ↔ ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ ∃𝑝𝐴𝑞𝐴 (𝑝𝑞𝑦 = (𝑝 𝑞))))
48 r19.42v 3341 . . . . . . . . . . 11 (∃𝑞𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞))) ↔ ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ ∃𝑞𝐴 (𝑝𝑞𝑦 = (𝑝 𝑞))))
4948rexbii 3241 . . . . . . . . . 10 (∃𝑝𝐴𝑞𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞))) ↔ ∃𝑝𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ ∃𝑞𝐴 (𝑝𝑞𝑦 = (𝑝 𝑞))))
50 an32 645 . . . . . . . . . 10 (((𝑦𝐵 ∧ ∃𝑝𝐴𝑞𝐴 (𝑝𝑞𝑦 = (𝑝 𝑞))) ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ↔ ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ ∃𝑝𝐴𝑞𝐴 (𝑝𝑞𝑦 = (𝑝 𝑞))))
5147, 49, 503bitr4ri 307 . . . . . . . . 9 (((𝑦𝐵 ∧ ∃𝑝𝐴𝑞𝐴 (𝑝𝑞𝑦 = (𝑝 𝑞))) ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ↔ ∃𝑝𝐴𝑞𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞))))
5246, 51syl6bb 290 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑋𝐵) → ((𝑦 ∈ (LLines‘𝐾) ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ↔ ∃𝑝𝐴𝑞𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞)))))
5352rexbidv 3289 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (∃𝑟𝐴 (𝑦 ∈ (LLines‘𝐾) ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ↔ ∃𝑟𝐴𝑝𝐴𝑞𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞)))))
54 rexcom 3346 . . . . . . . . 9 (∃𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞))) ↔ ∃𝑟𝐴𝑞𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞))))
5554rexbii 3241 . . . . . . . 8 (∃𝑝𝐴𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞))) ↔ ∃𝑝𝐴𝑟𝐴𝑞𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞))))
56 rexcom 3346 . . . . . . . 8 (∃𝑝𝐴𝑟𝐴𝑞𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞))) ↔ ∃𝑟𝐴𝑝𝐴𝑞𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞))))
5755, 56bitri 278 . . . . . . 7 (∃𝑝𝐴𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞))) ↔ ∃𝑟𝐴𝑝𝐴𝑞𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞))))
5853, 57syl6rbbr 293 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (∃𝑝𝐴𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞))) ↔ ∃𝑟𝐴 (𝑦 ∈ (LLines‘𝐾) ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟)))))
59 r19.42v 3341 . . . . . 6 (∃𝑟𝐴 (𝑦 ∈ (LLines‘𝐾) ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ↔ (𝑦 ∈ (LLines‘𝐾) ∧ ∃𝑟𝐴𝑟 𝑦𝑋 = (𝑦 𝑟))))
6058, 59syl6bb 290 . . . . 5 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (∃𝑝𝐴𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞))) ↔ (𝑦 ∈ (LLines‘𝐾) ∧ ∃𝑟𝐴𝑟 𝑦𝑋 = (𝑦 𝑟)))))
6160exbidv 1923 . . . 4 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (∃𝑦𝑝𝐴𝑞𝐴𝑟𝐴 ((𝑦𝐵 ∧ (¬ 𝑟 𝑦𝑋 = (𝑦 𝑟))) ∧ (𝑝𝑞𝑦 = (𝑝 𝑞))) ↔ ∃𝑦(𝑦 ∈ (LLines‘𝐾) ∧ ∃𝑟𝐴𝑟 𝑦𝑋 = (𝑦 𝑟)))))
6243, 61bitrd 282 . . 3 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (∃𝑝𝐴𝑞𝐴𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑋 = ((𝑝 𝑞) 𝑟)) ↔ ∃𝑦(𝑦 ∈ (LLines‘𝐾) ∧ ∃𝑟𝐴𝑟 𝑦𝑋 = (𝑦 𝑟)))))
63 df-rex 3139 . . 3 (∃𝑦 ∈ (LLines‘𝐾)∃𝑟𝐴𝑟 𝑦𝑋 = (𝑦 𝑟)) ↔ ∃𝑦(𝑦 ∈ (LLines‘𝐾) ∧ ∃𝑟𝐴𝑟 𝑦𝑋 = (𝑦 𝑟))))
6462, 63syl6rbbr 293 . 2 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (∃𝑦 ∈ (LLines‘𝐾)∃𝑟𝐴𝑟 𝑦𝑋 = (𝑦 𝑟)) ↔ ∃𝑝𝐴𝑞𝐴𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑋 = ((𝑝 𝑞) 𝑟))))
657, 64bitrd 282 1 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (𝑋𝑃 ↔ ∃𝑝𝐴𝑞𝐴𝑟𝐴 (𝑝𝑞 ∧ ¬ 𝑟 (𝑝 𝑞) ∧ 𝑋 = ((𝑝 𝑞) 𝑟))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wex 1781  wcel 2115  wne 3014  wrex 3134   class class class wbr 5052  cfv 6343  (class class class)co 7149  Basecbs 16483  lecple 16572  joincjn 17554  Atomscatm 36507  HLchlt 36594  LLinesclln 36735  LPlanesclpl 36736
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-ral 3138  df-rex 3139  df-reu 3140  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4825  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5447  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-riota 7107  df-ov 7152  df-oprab 7153  df-proset 17538  df-poset 17556  df-plt 17568  df-lub 17584  df-glb 17585  df-join 17586  df-meet 17587  df-p0 17649  df-lat 17656  df-clat 17718  df-oposet 36420  df-ol 36422  df-oml 36423  df-covers 36510  df-ats 36511  df-atl 36542  df-cvlat 36566  df-hlat 36595  df-llines 36742  df-lplanes 36743
This theorem is referenced by:  islpln2  36780  lplni2  36781
  Copyright terms: Public domain W3C validator