Theorem axtgsegcon 28452

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 28441	. . . . . 6 ⊢ TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
2		inss2 4189	. . . . . . 7 ⊢ ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})
3		inss1 4188	. . . . . . 7 ⊢ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}) ⊆ TarskiGCB
4	2, 3	sstri 3941	. . . . . 6 ⊢ ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥 ∈ 𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ TarskiGCB
5	1, 4	eqsstri 3978	. . . . 5 ⊢ TarskiG ⊆ TarskiGCB
6		axtrkg.g	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
7	5, 6	sselid 3929	. . . 4 ⊢ (𝜑 → 𝐺 ∈ TarskiGCB)
8		axtrkg.p	. . . . . . 7 ⊢ 𝑃 = (Base‘𝐺)
9		axtrkg.d	. . . . . . 7 ⊢ − = (dist‘𝐺)
10		axtrkg.i	. . . . . . 7 ⊢ 𝐼 = (Itv‘𝐺)
11	8, 9, 10	istrkgcb 28444	. . . . . 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 7362	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑥𝐼𝑧) = (𝑋𝐼𝑧))
18	17	eleq2d 2819	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (𝑦 ∈ (𝑥𝐼𝑧) ↔ 𝑦 ∈ (𝑋𝐼𝑧)))
19	18	anbi1d 631	. . . . . . 7 ⊢ (𝑥 = 𝑋 → ((𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏)) ↔ (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏))))
20	19	rexbidv 3158	. . . . . 6 ⊢ (𝑥 = 𝑋 → (∃𝑧 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏)) ↔ ∃𝑧 ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏))))
21	20	2ralbidv 3198	. . . . 5 ⊢ (𝑥 = 𝑋 → (∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏)) ↔ ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏))))
22		eleq1 2821	. . . . . . . 8 ⊢ (𝑦 = 𝑌 → (𝑦 ∈ (𝑋𝐼𝑧) ↔ 𝑌 ∈ (𝑋𝐼𝑧)))
23		oveq1 7362	. . . . . . . . 9 ⊢ (𝑦 = 𝑌 → (𝑦 − 𝑧) = (𝑌 − 𝑧))
24	23	eqeq1d 2735	. . . . . . . 8 ⊢ (𝑦 = 𝑌 → ((𝑦 − 𝑧) = (𝑎 − 𝑏) ↔ (𝑌 − 𝑧) = (𝑎 − 𝑏)))
25	22, 24	anbi12d 632	. . . . . . 7 ⊢ (𝑦 = 𝑌 → ((𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏)) ↔ (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝑎 − 𝑏))))
26	25	rexbidv 3158	. . . . . 6 ⊢ (𝑦 = 𝑌 → (∃𝑧 ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏)) ↔ ∃𝑧 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝑎 − 𝑏))))
27	26	2ralbidv 3198	. . . . 5 ⊢ (𝑦 = 𝑌 → (∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑦 ∈ (𝑋𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏)) ↔ ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝑎 − 𝑏))))
28	21, 27	rspc2v 3585	. . . 4 ⊢ ((𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏)) → ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝑎 − 𝑏))))
29	15, 16, 28	syl2anc 584	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑦 ∈ (𝑥𝐼𝑧) ∧ (𝑦 − 𝑧) = (𝑎 − 𝑏)) → ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝑎 − 𝑏))))
30	14, 29	mpd 15	. 2 ⊢ (𝜑 → ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ∃𝑧 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝑎 − 𝑏)))
31		axtgsegcon.3	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
32		axtgsegcon.4	. . 3 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
33		oveq1 7362	. . . . . . 7 ⊢ (𝑎 = 𝐴 → (𝑎 − 𝑏) = (𝐴 − 𝑏))
34	33	eqeq2d 2744	. . . . . 6 ⊢ (𝑎 = 𝐴 → ((𝑌 − 𝑧) = (𝑎 − 𝑏) ↔ (𝑌 − 𝑧) = (𝐴 − 𝑏)))
35	34	anbi2d 630	. . . . 5 ⊢ (𝑎 = 𝐴 → ((𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝑎 − 𝑏)) ↔ (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝐴 − 𝑏))))
36	35	rexbidv 3158	. . . 4 ⊢ (𝑎 = 𝐴 → (∃𝑧 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝑎 − 𝑏)) ↔ ∃𝑧 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝐴 − 𝑏))))
37		oveq2 7363	. . . . . . 7 ⊢ (𝑏 = 𝐵 → (𝐴 − 𝑏) = (𝐴 − 𝐵))
38	37	eqeq2d 2744	. . . . . 6 ⊢ (𝑏 = 𝐵 → ((𝑌 − 𝑧) = (𝐴 − 𝑏) ↔ (𝑌 − 𝑧) = (𝐴 − 𝐵)))
39	38	anbi2d 630	. . . . 5 ⊢ (𝑏 = 𝐵 → ((𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝐴 − 𝑏)) ↔ (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝐴 − 𝐵))))
40	39	rexbidv 3158	. . . 4 ⊢ (𝑏 = 𝐵 → (∃𝑧 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝐴 − 𝑏)) ↔ ∃𝑧 ∈ 𝑃 (𝑌 ∈ (𝑋𝐼𝑧) ∧ (𝑌 − 𝑧) = (𝐴 − 𝐵))))
41	36, 40	rspc2v 3585	. . 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 1541   ∈ wcel 2113  {cab 2711   ≠ wne 2930  ∀wral 3049  ∃wrex 3058  {crab 3397  Vcvv 3438  [wsbc 3738   ∖ cdif 3896   ∩ cin 3898  {csn 4577  ‘cfv 6489  (class class class)co 7355   ∈ cmpo 7357  Basecbs 17130  distcds 17180  TarskiGcstrkg 28415  TarskiG_Ccstrkgc 28416  TarskiG_Bcstrkgb 28417  TarskiG_CBcstrkgcb 28418  Itvcitv 28421  LineGclng 28422

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-nul 5248

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-sbc 3739  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6445  df-fv 6497  df-ov 7358  df-trkgcb 28438  df-trkg 28441

This theorem is referenced by:  tgcgrtriv  28472  tgbtwntriv2  28475  tgbtwnouttr2  28483  tgbtwndiff  28494  tgifscgr  28496  tgcgrxfr  28506  lnext  28555  tgbtwnconn1lem3  28562  tgbtwnconn1  28563  legtrid  28579  hlcgrex  28604  mirreu3  28642  miriso  28658  midexlem  28680  footexALT  28706  footex  28709  opphllem  28723  flatcgra  28812  dfcgra2  28818  f1otrg  28859