Metamath Proof Explorer

Theorem axtgsegcon

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 A B , one can construct a line segment congruent to it, starting at any point Y and going in the direction of any ray containing Y . The ray is determined by the point Y and a second point X , the endpoint of the ray. The other endpoint of the line segment to be constructed is just the point z whose existence is asserted." (Contributed by Thierry Arnoux, 15-Mar-2019)

Ref Expression
Hypotheses axtrkg.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
axtrkg.d ⊢ − = ( dist ‘ 𝐺 )
axtrkg.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
axtrkg.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
axtgsegcon.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
axtgsegcon.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
axtgsegcon.3 ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
axtgsegcon.4 ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
Assertion axtgsegcon ( 𝜑 → ∃ 𝑧 ∈ 𝑃 ( 𝑌 ∈ ( 𝑋 𝐼 𝑧 ) ∧ ( 𝑌 − 𝑧 ) = ( 𝐴 − 𝐵 ) ) )

Proof

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