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

Theorem axtgsegcon 27753
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 27742 . . . . . 6 TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})}))
2 inss2 4229 . . . . . . 7 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})})) βŠ† (TarskiGCB ∩ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})})
3 inss1 4228 . . . . . . 7 (TarskiGCB ∩ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})}) βŠ† TarskiGCB
42, 3sstri 3991 . . . . . 6 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})})) βŠ† TarskiGCB
51, 4eqsstri 4016 . . . . 5 TarskiG βŠ† TarskiGCB
6 axtrkg.g . . . . 5 (πœ‘ β†’ 𝐺 ∈ TarskiG)
75, 6sselid 3980 . . . 4 (πœ‘ β†’ 𝐺 ∈ TarskiGCB)
8 axtrkg.p . . . . . . 7 𝑃 = (Baseβ€˜πΊ)
9 axtrkg.d . . . . . . 7 βˆ’ = (distβ€˜πΊ)
10 axtrkg.i . . . . . . 7 𝐼 = (Itvβ€˜πΊ)
118, 9, 10istrkgcb 27745 . . . . . 6 (𝐺 ∈ TarskiGCB ↔ (𝐺 ∈ V ∧ (βˆ€π‘₯ ∈ 𝑃 βˆ€π‘¦ ∈ 𝑃 βˆ€π‘§ ∈ 𝑃 βˆ€π‘’ ∈ 𝑃 βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆ€π‘£ ∈ 𝑃 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐼𝑧) ∧ 𝑏 ∈ (π‘ŽπΌπ‘)) ∧ (((π‘₯ βˆ’ 𝑦) = (π‘Ž βˆ’ 𝑏) ∧ (𝑦 βˆ’ 𝑧) = (𝑏 βˆ’ 𝑐)) ∧ ((π‘₯ βˆ’ 𝑒) = (π‘Ž βˆ’ 𝑣) ∧ (𝑦 βˆ’ 𝑒) = (𝑏 βˆ’ 𝑣)))) β†’ (𝑧 βˆ’ 𝑒) = (𝑐 βˆ’ 𝑣)) ∧ βˆ€π‘₯ ∈ 𝑃 βˆ€π‘¦ ∈ 𝑃 βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (𝑦 ∈ (π‘₯𝐼𝑧) ∧ (𝑦 βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)))))
1211simprbi 497 . . . . 5 (𝐺 ∈ TarskiGCB β†’ (βˆ€π‘₯ ∈ 𝑃 βˆ€π‘¦ ∈ 𝑃 βˆ€π‘§ ∈ 𝑃 βˆ€π‘’ ∈ 𝑃 βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆ€π‘£ ∈ 𝑃 (((π‘₯ β‰  𝑦 ∧ 𝑦 ∈ (π‘₯𝐼𝑧) ∧ 𝑏 ∈ (π‘ŽπΌπ‘)) ∧ (((π‘₯ βˆ’ 𝑦) = (π‘Ž βˆ’ 𝑏) ∧ (𝑦 βˆ’ 𝑧) = (𝑏 βˆ’ 𝑐)) ∧ ((π‘₯ βˆ’ 𝑒) = (π‘Ž βˆ’ 𝑣) ∧ (𝑦 βˆ’ 𝑒) = (𝑏 βˆ’ 𝑣)))) β†’ (𝑧 βˆ’ 𝑒) = (𝑐 βˆ’ 𝑣)) ∧ βˆ€π‘₯ ∈ 𝑃 βˆ€π‘¦ ∈ 𝑃 βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (𝑦 ∈ (π‘₯𝐼𝑧) ∧ (𝑦 βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏))))
1312simprd 496 . . . 4 (𝐺 ∈ TarskiGCB β†’ βˆ€π‘₯ ∈ 𝑃 βˆ€π‘¦ ∈ 𝑃 βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (𝑦 ∈ (π‘₯𝐼𝑧) ∧ (𝑦 βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)))
147, 13syl 17 . . 3 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑃 βˆ€π‘¦ ∈ 𝑃 βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (𝑦 ∈ (π‘₯𝐼𝑧) ∧ (𝑦 βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)))
15 axtgsegcon.1 . . . 4 (πœ‘ β†’ 𝑋 ∈ 𝑃)
16 axtgsegcon.2 . . . 4 (πœ‘ β†’ π‘Œ ∈ 𝑃)
17 oveq1 7418 . . . . . . . . 9 (π‘₯ = 𝑋 β†’ (π‘₯𝐼𝑧) = (𝑋𝐼𝑧))
1817eleq2d 2819 . . . . . . . 8 (π‘₯ = 𝑋 β†’ (𝑦 ∈ (π‘₯𝐼𝑧) ↔ 𝑦 ∈ (𝑋𝐼𝑧)))
1918anbi1d 630 . . . . . . 7 (π‘₯ = 𝑋 β†’ ((𝑦 ∈ (π‘₯𝐼𝑧) ∧ (𝑦 βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)) ↔ (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏))))
2019rexbidv 3178 . . . . . 6 (π‘₯ = 𝑋 β†’ (βˆƒπ‘§ ∈ 𝑃 (𝑦 ∈ (π‘₯𝐼𝑧) ∧ (𝑦 βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)) ↔ βˆƒπ‘§ ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏))))
21202ralbidv 3218 . . . . 5 (π‘₯ = 𝑋 β†’ (βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (𝑦 ∈ (π‘₯𝐼𝑧) ∧ (𝑦 βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)) ↔ βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏))))
22 eleq1 2821 . . . . . . . 8 (𝑦 = π‘Œ β†’ (𝑦 ∈ (𝑋𝐼𝑧) ↔ π‘Œ ∈ (𝑋𝐼𝑧)))
23 oveq1 7418 . . . . . . . . 9 (𝑦 = π‘Œ β†’ (𝑦 βˆ’ 𝑧) = (π‘Œ βˆ’ 𝑧))
2423eqeq1d 2734 . . . . . . . 8 (𝑦 = π‘Œ β†’ ((𝑦 βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏) ↔ (π‘Œ βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)))
2522, 24anbi12d 631 . . . . . . 7 (𝑦 = π‘Œ β†’ ((𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)) ↔ (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏))))
2625rexbidv 3178 . . . . . 6 (𝑦 = π‘Œ β†’ (βˆƒπ‘§ ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)) ↔ βˆƒπ‘§ ∈ 𝑃 (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏))))
27262ralbidv 3218 . . . . 5 (𝑦 = π‘Œ β†’ (βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)) ↔ βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏))))
2821, 27rspc2v 3622 . . . 4 ((𝑋 ∈ 𝑃 ∧ π‘Œ ∈ 𝑃) β†’ (βˆ€π‘₯ ∈ 𝑃 βˆ€π‘¦ ∈ 𝑃 βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (𝑦 ∈ (π‘₯𝐼𝑧) ∧ (𝑦 βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)) β†’ βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏))))
2915, 16, 28syl2anc 584 . . 3 (πœ‘ β†’ (βˆ€π‘₯ ∈ 𝑃 βˆ€π‘¦ ∈ 𝑃 βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (𝑦 ∈ (π‘₯𝐼𝑧) ∧ (𝑦 βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)) β†’ βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏))))
3014, 29mpd 15 . 2 (πœ‘ β†’ βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)))
31 axtgsegcon.3 . . 3 (πœ‘ β†’ 𝐴 ∈ 𝑃)
32 axtgsegcon.4 . . 3 (πœ‘ β†’ 𝐡 ∈ 𝑃)
33 oveq1 7418 . . . . . . 7 (π‘Ž = 𝐴 β†’ (π‘Ž βˆ’ 𝑏) = (𝐴 βˆ’ 𝑏))
3433eqeq2d 2743 . . . . . 6 (π‘Ž = 𝐴 β†’ ((π‘Œ βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏) ↔ (π‘Œ βˆ’ 𝑧) = (𝐴 βˆ’ 𝑏)))
3534anbi2d 629 . . . . 5 (π‘Ž = 𝐴 β†’ ((π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)) ↔ (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (𝐴 βˆ’ 𝑏))))
3635rexbidv 3178 . . . 4 (π‘Ž = 𝐴 β†’ (βˆƒπ‘§ ∈ 𝑃 (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)) ↔ βˆƒπ‘§ ∈ 𝑃 (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (𝐴 βˆ’ 𝑏))))
37 oveq2 7419 . . . . . . 7 (𝑏 = 𝐡 β†’ (𝐴 βˆ’ 𝑏) = (𝐴 βˆ’ 𝐡))
3837eqeq2d 2743 . . . . . 6 (𝑏 = 𝐡 β†’ ((π‘Œ βˆ’ 𝑧) = (𝐴 βˆ’ 𝑏) ↔ (π‘Œ βˆ’ 𝑧) = (𝐴 βˆ’ 𝐡)))
3938anbi2d 629 . . . . 5 (𝑏 = 𝐡 β†’ ((π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (𝐴 βˆ’ 𝑏)) ↔ (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (𝐴 βˆ’ 𝐡))))
4039rexbidv 3178 . . . 4 (𝑏 = 𝐡 β†’ (βˆƒπ‘§ ∈ 𝑃 (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (𝐴 βˆ’ 𝑏)) ↔ βˆƒπ‘§ ∈ 𝑃 (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (𝐴 βˆ’ 𝐡))))
4136, 40rspc2v 3622 . . 3 ((𝐴 ∈ 𝑃 ∧ 𝐡 ∈ 𝑃) β†’ (βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)) β†’ βˆƒπ‘§ ∈ 𝑃 (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (𝐴 βˆ’ 𝐡))))
4231, 32, 41syl2anc 584 . 2 (πœ‘ β†’ (βˆ€π‘Ž ∈ 𝑃 βˆ€π‘ ∈ 𝑃 βˆƒπ‘§ ∈ 𝑃 (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (π‘Ž βˆ’ 𝑏)) β†’ βˆƒπ‘§ ∈ 𝑃 (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (𝐴 βˆ’ 𝐡))))
4330, 42mpd 15 1 (πœ‘ β†’ βˆƒπ‘§ ∈ 𝑃 (π‘Œ ∈ (𝑋𝐼𝑧) ∧ (π‘Œ βˆ’ 𝑧) = (𝐴 βˆ’ 𝐡)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396   ∨ w3o 1086   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  {cab 2709   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  {crab 3432  Vcvv 3474  [wsbc 3777   βˆ– cdif 3945   ∩ cin 3947  {csn 4628  β€˜cfv 6543  (class class class)co 7411   ∈ cmpo 7413  Basecbs 17146  distcds 17208  TarskiGcstrkg 27716  TarskiGCcstrkgc 27717  TarskiGBcstrkgb 27718  TarskiGCBcstrkgcb 27719  Itvcitv 27722  LineGclng 27723
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-nul 5306
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7414  df-trkgcb 27739  df-trkg 27742
This theorem is referenced by:  tgcgrtriv  27773  tgbtwntriv2  27776  tgbtwnouttr2  27784  tgbtwndiff  27795  tgifscgr  27797  tgcgrxfr  27807  lnext  27856  tgbtwnconn1lem3  27863  tgbtwnconn1  27864  legtrid  27880  hlcgrex  27905  mirreu3  27943  miriso  27959  midexlem  27981  footexALT  28007  footex  28010  opphllem  28024  flatcgra  28113  dfcgra2  28119  f1otrg  28160
  Copyright terms: Public domain W3C validator