Theorem axtgsegcon 28389

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.

Step	Hyp	Ref	Expression
1		df-trkg 28378	. . . . . 6 ⊢ TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
2		inss2 4213	. . . . . . 7 ⊢ ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})
3		inss1 4212	. . . . . . 7 ⊢ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}) ⊆ TarskiGCB
4	2, 3	sstri 3968	. . . . . 6 ⊢ ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ TarskiGCB
5	1, 4	eqsstri 4005	. . . . 5 ⊢ TarskiG ⊆ TarskiGCB
6		axtrkg.g	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
7	5, 6	sselid 3956	. . . 4 ⊢ (𝜑 → 𝐺 ∈ TarskiGCB)
8		axtrkg.p	. . . . . . 7 ⊢ 𝑃 = (Base‘𝐺)
9		axtrkg.d	. . . . . . 7 ⊢ − = (dist‘𝐺)
10		axtrkg.i	. . . . . . 7 ⊢ 𝐼 = (Itv‘𝐺)
11	8, 9, 10	istrkgcb 28381	. . . . . 6 ⊢ (𝐺 ∈ TarskiGCB ↔ (𝐺 ∈ V ∧ (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏)))))
12	11	simprbi 496	. . . . 5 ⊢ (𝐺 ∈ TarskiGCB → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 ∀𝑢 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∀𝑐 ∈ 𝑃 ∀𝑣 ∈ 𝑃 (((𝑥 ≠ 𝑦 ∧ 𝑦 ∈ (𝑥𝐼𝑧) ∧ 𝑏 ∈ (𝑎𝐼𝑐)) ∧ (((𝑥 − 𝑦) = (𝑎 − 𝑏) ∧ (𝑦 − 𝑧) = (𝑏 − 𝑐)) ∧ ((𝑥 − 𝑢) = (𝑎 − 𝑣) ∧ (𝑦 − 𝑢) = (𝑏 − 𝑣)))) → (𝑧 − 𝑢) = (𝑐 − 𝑣)) ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏))))
13	12	simprd 495	. . . 4 ⊢ (𝐺 ∈ TarskiGCB → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏)))
14	7, 13	syl 17	. . 3 ⊢ (𝜑 → ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏)))
15		axtgsegcon.1	. . . 4 ⊢ (𝜑 → 𝑋 ∈ 𝑃)
16		axtgsegcon.2	. . . 4 ⊢ (𝜑 → 𝑌 ∈ 𝑃)
17		oveq1 7410	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑥𝐼𝑧) = (𝑋𝐼𝑧))
18	17	eleq2d 2820	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (𝑦 ∈ (𝑥𝐼𝑧) ↔ 𝑦 ∈ (𝑋𝐼𝑧)))
19	18	anbi1d 631	. . . . . . 7 ⊢ (𝑥 = 𝑋 → ((𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏)) ↔ (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏))))
20	19	rexbidv 3164	. . . . . 6 ⊢ (𝑥 = 𝑋 → (∃𝑧 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏)) ↔ ∃𝑧 ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏))))
21	20	2ralbidv 3205	. . . . 5 ⊢ (𝑥 = 𝑋 → (∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏)) ↔ ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏))))
22		eleq1 2822	. . . . . . . 8 ⊢ (𝑦 = 𝑌 → (𝑦 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑧)))
23		oveq1 7410	. . . . . . . . 9 ⊢ (𝑦 = 𝑌 → (𝑦 − 𝑧) = (𝑌 − 𝑧))
24	23	eqeq1d 2737	. . . . . . . 8 ⊢ (𝑦 = 𝑌 → ((𝑦 − 𝑧) = (𝑎 − 𝑏) ↔ (𝑌 − 𝑧) = (𝑎 − 𝑏)))
25	22, 24	anbi12d 632	. . . . . . 7 ⊢ (𝑦 = 𝑌 → ((𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏)) ↔ (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝑎 − 𝑏))))
26	25	rexbidv 3164	. . . . . 6 ⊢ (𝑦 = 𝑌 → (∃𝑧 ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏)) ↔ ∃𝑧 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝑎 − 𝑏))))
27	26	2ralbidv 3205	. . . . 5 ⊢ (𝑦 = 𝑌 → (∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏)) ↔ ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝑎 − 𝑏))))
28	21, 27	rspc2v 3612	. . . 4 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏)) → ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝑎 − 𝑏))))
29	15, 16, 28	syl2anc 584	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏)) → ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝑎 − 𝑏))))
30	14, 29	mpd 15	. 2 ⊢ (𝜑 → ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝑎 − 𝑏)))
31		axtgsegcon.3	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
32		axtgsegcon.4	. . 3 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
33		oveq1 7410	. . . . . . 7 ⊢ (𝑎 = 𝐴 → (𝑎 − 𝑏) = (𝐴 − 𝑏))
34	33	eqeq2d 2746	. . . . . 6 ⊢ (𝑎 = 𝐴 → ((𝑌 − 𝑧) = (𝑎 − 𝑏) ↔ (𝑌 − 𝑧) = (𝐴 − 𝑏)))
35	34	anbi2d 630	. . . . 5 ⊢ (𝑎 = 𝐴 → ((𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝑎 − 𝑏)) ↔ (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝐴 − 𝑏))))
36	35	rexbidv 3164	. . . 4 ⊢ (𝑎 = 𝐴 → (∃𝑧 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝑎 − 𝑏)) ↔ ∃𝑧 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝐴 − 𝑏))))
37		oveq2 7411	. . . . . . 7 ⊢ (𝑏 = 𝐵 → (𝐴 − 𝑏) = (𝐴 − 𝐵))
38	37	eqeq2d 2746	. . . . . 6 ⊢ (𝑏 = 𝐵 → ((𝑌 − 𝑧) = (𝐴 − 𝑏) ↔ (𝑌 − 𝑧) = (𝐴 − 𝐵)))
39	38	anbi2d 630	. . . . 5 ⊢ (𝑏 = 𝐵 → ((𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝐴 − 𝑏)) ↔ (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝐴 − 𝐵))))
40	39	rexbidv 3164	. . . 4 ⊢ (𝑏 = 𝐵 → (∃𝑧 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝐴 − 𝑏)) ↔ ∃𝑧 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝐴 − 𝐵))))
41	36, 40	rspc2v 3612	. . 3 ⊢ ((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) → (∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝑎 − 𝑏)) → ∃𝑧 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝐴 − 𝐵))))
42	31, 32, 41	syl2anc 584	. 2 ⊢ (𝜑 → (∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝑎 − 𝑏)) → ∃𝑧 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝐴 − 𝐵))))
43	30, 42	mpd 15	1 ⊢ (𝜑 → ∃𝑧 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝐴 − 𝐵)))

Syntax hints:   → wi 4   ∧ wa 395   ∨ w3o 1085   ∧ w3a 1086   = wceq 1540   ∈ wcel 2108  {cab 2713   ≠ wne 2932  ∀wral 3051  ∃wrex 3060  {crab 3415  Vcvv 3459  [wsbc 3765   ∖ cdif 3923   ∩ cin 3925  {csn 4601  ‘cfv 6530  (class class class)co 7403   ∈ cmpo 7405  Basecbs 17226  distcds 17278  TarskiGcstrkg 28352  TarskiG_Ccstrkgc 28353  TarskiG_Bcstrkgb 28354  TarskiG_CBcstrkgcb 28355  Itvcitv 28358  LineGclng 28359

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-nul 5276

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406  df-trkgcb 28375  df-trkg 28378

This theorem is referenced by:  tgcgrtriv  28409  tgbtwntriv2  28412  tgbtwnouttr2  28420  tgbtwndiff  28431  tgifscgr  28433  tgcgrxfr  28443  lnext  28492  tgbtwnconn1lem3  28499  tgbtwnconn1  28500  legtrid  28516  hlcgrex  28541  mirreu3  28579  miriso  28595  midexlem  28617  footexALT  28643  footex  28646  opphllem  28660  flatcgra  28749  dfcgra2  28755  f1otrg  28796