MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  legov Structured version   Visualization version   GIF version

Theorem legov 28101
Description: Value of the less-than relationship. Definition 5.4 of [Schwabhauser] p. 41. (Contributed by Thierry Arnoux, 21-Jun-2019.)
Hypotheses
Ref Expression
legval.p 𝑃 = (Baseβ€˜πΊ)
legval.d βˆ’ = (distβ€˜πΊ)
legval.i 𝐼 = (Itvβ€˜πΊ)
legval.l ≀ = (≀Gβ€˜πΊ)
legval.g (πœ‘ β†’ 𝐺 ∈ TarskiG)
legov.a (πœ‘ β†’ 𝐴 ∈ 𝑃)
legov.b (πœ‘ β†’ 𝐡 ∈ 𝑃)
legov.c (πœ‘ β†’ 𝐢 ∈ 𝑃)
legov.d (πœ‘ β†’ 𝐷 ∈ 𝑃)
Assertion
Ref Expression
legov (πœ‘ β†’ ((𝐴 βˆ’ 𝐡) ≀ (𝐢 βˆ’ 𝐷) ↔ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝐢𝐼𝐷) ∧ (𝐴 βˆ’ 𝐡) = (𝐢 βˆ’ 𝑧))))
Distinct variable groups:   𝑧, βˆ’   𝑧,𝐴   𝑧,𝐡   𝑧,𝐢   𝑧,𝐷   𝑧,𝐼   𝑧,𝑃   𝑧,𝐺   πœ‘,𝑧
Allowed substitution hint:   ≀ (𝑧)

Proof of Theorem legov
Dummy variables 𝑐 𝑑 𝑒 𝑓 π‘₯ 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 legval.p . . . . 5 𝑃 = (Baseβ€˜πΊ)
2 legval.d . . . . 5 βˆ’ = (distβ€˜πΊ)
3 legval.i . . . . 5 𝐼 = (Itvβ€˜πΊ)
4 legval.l . . . . 5 ≀ = (≀Gβ€˜πΊ)
5 legval.g . . . . 5 (πœ‘ β†’ 𝐺 ∈ TarskiG)
61, 2, 3, 4, 5legval 28100 . . . 4 (πœ‘ β†’ ≀ = {βŸ¨π‘’, π‘“βŸ© ∣ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 (𝑓 = (π‘₯ βˆ’ 𝑦) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (π‘₯𝐼𝑦) ∧ 𝑒 = (π‘₯ βˆ’ 𝑧)))})
76breqd 5160 . . 3 (πœ‘ β†’ ((𝐴 βˆ’ 𝐡) ≀ (𝐢 βˆ’ 𝐷) ↔ (𝐴 βˆ’ 𝐡){βŸ¨π‘’, π‘“βŸ© ∣ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 (𝑓 = (π‘₯ βˆ’ 𝑦) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (π‘₯𝐼𝑦) ∧ 𝑒 = (π‘₯ βˆ’ 𝑧)))} (𝐢 βˆ’ 𝐷)))
8 ovex 7446 . . . 4 (𝐴 βˆ’ 𝐡) ∈ V
9 ovex 7446 . . . 4 (𝐢 βˆ’ 𝐷) ∈ V
10 simpr 483 . . . . . . 7 ((𝑒 = (𝐴 βˆ’ 𝐡) ∧ 𝑓 = (𝐢 βˆ’ 𝐷)) β†’ 𝑓 = (𝐢 βˆ’ 𝐷))
1110eqeq1d 2732 . . . . . 6 ((𝑒 = (𝐴 βˆ’ 𝐡) ∧ 𝑓 = (𝐢 βˆ’ 𝐷)) β†’ (𝑓 = (π‘₯ βˆ’ 𝑦) ↔ (𝐢 βˆ’ 𝐷) = (π‘₯ βˆ’ 𝑦)))
12 simpl 481 . . . . . . . . 9 ((𝑒 = (𝐴 βˆ’ 𝐡) ∧ 𝑓 = (𝐢 βˆ’ 𝐷)) β†’ 𝑒 = (𝐴 βˆ’ 𝐡))
1312eqeq1d 2732 . . . . . . . 8 ((𝑒 = (𝐴 βˆ’ 𝐡) ∧ 𝑓 = (𝐢 βˆ’ 𝐷)) β†’ (𝑒 = (π‘₯ βˆ’ 𝑧) ↔ (𝐴 βˆ’ 𝐡) = (π‘₯ βˆ’ 𝑧)))
1413anbi2d 627 . . . . . . 7 ((𝑒 = (𝐴 βˆ’ 𝐡) ∧ 𝑓 = (𝐢 βˆ’ 𝐷)) β†’ ((𝑧 ∈ (π‘₯𝐼𝑦) ∧ 𝑒 = (π‘₯ βˆ’ 𝑧)) ↔ (𝑧 ∈ (π‘₯𝐼𝑦) ∧ (𝐴 βˆ’ 𝐡) = (π‘₯ βˆ’ 𝑧))))
1514rexbidv 3176 . . . . . 6 ((𝑒 = (𝐴 βˆ’ 𝐡) ∧ 𝑓 = (𝐢 βˆ’ 𝐷)) β†’ (βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (π‘₯𝐼𝑦) ∧ 𝑒 = (π‘₯ βˆ’ 𝑧)) ↔ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (π‘₯𝐼𝑦) ∧ (𝐴 βˆ’ 𝐡) = (π‘₯ βˆ’ 𝑧))))
1611, 15anbi12d 629 . . . . 5 ((𝑒 = (𝐴 βˆ’ 𝐡) ∧ 𝑓 = (𝐢 βˆ’ 𝐷)) β†’ ((𝑓 = (π‘₯ βˆ’ 𝑦) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (π‘₯𝐼𝑦) ∧ 𝑒 = (π‘₯ βˆ’ 𝑧))) ↔ ((𝐢 βˆ’ 𝐷) = (π‘₯ βˆ’ 𝑦) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (π‘₯𝐼𝑦) ∧ (𝐴 βˆ’ 𝐡) = (π‘₯ βˆ’ 𝑧)))))
17162rexbidv 3217 . . . 4 ((𝑒 = (𝐴 βˆ’ 𝐡) ∧ 𝑓 = (𝐢 βˆ’ 𝐷)) β†’ (βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 (𝑓 = (π‘₯ βˆ’ 𝑦) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (π‘₯𝐼𝑦) ∧ 𝑒 = (π‘₯ βˆ’ 𝑧))) ↔ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 ((𝐢 βˆ’ 𝐷) = (π‘₯ βˆ’ 𝑦) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (π‘₯𝐼𝑦) ∧ (𝐴 βˆ’ 𝐡) = (π‘₯ βˆ’ 𝑧)))))
18 eqid 2730 . . . 4 {βŸ¨π‘’, π‘“βŸ© ∣ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 (𝑓 = (π‘₯ βˆ’ 𝑦) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (π‘₯𝐼𝑦) ∧ 𝑒 = (π‘₯ βˆ’ 𝑧)))} = {βŸ¨π‘’, π‘“βŸ© ∣ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 (𝑓 = (π‘₯ βˆ’ 𝑦) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (π‘₯𝐼𝑦) ∧ 𝑒 = (π‘₯ βˆ’ 𝑧)))}
198, 9, 17, 18braba 5538 . . 3 ((𝐴 βˆ’ 𝐡){βŸ¨π‘’, π‘“βŸ© ∣ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 (𝑓 = (π‘₯ βˆ’ 𝑦) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (π‘₯𝐼𝑦) ∧ 𝑒 = (π‘₯ βˆ’ 𝑧)))} (𝐢 βˆ’ 𝐷) ↔ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 ((𝐢 βˆ’ 𝐷) = (π‘₯ βˆ’ 𝑦) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (π‘₯𝐼𝑦) ∧ (𝐴 βˆ’ 𝐡) = (π‘₯ βˆ’ 𝑧))))
207, 19bitrdi 286 . 2 (πœ‘ β†’ ((𝐴 βˆ’ 𝐡) ≀ (𝐢 βˆ’ 𝐷) ↔ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 ((𝐢 βˆ’ 𝐷) = (π‘₯ βˆ’ 𝑦) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (π‘₯𝐼𝑦) ∧ (𝐴 βˆ’ 𝐡) = (π‘₯ βˆ’ 𝑧)))))
21 anass 467 . . . . . . . 8 (((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑)) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ 𝑧))) ↔ (((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ 𝑧)))))
2221anbi1i 622 . . . . . . 7 ((((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑)) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ 𝑧))) ∧ π‘₯ ∈ 𝑃) ↔ ((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ 𝑧)))) ∧ π‘₯ ∈ 𝑃))
23 eqid 2730 . . . . . . . . . . 11 (cgrGβ€˜πΊ) = (cgrGβ€˜πΊ)
245ad5antr 730 . . . . . . . . . . . 12 ((((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑)) ∧ π‘₯ ∈ 𝑃) ∧ (π‘₯ ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯))) β†’ 𝐺 ∈ TarskiG)
2524adantr 479 . . . . . . . . . . 11 (((((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑)) ∧ π‘₯ ∈ 𝑃) ∧ (π‘₯ ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯))) ∧ (𝑧 ∈ 𝑃 ∧ βŸ¨β€œπ‘π‘‘π‘₯β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπΆπ·π‘§β€βŸ©)) β†’ 𝐺 ∈ TarskiG)
26 simp-5r 782 . . . . . . . . . . . 12 ((((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑)) ∧ π‘₯ ∈ 𝑃) ∧ (π‘₯ ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯))) β†’ 𝑐 ∈ 𝑃)
2726adantr 479 . . . . . . . . . . 11 (((((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑)) ∧ π‘₯ ∈ 𝑃) ∧ (π‘₯ ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯))) ∧ (𝑧 ∈ 𝑃 ∧ βŸ¨β€œπ‘π‘‘π‘₯β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπΆπ·π‘§β€βŸ©)) β†’ 𝑐 ∈ 𝑃)
28 simpllr 772 . . . . . . . . . . 11 (((((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑)) ∧ π‘₯ ∈ 𝑃) ∧ (π‘₯ ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯))) ∧ (𝑧 ∈ 𝑃 ∧ βŸ¨β€œπ‘π‘‘π‘₯β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπΆπ·π‘§β€βŸ©)) β†’ π‘₯ ∈ 𝑃)
29 simp-4r 780 . . . . . . . . . . . 12 ((((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑)) ∧ π‘₯ ∈ 𝑃) ∧ (π‘₯ ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯))) β†’ 𝑑 ∈ 𝑃)
3029adantr 479 . . . . . . . . . . 11 (((((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑)) ∧ π‘₯ ∈ 𝑃) ∧ (π‘₯ ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯))) ∧ (𝑧 ∈ 𝑃 ∧ βŸ¨β€œπ‘π‘‘π‘₯β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπΆπ·π‘§β€βŸ©)) β†’ 𝑑 ∈ 𝑃)
31 legov.c . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐢 ∈ 𝑃)
3231ad5antr 730 . . . . . . . . . . . 12 ((((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑)) ∧ π‘₯ ∈ 𝑃) ∧ (π‘₯ ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯))) β†’ 𝐢 ∈ 𝑃)
3332adantr 479 . . . . . . . . . . 11 (((((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑)) ∧ π‘₯ ∈ 𝑃) ∧ (π‘₯ ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯))) ∧ (𝑧 ∈ 𝑃 ∧ βŸ¨β€œπ‘π‘‘π‘₯β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπΆπ·π‘§β€βŸ©)) β†’ 𝐢 ∈ 𝑃)
34 simprl 767 . . . . . . . . . . 11 (((((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑)) ∧ π‘₯ ∈ 𝑃) ∧ (π‘₯ ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯))) ∧ (𝑧 ∈ 𝑃 ∧ βŸ¨β€œπ‘π‘‘π‘₯β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπΆπ·π‘§β€βŸ©)) β†’ 𝑧 ∈ 𝑃)
35 legov.d . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐷 ∈ 𝑃)
3635ad5antr 730 . . . . . . . . . . . 12 ((((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑)) ∧ π‘₯ ∈ 𝑃) ∧ (π‘₯ ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯))) β†’ 𝐷 ∈ 𝑃)
3736adantr 479 . . . . . . . . . . 11 (((((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑)) ∧ π‘₯ ∈ 𝑃) ∧ (π‘₯ ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯))) ∧ (𝑧 ∈ 𝑃 ∧ βŸ¨β€œπ‘π‘‘π‘₯β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπΆπ·π‘§β€βŸ©)) β†’ 𝐷 ∈ 𝑃)
38 simprr 769 . . . . . . . . . . . 12 (((((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑)) ∧ π‘₯ ∈ 𝑃) ∧ (π‘₯ ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯))) ∧ (𝑧 ∈ 𝑃 ∧ βŸ¨β€œπ‘π‘‘π‘₯β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπΆπ·π‘§β€βŸ©)) β†’ βŸ¨β€œπ‘π‘‘π‘₯β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπΆπ·π‘§β€βŸ©)
391, 2, 3, 23, 25, 27, 30, 28, 33, 37, 34, 38cgr3swap23 28040 . . . . . . . . . . 11 (((((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑)) ∧ π‘₯ ∈ 𝑃) ∧ (π‘₯ ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯))) ∧ (𝑧 ∈ 𝑃 ∧ βŸ¨β€œπ‘π‘‘π‘₯β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπΆπ·π‘§β€βŸ©)) β†’ βŸ¨β€œπ‘π‘₯π‘‘β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπΆπ‘§π·β€βŸ©)
40 simprl 767 . . . . . . . . . . . 12 ((((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑)) ∧ π‘₯ ∈ 𝑃) ∧ (π‘₯ ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯))) β†’ π‘₯ ∈ (𝑐𝐼𝑑))
4140adantr 479 . . . . . . . . . . 11 (((((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑)) ∧ π‘₯ ∈ 𝑃) ∧ (π‘₯ ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯))) ∧ (𝑧 ∈ 𝑃 ∧ βŸ¨β€œπ‘π‘‘π‘₯β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπΆπ·π‘§β€βŸ©)) β†’ π‘₯ ∈ (𝑐𝐼𝑑))
421, 2, 3, 23, 25, 27, 28, 30, 33, 34, 37, 39, 41tgbtwnxfr 28046 . . . . . . . . . 10 (((((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑)) ∧ π‘₯ ∈ 𝑃) ∧ (π‘₯ ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯))) ∧ (𝑧 ∈ 𝑃 ∧ βŸ¨β€œπ‘π‘‘π‘₯β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπΆπ·π‘§β€βŸ©)) β†’ 𝑧 ∈ (𝐢𝐼𝐷))
43 simplrr 774 . . . . . . . . . . 11 (((((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑)) ∧ π‘₯ ∈ 𝑃) ∧ (π‘₯ ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯))) ∧ (𝑧 ∈ 𝑃 ∧ βŸ¨β€œπ‘π‘‘π‘₯β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπΆπ·π‘§β€βŸ©)) β†’ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯))
441, 2, 3, 23, 25, 27, 28, 30, 33, 34, 37, 39cgr3simp1 28036 . . . . . . . . . . 11 (((((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑)) ∧ π‘₯ ∈ 𝑃) ∧ (π‘₯ ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯))) ∧ (𝑧 ∈ 𝑃 ∧ βŸ¨β€œπ‘π‘‘π‘₯β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπΆπ·π‘§β€βŸ©)) β†’ (𝑐 βˆ’ π‘₯) = (𝐢 βˆ’ 𝑧))
4543, 44eqtrd 2770 . . . . . . . . . 10 (((((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑)) ∧ π‘₯ ∈ 𝑃) ∧ (π‘₯ ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯))) ∧ (𝑧 ∈ 𝑃 ∧ βŸ¨β€œπ‘π‘‘π‘₯β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπΆπ·π‘§β€βŸ©)) β†’ (𝐴 βˆ’ 𝐡) = (𝐢 βˆ’ 𝑧))
4642, 45jca 510 . . . . . . . . 9 (((((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑)) ∧ π‘₯ ∈ 𝑃) ∧ (π‘₯ ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯))) ∧ (𝑧 ∈ 𝑃 ∧ βŸ¨β€œπ‘π‘‘π‘₯β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπΆπ·π‘§β€βŸ©)) β†’ (𝑧 ∈ (𝐢𝐼𝐷) ∧ (𝐴 βˆ’ 𝐡) = (𝐢 βˆ’ 𝑧)))
47 eqid 2730 . . . . . . . . . 10 (LineGβ€˜πΊ) = (LineGβ€˜πΊ)
48 simplr 765 . . . . . . . . . 10 ((((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑)) ∧ π‘₯ ∈ 𝑃) ∧ (π‘₯ ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯))) β†’ π‘₯ ∈ 𝑃)
491, 47, 3, 24, 26, 48, 29, 40btwncolg3 28073 . . . . . . . . . 10 ((((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑)) ∧ π‘₯ ∈ 𝑃) ∧ (π‘₯ ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯))) β†’ (𝑑 ∈ (𝑐(LineGβ€˜πΊ)π‘₯) ∨ 𝑐 = π‘₯))
50 simpllr 772 . . . . . . . . . . 11 ((((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑)) ∧ π‘₯ ∈ 𝑃) ∧ (π‘₯ ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯))) β†’ (𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑))
5150eqcomd 2736 . . . . . . . . . 10 ((((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑)) ∧ π‘₯ ∈ 𝑃) ∧ (π‘₯ ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯))) β†’ (𝑐 βˆ’ 𝑑) = (𝐢 βˆ’ 𝐷))
521, 47, 3, 24, 26, 29, 48, 23, 32, 36, 2, 49, 51lnext 28083 . . . . . . . . 9 ((((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑)) ∧ π‘₯ ∈ 𝑃) ∧ (π‘₯ ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯))) β†’ βˆƒπ‘§ ∈ 𝑃 βŸ¨β€œπ‘π‘‘π‘₯β€βŸ©(cgrGβ€˜πΊ)βŸ¨β€œπΆπ·π‘§β€βŸ©)
5346, 52reximddv 3169 . . . . . . . 8 ((((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑)) ∧ π‘₯ ∈ 𝑃) ∧ (π‘₯ ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯))) β†’ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝐢𝐼𝐷) ∧ (𝐴 βˆ’ 𝐡) = (𝐢 βˆ’ 𝑧)))
5453adantllr 715 . . . . . . 7 (((((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ (𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑)) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ 𝑧))) ∧ π‘₯ ∈ 𝑃) ∧ (π‘₯ ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯))) β†’ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝐢𝐼𝐷) ∧ (𝐴 βˆ’ 𝐡) = (𝐢 βˆ’ 𝑧)))
5522, 54sylanbr 580 . . . . . 6 ((((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ 𝑧)))) ∧ π‘₯ ∈ 𝑃) ∧ (π‘₯ ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯))) β†’ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝐢𝐼𝐷) ∧ (𝐴 βˆ’ 𝐡) = (𝐢 βˆ’ 𝑧)))
56 simprr 769 . . . . . . 7 ((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ 𝑧)))) β†’ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ 𝑧)))
57 eleq1w 2814 . . . . . . . . 9 (π‘₯ = 𝑧 β†’ (π‘₯ ∈ (𝑐𝐼𝑑) ↔ 𝑧 ∈ (𝑐𝐼𝑑)))
58 oveq2 7421 . . . . . . . . . 10 (π‘₯ = 𝑧 β†’ (𝑐 βˆ’ π‘₯) = (𝑐 βˆ’ 𝑧))
5958eqeq2d 2741 . . . . . . . . 9 (π‘₯ = 𝑧 β†’ ((𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯) ↔ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ 𝑧)))
6057, 59anbi12d 629 . . . . . . . 8 (π‘₯ = 𝑧 β†’ ((π‘₯ ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯)) ↔ (𝑧 ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ 𝑧))))
6160cbvrexvw 3233 . . . . . . 7 (βˆƒπ‘₯ ∈ 𝑃 (π‘₯ ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯)) ↔ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ 𝑧)))
6256, 61sylibr 233 . . . . . 6 ((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ 𝑧)))) β†’ βˆƒπ‘₯ ∈ 𝑃 (π‘₯ ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ π‘₯)))
6355, 62r19.29a 3160 . . . . 5 ((((πœ‘ ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ 𝑧)))) β†’ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝐢𝐼𝐷) ∧ (𝐴 βˆ’ 𝐡) = (𝐢 βˆ’ 𝑧)))
6463adantl3r 746 . . . 4 (((((πœ‘ ∧ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 ((𝐢 βˆ’ 𝐷) = (π‘₯ βˆ’ 𝑦) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (π‘₯𝐼𝑦) ∧ (𝐴 βˆ’ 𝐡) = (π‘₯ βˆ’ 𝑧)))) ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 ∈ 𝑃) ∧ ((𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ 𝑧)))) β†’ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝐢𝐼𝐷) ∧ (𝐴 βˆ’ 𝐡) = (𝐢 βˆ’ 𝑧)))
65 simpr 483 . . . . 5 ((πœ‘ ∧ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 ((𝐢 βˆ’ 𝐷) = (π‘₯ βˆ’ 𝑦) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (π‘₯𝐼𝑦) ∧ (𝐴 βˆ’ 𝐡) = (π‘₯ βˆ’ 𝑧)))) β†’ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 ((𝐢 βˆ’ 𝐷) = (π‘₯ βˆ’ 𝑦) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (π‘₯𝐼𝑦) ∧ (𝐴 βˆ’ 𝐡) = (π‘₯ βˆ’ 𝑧))))
66 oveq1 7420 . . . . . . . 8 (𝑐 = π‘₯ β†’ (𝑐 βˆ’ 𝑑) = (π‘₯ βˆ’ 𝑑))
6766eqeq2d 2741 . . . . . . 7 (𝑐 = π‘₯ β†’ ((𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑) ↔ (𝐢 βˆ’ 𝐷) = (π‘₯ βˆ’ 𝑑)))
68 oveq1 7420 . . . . . . . . . 10 (𝑐 = π‘₯ β†’ (𝑐𝐼𝑑) = (π‘₯𝐼𝑑))
6968eleq2d 2817 . . . . . . . . 9 (𝑐 = π‘₯ β†’ (𝑧 ∈ (𝑐𝐼𝑑) ↔ 𝑧 ∈ (π‘₯𝐼𝑑)))
70 oveq1 7420 . . . . . . . . . 10 (𝑐 = π‘₯ β†’ (𝑐 βˆ’ 𝑧) = (π‘₯ βˆ’ 𝑧))
7170eqeq2d 2741 . . . . . . . . 9 (𝑐 = π‘₯ β†’ ((𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ 𝑧) ↔ (𝐴 βˆ’ 𝐡) = (π‘₯ βˆ’ 𝑧)))
7269, 71anbi12d 629 . . . . . . . 8 (𝑐 = π‘₯ β†’ ((𝑧 ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ 𝑧)) ↔ (𝑧 ∈ (π‘₯𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (π‘₯ βˆ’ 𝑧))))
7372rexbidv 3176 . . . . . . 7 (𝑐 = π‘₯ β†’ (βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ 𝑧)) ↔ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (π‘₯𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (π‘₯ βˆ’ 𝑧))))
7467, 73anbi12d 629 . . . . . 6 (𝑐 = π‘₯ β†’ (((𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ 𝑧))) ↔ ((𝐢 βˆ’ 𝐷) = (π‘₯ βˆ’ 𝑑) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (π‘₯𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (π‘₯ βˆ’ 𝑧)))))
75 oveq2 7421 . . . . . . . 8 (𝑑 = 𝑦 β†’ (π‘₯ βˆ’ 𝑑) = (π‘₯ βˆ’ 𝑦))
7675eqeq2d 2741 . . . . . . 7 (𝑑 = 𝑦 β†’ ((𝐢 βˆ’ 𝐷) = (π‘₯ βˆ’ 𝑑) ↔ (𝐢 βˆ’ 𝐷) = (π‘₯ βˆ’ 𝑦)))
77 oveq2 7421 . . . . . . . . . 10 (𝑑 = 𝑦 β†’ (π‘₯𝐼𝑑) = (π‘₯𝐼𝑦))
7877eleq2d 2817 . . . . . . . . 9 (𝑑 = 𝑦 β†’ (𝑧 ∈ (π‘₯𝐼𝑑) ↔ 𝑧 ∈ (π‘₯𝐼𝑦)))
7978anbi1d 628 . . . . . . . 8 (𝑑 = 𝑦 β†’ ((𝑧 ∈ (π‘₯𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (π‘₯ βˆ’ 𝑧)) ↔ (𝑧 ∈ (π‘₯𝐼𝑦) ∧ (𝐴 βˆ’ 𝐡) = (π‘₯ βˆ’ 𝑧))))
8079rexbidv 3176 . . . . . . 7 (𝑑 = 𝑦 β†’ (βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (π‘₯𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (π‘₯ βˆ’ 𝑧)) ↔ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (π‘₯𝐼𝑦) ∧ (𝐴 βˆ’ 𝐡) = (π‘₯ βˆ’ 𝑧))))
8176, 80anbi12d 629 . . . . . 6 (𝑑 = 𝑦 β†’ (((𝐢 βˆ’ 𝐷) = (π‘₯ βˆ’ 𝑑) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (π‘₯𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (π‘₯ βˆ’ 𝑧))) ↔ ((𝐢 βˆ’ 𝐷) = (π‘₯ βˆ’ 𝑦) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (π‘₯𝐼𝑦) ∧ (𝐴 βˆ’ 𝐡) = (π‘₯ βˆ’ 𝑧)))))
8274, 81cbvrex2vw 3237 . . . . 5 (βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 ((𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ 𝑧))) ↔ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 ((𝐢 βˆ’ 𝐷) = (π‘₯ βˆ’ 𝑦) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (π‘₯𝐼𝑦) ∧ (𝐴 βˆ’ 𝐡) = (π‘₯ βˆ’ 𝑧))))
8365, 82sylibr 233 . . . 4 ((πœ‘ ∧ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 ((𝐢 βˆ’ 𝐷) = (π‘₯ βˆ’ 𝑦) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (π‘₯𝐼𝑦) ∧ (𝐴 βˆ’ 𝐡) = (π‘₯ βˆ’ 𝑧)))) β†’ βˆƒπ‘ ∈ 𝑃 βˆƒπ‘‘ ∈ 𝑃 ((𝐢 βˆ’ 𝐷) = (𝑐 βˆ’ 𝑑) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝑐𝐼𝑑) ∧ (𝐴 βˆ’ 𝐡) = (𝑐 βˆ’ 𝑧))))
8464, 83r19.29vva 3211 . . 3 ((πœ‘ ∧ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 ((𝐢 βˆ’ 𝐷) = (π‘₯ βˆ’ 𝑦) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (π‘₯𝐼𝑦) ∧ (𝐴 βˆ’ 𝐡) = (π‘₯ βˆ’ 𝑧)))) β†’ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝐢𝐼𝐷) ∧ (𝐴 βˆ’ 𝐡) = (𝐢 βˆ’ 𝑧)))
8531adantr 479 . . . 4 ((πœ‘ ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝐢𝐼𝐷) ∧ (𝐴 βˆ’ 𝐡) = (𝐢 βˆ’ 𝑧))) β†’ 𝐢 ∈ 𝑃)
8635adantr 479 . . . 4 ((πœ‘ ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝐢𝐼𝐷) ∧ (𝐴 βˆ’ 𝐡) = (𝐢 βˆ’ 𝑧))) β†’ 𝐷 ∈ 𝑃)
87 eqidd 2731 . . . 4 ((πœ‘ ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝐢𝐼𝐷) ∧ (𝐴 βˆ’ 𝐡) = (𝐢 βˆ’ 𝑧))) β†’ (𝐢 βˆ’ 𝐷) = (𝐢 βˆ’ 𝐷))
88 simpr 483 . . . 4 ((πœ‘ ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝐢𝐼𝐷) ∧ (𝐴 βˆ’ 𝐡) = (𝐢 βˆ’ 𝑧))) β†’ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝐢𝐼𝐷) ∧ (𝐴 βˆ’ 𝐡) = (𝐢 βˆ’ 𝑧)))
89 oveq1 7420 . . . . . . 7 (π‘₯ = 𝐢 β†’ (π‘₯ βˆ’ 𝑦) = (𝐢 βˆ’ 𝑦))
9089eqeq2d 2741 . . . . . 6 (π‘₯ = 𝐢 β†’ ((𝐢 βˆ’ 𝐷) = (π‘₯ βˆ’ 𝑦) ↔ (𝐢 βˆ’ 𝐷) = (𝐢 βˆ’ 𝑦)))
91 oveq1 7420 . . . . . . . . 9 (π‘₯ = 𝐢 β†’ (π‘₯𝐼𝑦) = (𝐢𝐼𝑦))
9291eleq2d 2817 . . . . . . . 8 (π‘₯ = 𝐢 β†’ (𝑧 ∈ (π‘₯𝐼𝑦) ↔ 𝑧 ∈ (𝐢𝐼𝑦)))
93 oveq1 7420 . . . . . . . . 9 (π‘₯ = 𝐢 β†’ (π‘₯ βˆ’ 𝑧) = (𝐢 βˆ’ 𝑧))
9493eqeq2d 2741 . . . . . . . 8 (π‘₯ = 𝐢 β†’ ((𝐴 βˆ’ 𝐡) = (π‘₯ βˆ’ 𝑧) ↔ (𝐴 βˆ’ 𝐡) = (𝐢 βˆ’ 𝑧)))
9592, 94anbi12d 629 . . . . . . 7 (π‘₯ = 𝐢 β†’ ((𝑧 ∈ (π‘₯𝐼𝑦) ∧ (𝐴 βˆ’ 𝐡) = (π‘₯ βˆ’ 𝑧)) ↔ (𝑧 ∈ (𝐢𝐼𝑦) ∧ (𝐴 βˆ’ 𝐡) = (𝐢 βˆ’ 𝑧))))
9695rexbidv 3176 . . . . . 6 (π‘₯ = 𝐢 β†’ (βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (π‘₯𝐼𝑦) ∧ (𝐴 βˆ’ 𝐡) = (π‘₯ βˆ’ 𝑧)) ↔ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝐢𝐼𝑦) ∧ (𝐴 βˆ’ 𝐡) = (𝐢 βˆ’ 𝑧))))
9790, 96anbi12d 629 . . . . 5 (π‘₯ = 𝐢 β†’ (((𝐢 βˆ’ 𝐷) = (π‘₯ βˆ’ 𝑦) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (π‘₯𝐼𝑦) ∧ (𝐴 βˆ’ 𝐡) = (π‘₯ βˆ’ 𝑧))) ↔ ((𝐢 βˆ’ 𝐷) = (𝐢 βˆ’ 𝑦) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝐢𝐼𝑦) ∧ (𝐴 βˆ’ 𝐡) = (𝐢 βˆ’ 𝑧)))))
98 oveq2 7421 . . . . . . 7 (𝑦 = 𝐷 β†’ (𝐢 βˆ’ 𝑦) = (𝐢 βˆ’ 𝐷))
9998eqeq2d 2741 . . . . . 6 (𝑦 = 𝐷 β†’ ((𝐢 βˆ’ 𝐷) = (𝐢 βˆ’ 𝑦) ↔ (𝐢 βˆ’ 𝐷) = (𝐢 βˆ’ 𝐷)))
100 oveq2 7421 . . . . . . . . 9 (𝑦 = 𝐷 β†’ (𝐢𝐼𝑦) = (𝐢𝐼𝐷))
101100eleq2d 2817 . . . . . . . 8 (𝑦 = 𝐷 β†’ (𝑧 ∈ (𝐢𝐼𝑦) ↔ 𝑧 ∈ (𝐢𝐼𝐷)))
102101anbi1d 628 . . . . . . 7 (𝑦 = 𝐷 β†’ ((𝑧 ∈ (𝐢𝐼𝑦) ∧ (𝐴 βˆ’ 𝐡) = (𝐢 βˆ’ 𝑧)) ↔ (𝑧 ∈ (𝐢𝐼𝐷) ∧ (𝐴 βˆ’ 𝐡) = (𝐢 βˆ’ 𝑧))))
103102rexbidv 3176 . . . . . 6 (𝑦 = 𝐷 β†’ (βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝐢𝐼𝑦) ∧ (𝐴 βˆ’ 𝐡) = (𝐢 βˆ’ 𝑧)) ↔ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝐢𝐼𝐷) ∧ (𝐴 βˆ’ 𝐡) = (𝐢 βˆ’ 𝑧))))
10499, 103anbi12d 629 . . . . 5 (𝑦 = 𝐷 β†’ (((𝐢 βˆ’ 𝐷) = (𝐢 βˆ’ 𝑦) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝐢𝐼𝑦) ∧ (𝐴 βˆ’ 𝐡) = (𝐢 βˆ’ 𝑧))) ↔ ((𝐢 βˆ’ 𝐷) = (𝐢 βˆ’ 𝐷) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝐢𝐼𝐷) ∧ (𝐴 βˆ’ 𝐡) = (𝐢 βˆ’ 𝑧)))))
10597, 104rspc2ev 3625 . . . 4 ((𝐢 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ ((𝐢 βˆ’ 𝐷) = (𝐢 βˆ’ 𝐷) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝐢𝐼𝐷) ∧ (𝐴 βˆ’ 𝐡) = (𝐢 βˆ’ 𝑧)))) β†’ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 ((𝐢 βˆ’ 𝐷) = (π‘₯ βˆ’ 𝑦) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (π‘₯𝐼𝑦) ∧ (𝐴 βˆ’ 𝐡) = (π‘₯ βˆ’ 𝑧))))
10685, 86, 87, 88, 105syl112anc 1372 . . 3 ((πœ‘ ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝐢𝐼𝐷) ∧ (𝐴 βˆ’ 𝐡) = (𝐢 βˆ’ 𝑧))) β†’ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 ((𝐢 βˆ’ 𝐷) = (π‘₯ βˆ’ 𝑦) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (π‘₯𝐼𝑦) ∧ (𝐴 βˆ’ 𝐡) = (π‘₯ βˆ’ 𝑧))))
10784, 106impbida 797 . 2 (πœ‘ β†’ (βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 ((𝐢 βˆ’ 𝐷) = (π‘₯ βˆ’ 𝑦) ∧ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (π‘₯𝐼𝑦) ∧ (𝐴 βˆ’ 𝐡) = (π‘₯ βˆ’ 𝑧))) ↔ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝐢𝐼𝐷) ∧ (𝐴 βˆ’ 𝐡) = (𝐢 βˆ’ 𝑧))))
10820, 107bitrd 278 1 (πœ‘ β†’ ((𝐴 βˆ’ 𝐡) ≀ (𝐢 βˆ’ 𝐷) ↔ βˆƒπ‘§ ∈ 𝑃 (𝑧 ∈ (𝐢𝐼𝐷) ∧ (𝐴 βˆ’ 𝐡) = (𝐢 βˆ’ 𝑧))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   = wceq 1539   ∈ wcel 2104  βˆƒwrex 3068   class class class wbr 5149  {copab 5211  β€˜cfv 6544  (class class class)co 7413  βŸ¨β€œcs3 14799  Basecbs 17150  distcds 17212  TarskiGcstrkg 27943  Itvcitv 27949  LineGclng 27950  cgrGccgrg 28026  β‰€Gcleg 28098
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7729  ax-cnex 11170  ax-resscn 11171  ax-1cn 11172  ax-icn 11173  ax-addcl 11174  ax-addrcl 11175  ax-mulcl 11176  ax-mulrcl 11177  ax-mulcom 11178  ax-addass 11179  ax-mulass 11180  ax-distr 11181  ax-i2m1 11182  ax-1ne0 11183  ax-1rid 11184  ax-rnegex 11185  ax-rrecex 11186  ax-cnre 11187  ax-pre-lttri 11188  ax-pre-lttrn 11189  ax-pre-ltadd 11190  ax-pre-mulgt0 11191
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7369  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7860  df-1st 7979  df-2nd 7980  df-frecs 8270  df-wrecs 8301  df-recs 8375  df-rdg 8414  df-1o 8470  df-oadd 8474  df-er 8707  df-pm 8827  df-en 8944  df-dom 8945  df-sdom 8946  df-fin 8947  df-dju 9900  df-card 9938  df-pnf 11256  df-mnf 11257  df-xr 11258  df-ltxr 11259  df-le 11260  df-sub 11452  df-neg 11453  df-nn 12219  df-2 12281  df-3 12282  df-n0 12479  df-xnn0 12551  df-z 12565  df-uz 12829  df-fz 13491  df-fzo 13634  df-hash 14297  df-word 14471  df-concat 14527  df-s1 14552  df-s2 14805  df-s3 14806  df-trkgc 27964  df-trkgb 27965  df-trkgcb 27966  df-trkg 27969  df-cgrg 28027  df-leg 28099
This theorem is referenced by:  legov2  28102  legid  28103  btwnleg  28104  legtrd  28105  legtri3  28106  legtrid  28107  leg0  28108  mideulem  28252  opphllem3  28265
  Copyright terms: Public domain W3C validator