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

Theorem axtgsegcon 27715
Description: Axiom of segment construction, Axiom A4 of [Schwabhauser] p. 11. As discussed in Axiom 4 of [Tarski1999] p. 178, "The intuitive content [is that] given any line segment 𝐴𝐡, one can construct a line segment congruent to it, starting at any point π‘Œ and going in the direction of any ray containing π‘Œ. The ray is determined by the point π‘Œ and a second point 𝑋, the endpoint of the ray. The other endpoint of the line segment to be constructed is just the point 𝑧 whose existence is asserted." (Contributed by Thierry Arnoux, 15-Mar-2019.)
Hypotheses
Ref Expression
axtrkg.p 𝑃 = (Baseβ€˜πΊ)
axtrkg.d βˆ’ = (distβ€˜πΊ)
axtrkg.i 𝐼 = (Itvβ€˜πΊ)
axtrkg.g (πœ‘ β†’ 𝐺 ∈ TarskiG)
axtgsegcon.1 (πœ‘ β†’ 𝑋 ∈ 𝑃)
axtgsegcon.2 (πœ‘ β†’ π‘Œ ∈ 𝑃)
axtgsegcon.3 (πœ‘ β†’ 𝐴 ∈ 𝑃)
axtgsegcon.4 (πœ‘ β†’ 𝐡 ∈ 𝑃)
Assertion
Ref Expression
axtgsegcon (πœ‘ β†’ βˆƒπ‘§ ∈ 𝑃 (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (𝐴 βˆ’ 𝐡)))
Distinct variable groups:   𝑧,𝐴   𝑧,𝐡   𝑧,𝐼   𝑧,𝑃   𝑧,𝑋   𝑧,π‘Œ   𝑧, βˆ’
Allowed substitution hints:   πœ‘(𝑧)   𝐺(𝑧)

Proof of Theorem axtgsegcon
Dummy variables 𝑓 𝑖 𝑝 π‘₯ 𝑦 π‘Ž 𝑏 𝑐 𝑣 𝑒 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-trkg 27704 . . . . . 6 TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})}))
2 inss2 4230 . . . . . . 7 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})})) βŠ† (TarskiGCB ∩ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})})
3 inss1 4229 . . . . . . 7 (TarskiGCB ∩ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})}) βŠ† TarskiGCB
42, 3sstri 3992 . . . . . 6 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})})) βŠ† TarskiGCB
51, 4eqsstri 4017 . . . . 5 TarskiG βŠ† TarskiGCB
6 axtrkg.g . . . . 5 (πœ‘ β†’ 𝐺 ∈ TarskiG)
75, 6sselid 3981 . . . 4 (πœ‘ β†’ 𝐺 ∈ TarskiGCB)
8 axtrkg.p . . . . . . 7 𝑃 = (Baseβ€˜πΊ)
9 axtrkg.d . . . . . . 7 βˆ’ = (distβ€˜πΊ)
10 axtrkg.i . . . . . . 7 𝐼 = (Itvβ€˜πΊ)
118, 9, 10istrkgcb 27707 . . . . . 6 (𝐺 ∈ TarskiGCB ↔ (𝐺 ∈ V ∧ (βˆ€π‘₯ ∈ 𝑃 βˆ€π‘¦ ∈ 𝑃 βˆ€π‘§ ∈ 𝑃 βˆ€π‘’ ∈ 𝑃 βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆ€π‘£ ∈ 𝑃 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐼𝑧) ∧ 𝑏 ∈ (π‘ŽπΌπ‘)) ∧ (((π‘₯ βˆ’ 𝑦) = (π‘Ž βˆ’ 𝑏) ∧ (𝑦 βˆ’ 𝑧) = (𝑏 βˆ’ 𝑐)) ∧ ((π‘₯ βˆ’ 𝑒) = (π‘Ž βˆ’ 𝑣) ∧ (𝑦 βˆ’ 𝑒) = (𝑏 βˆ’ 𝑣)))) β†’ (𝑧 βˆ’ 𝑒) = (𝑐 βˆ’ 𝑣)) ∧ βˆ€π‘₯ ∈ 𝑃 βˆ€π‘¦ ∈ 𝑃 βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (𝑦 ∈ (π‘₯𝐼𝑧) ∧ (𝑦 βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)))))
1211simprbi 498 . . . . 5 (𝐺 ∈ TarskiGCB β†’ (βˆ€π‘₯ ∈ 𝑃 βˆ€π‘¦ ∈ 𝑃 βˆ€π‘§ ∈ 𝑃 βˆ€π‘’ ∈ 𝑃 βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆ€π‘£ ∈ 𝑃 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐼𝑧) ∧ 𝑏 ∈ (π‘ŽπΌπ‘)) ∧ (((π‘₯ βˆ’ 𝑦) = (π‘Ž βˆ’ 𝑏) ∧ (𝑦 βˆ’ 𝑧) = (𝑏 βˆ’ 𝑐)) ∧ ((π‘₯ βˆ’ 𝑒) = (π‘Ž βˆ’ 𝑣) ∧ (𝑦 βˆ’ 𝑒) = (𝑏 βˆ’ 𝑣)))) β†’ (𝑧 βˆ’ 𝑒) = (𝑐 βˆ’ 𝑣)) ∧ βˆ€π‘₯ ∈ 𝑃 βˆ€π‘¦ ∈ 𝑃 βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (𝑦 ∈ (π‘₯𝐼𝑧) ∧ (𝑦 βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏))))
1312simprd 497 . . . 4 (𝐺 ∈ TarskiGCB β†’ βˆ€π‘₯ ∈ 𝑃 βˆ€π‘¦ ∈ 𝑃 βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (𝑦 ∈ (π‘₯𝐼𝑧) ∧ (𝑦 βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)))
147, 13syl 17 . . 3 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑃 βˆ€π‘¦ ∈ 𝑃 βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (𝑦 ∈ (π‘₯𝐼𝑧) ∧ (𝑦 βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)))
15 axtgsegcon.1 . . . 4 (πœ‘ β†’ 𝑋 ∈ 𝑃)
16 axtgsegcon.2 . . . 4 (πœ‘ β†’ π‘Œ ∈ 𝑃)
17 oveq1 7416 . . . . . . . . 9 (π‘₯ = 𝑋 β†’ (π‘₯𝐼𝑧) = (𝑋𝐼𝑧))
1817eleq2d 2820 . . . . . . . 8 (π‘₯ = 𝑋 β†’ (𝑦 ∈ (π‘₯𝐼𝑧) ↔ 𝑦 ∈ (𝑋𝐼𝑧)))
1918anbi1d 631 . . . . . . 7 (π‘₯ = 𝑋 β†’ ((𝑦 ∈ (π‘₯𝐼𝑧) ∧ (𝑦 βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)) ↔ (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏))))
2019rexbidv 3179 . . . . . 6 (π‘₯ = 𝑋 β†’ (βˆƒπ‘§ ∈ 𝑃 (𝑦 ∈ (π‘₯𝐼𝑧) ∧ (𝑦 βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)) ↔ βˆƒπ‘§ ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏))))
21202ralbidv 3219 . . . . 5 (π‘₯ = 𝑋 β†’ (βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (𝑦 ∈ (π‘₯𝐼𝑧) ∧ (𝑦 βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)) ↔ βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏))))
22 eleq1 2822 . . . . . . . 8 (𝑦 = π‘Œ β†’ (𝑦 ∈ (𝑋𝐼𝑧) ↔ π‘Œ ∈ (𝑋𝐼𝑧)))
23 oveq1 7416 . . . . . . . . 9 (𝑦 = π‘Œ β†’ (𝑦 βˆ’ 𝑧) = (π‘Œ βˆ’ 𝑧))
2423eqeq1d 2735 . . . . . . . 8 (𝑦 = π‘Œ β†’ ((𝑦 βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏) ↔ (π‘Œ βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)))
2522, 24anbi12d 632 . . . . . . 7 (𝑦 = π‘Œ β†’ ((𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)) ↔ (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏))))
2625rexbidv 3179 . . . . . 6 (𝑦 = π‘Œ β†’ (βˆƒπ‘§ ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)) ↔ βˆƒπ‘§ ∈ 𝑃 (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏))))
27262ralbidv 3219 . . . . 5 (𝑦 = π‘Œ β†’ (βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)) ↔ βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏))))
2821, 27rspc2v 3623 . . . 4 ((𝑋 ∈ 𝑃 ∧ π‘Œ ∈ 𝑃) β†’ (βˆ€π‘₯ ∈ 𝑃 βˆ€π‘¦ ∈ 𝑃 βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (𝑦 ∈ (π‘₯𝐼𝑧) ∧ (𝑦 βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)) β†’ βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏))))
2915, 16, 28syl2anc 585 . . 3 (πœ‘ β†’ (βˆ€π‘₯ ∈ 𝑃 βˆ€π‘¦ ∈ 𝑃 βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (𝑦 ∈ (π‘₯𝐼𝑧) ∧ (𝑦 βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)) β†’ βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏))))
3014, 29mpd 15 . 2 (πœ‘ β†’ βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)))
31 axtgsegcon.3 . . 3 (πœ‘ β†’ 𝐴 ∈ 𝑃)
32 axtgsegcon.4 . . 3 (πœ‘ β†’ 𝐡 ∈ 𝑃)
33 oveq1 7416 . . . . . . 7 (π‘Ž = 𝐴 β†’ (π‘Ž βˆ’ 𝑏) = (𝐴 βˆ’ 𝑏))
3433eqeq2d 2744 . . . . . 6 (π‘Ž = 𝐴 β†’ ((π‘Œ βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏) ↔ (π‘Œ βˆ’ 𝑧) = (𝐴 βˆ’ 𝑏)))
3534anbi2d 630 . . . . 5 (π‘Ž = 𝐴 β†’ ((π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)) ↔ (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (𝐴 βˆ’ 𝑏))))
3635rexbidv 3179 . . . 4 (π‘Ž = 𝐴 β†’ (βˆƒπ‘§ ∈ 𝑃 (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)) ↔ βˆƒπ‘§ ∈ 𝑃 (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (𝐴 βˆ’ 𝑏))))
37 oveq2 7417 . . . . . . 7 (𝑏 = 𝐡 β†’ (𝐴 βˆ’ 𝑏) = (𝐴 βˆ’ 𝐡))
3837eqeq2d 2744 . . . . . 6 (𝑏 = 𝐡 β†’ ((π‘Œ βˆ’ 𝑧) = (𝐴 βˆ’ 𝑏) ↔ (π‘Œ βˆ’ 𝑧) = (𝐴 βˆ’ 𝐡)))
3938anbi2d 630 . . . . 5 (𝑏 = 𝐡 β†’ ((π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (𝐴 βˆ’ 𝑏)) ↔ (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (𝐴 βˆ’ 𝐡))))
4039rexbidv 3179 . . . 4 (𝑏 = 𝐡 β†’ (βˆƒπ‘§ ∈ 𝑃 (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (𝐴 βˆ’ 𝑏)) ↔ βˆƒπ‘§ ∈ 𝑃 (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (𝐴 βˆ’ 𝐡))))
4136, 40rspc2v 3623 . . 3 ((𝐴 ∈ 𝑃 ∧ 𝐡 ∈ 𝑃) β†’ (βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)) β†’ βˆƒπ‘§ ∈ 𝑃 (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (𝐴 βˆ’ 𝐡))))
4231, 32, 41syl2anc 585 . 2 (πœ‘ β†’ (βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)) β†’ βˆƒπ‘§ ∈ 𝑃 (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (𝐴 βˆ’ 𝐡))))
4330, 42mpd 15 1 (πœ‘ β†’ βˆƒπ‘§ ∈ 𝑃 (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (𝐴 βˆ’ 𝐡)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 397   ∨ w3o 1087   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  {cab 2710   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071  {crab 3433  Vcvv 3475  [wsbc 3778   βˆ– cdif 3946   ∩ cin 3948  {csn 4629  β€˜cfv 6544  (class class class)co 7409   ∈ cmpo 7411  Basecbs 17144  distcds 17206  TarskiGcstrkg 27678  TarskiGCcstrkgc 27679  TarskiGBcstrkgb 27680  TarskiGCBcstrkgcb 27681  Itvcitv 27684  LineGclng 27685
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-nul 5307
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-trkgcb 27701  df-trkg 27704
This theorem is referenced by:  tgcgrtriv  27735  tgbtwntriv2  27738  tgbtwnouttr2  27746  tgbtwndiff  27757  tgifscgr  27759  tgcgrxfr  27769  lnext  27818  tgbtwnconn1lem3  27825  tgbtwnconn1  27826  legtrid  27842  hlcgrex  27867  mirreu3  27905  miriso  27921  midexlem  27943  footexALT  27969  footex  27972  opphllem  27986  flatcgra  28075  dfcgra2  28081  f1otrg  28122
  Copyright terms: Public domain W3C validator