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 
|- P = ( Base ` G )
axtrkg.d 
|- .- = ( dist ` G )
axtrkg.i 
|- I = ( Itv ` G )
axtrkg.g 
|- ( ph -> G e. TarskiG )
axtgsegcon.1 
|- ( ph -> X e. P )
axtgsegcon.2 
|- ( ph -> Y e. P )
axtgsegcon.3 
|- ( ph -> A e. P )
axtgsegcon.4 
|- ( ph -> B e. P )
Assertion axtgsegcon 
|- ( ph -> E. z e. P ( Y e. ( X I z ) /\ ( Y .- z ) = ( A .- B ) ) )

Proof

Step Hyp Ref Expression
1 axtrkg.p 
 |-  P = ( Base ` G )
2 axtrkg.d 
 |-  .- = ( dist ` G )
3 axtrkg.i 
 |-  I = ( Itv ` G )
4 axtrkg.g 
 |-  ( ph -> G e. TarskiG )
5 axtgsegcon.1 
 |-  ( ph -> X e. P )
6 axtgsegcon.2 
 |-  ( ph -> Y e. P )
7 axtgsegcon.3 
 |-  ( ph -> A e. P )
8 axtgsegcon.4 
 |-  ( ph -> B e. P )
9 df-trkg 
 |-  TarskiG = ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB i^i { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } ) )
10 inss2 
 |-  ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB i^i { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } ) ) C_ ( TarskiGCB i^i { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } )
11 inss1 
 |-  ( TarskiGCB i^i { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } ) C_ TarskiGCB
12 10 11 sstri 
 |-  ( ( TarskiGC i^i TarskiGB ) i^i ( TarskiGCB i^i { f | [. ( Base ` f ) / p ]. [. ( Itv ` f ) / i ]. ( LineG ` f ) = ( x e. p , y e. ( p \ { x } ) |-> { z e. p | ( z e. ( x i y ) \/ x e. ( z i y ) \/ y e. ( x i z ) ) } ) } ) ) C_ TarskiGCB
13 9 12 eqsstri 
 |-  TarskiG C_ TarskiGCB
14 13 4 sseldi 
 |-  ( ph -> G e. TarskiGCB )
15 1 2 3 istrkgcb 
 |-  ( G e. TarskiGCB <-> ( G e. _V /\ ( A. x e. P A. y e. P A. z e. P A. u e. P A. a e. P A. b e. P A. c e. P A. v e. P ( ( ( x =/= y /\ y e. ( x I z ) /\ b e. ( a I c ) ) /\ ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) /\ A. x e. P A. y e. P A. a e. P A. b e. P E. z e. P ( y e. ( x I z ) /\ ( y .- z ) = ( a .- b ) ) ) ) )
16 15 simprbi 
 |-  ( G e. TarskiGCB -> ( A. x e. P A. y e. P A. z e. P A. u e. P A. a e. P A. b e. P A. c e. P A. v e. P ( ( ( x =/= y /\ y e. ( x I z ) /\ b e. ( a I c ) ) /\ ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) -> ( z .- u ) = ( c .- v ) ) /\ A. x e. P A. y e. P A. a e. P A. b e. P E. z e. P ( y e. ( x I z ) /\ ( y .- z ) = ( a .- b ) ) ) )
17 16 simprd 
 |-  ( G e. TarskiGCB -> A. x e. P A. y e. P A. a e. P A. b e. P E. z e. P ( y e. ( x I z ) /\ ( y .- z ) = ( a .- b ) ) )
18 14 17 syl 
 |-  ( ph -> A. x e. P A. y e. P A. a e. P A. b e. P E. z e. P ( y e. ( x I z ) /\ ( y .- z ) = ( a .- b ) ) )
19 oveq1 
 |-  ( x = X -> ( x I z ) = ( X I z ) )
20 19 eleq2d 
 |-  ( x = X -> ( y e. ( x I z ) <-> y e. ( X I z ) ) )
21 20 anbi1d 
 |-  ( x = X -> ( ( y e. ( x I z ) /\ ( y .- z ) = ( a .- b ) ) <-> ( y e. ( X I z ) /\ ( y .- z ) = ( a .- b ) ) ) )
22 21 rexbidv 
 |-  ( x = X -> ( E. z e. P ( y e. ( x I z ) /\ ( y .- z ) = ( a .- b ) ) <-> E. z e. P ( y e. ( X I z ) /\ ( y .- z ) = ( a .- b ) ) ) )
23 22 2ralbidv 
 |-  ( x = X -> ( A. a e. P A. b e. P E. z e. P ( y e. ( x I z ) /\ ( y .- z ) = ( a .- b ) ) <-> A. a e. P A. b e. P E. z e. P ( y e. ( X I z ) /\ ( y .- z ) = ( a .- b ) ) ) )
24 eleq1 
 |-  ( y = Y -> ( y e. ( X I z ) <-> Y e. ( X I z ) ) )
25 oveq1 
 |-  ( y = Y -> ( y .- z ) = ( Y .- z ) )
26 25 eqeq1d 
 |-  ( y = Y -> ( ( y .- z ) = ( a .- b ) <-> ( Y .- z ) = ( a .- b ) ) )
27 24 26 anbi12d 
 |-  ( y = Y -> ( ( y e. ( X I z ) /\ ( y .- z ) = ( a .- b ) ) <-> ( Y e. ( X I z ) /\ ( Y .- z ) = ( a .- b ) ) ) )
28 27 rexbidv 
 |-  ( y = Y -> ( E. z e. P ( y e. ( X I z ) /\ ( y .- z ) = ( a .- b ) ) <-> E. z e. P ( Y e. ( X I z ) /\ ( Y .- z ) = ( a .- b ) ) ) )
29 28 2ralbidv 
 |-  ( y = Y -> ( A. a e. P A. b e. P E. z e. P ( y e. ( X I z ) /\ ( y .- z ) = ( a .- b ) ) <-> A. a e. P A. b e. P E. z e. P ( Y e. ( X I z ) /\ ( Y .- z ) = ( a .- b ) ) ) )
30 23 29 rspc2v 
 |-  ( ( X e. P /\ Y e. P ) -> ( A. x e. P A. y e. P A. a e. P A. b e. P E. z e. P ( y e. ( x I z ) /\ ( y .- z ) = ( a .- b ) ) -> A. a e. P A. b e. P E. z e. P ( Y e. ( X I z ) /\ ( Y .- z ) = ( a .- b ) ) ) )
31 5 6 30 syl2anc 
 |-  ( ph -> ( A. x e. P A. y e. P A. a e. P A. b e. P E. z e. P ( y e. ( x I z ) /\ ( y .- z ) = ( a .- b ) ) -> A. a e. P A. b e. P E. z e. P ( Y e. ( X I z ) /\ ( Y .- z ) = ( a .- b ) ) ) )
32 18 31 mpd 
 |-  ( ph -> A. a e. P A. b e. P E. z e. P ( Y e. ( X I z ) /\ ( Y .- z ) = ( a .- b ) ) )
33 oveq1 
 |-  ( a = A -> ( a .- b ) = ( A .- b ) )
34 33 eqeq2d 
 |-  ( a = A -> ( ( Y .- z ) = ( a .- b ) <-> ( Y .- z ) = ( A .- b ) ) )
35 34 anbi2d 
 |-  ( a = A -> ( ( Y e. ( X I z ) /\ ( Y .- z ) = ( a .- b ) ) <-> ( Y e. ( X I z ) /\ ( Y .- z ) = ( A .- b ) ) ) )
36 35 rexbidv 
 |-  ( a = A -> ( E. z e. P ( Y e. ( X I z ) /\ ( Y .- z ) = ( a .- b ) ) <-> E. z e. P ( Y e. ( X I z ) /\ ( Y .- z ) = ( A .- b ) ) ) )
37 oveq2 
 |-  ( b = B -> ( A .- b ) = ( A .- B ) )
38 37 eqeq2d 
 |-  ( b = B -> ( ( Y .- z ) = ( A .- b ) <-> ( Y .- z ) = ( A .- B ) ) )
39 38 anbi2d 
 |-  ( b = B -> ( ( Y e. ( X I z ) /\ ( Y .- z ) = ( A .- b ) ) <-> ( Y e. ( X I z ) /\ ( Y .- z ) = ( A .- B ) ) ) )
40 39 rexbidv 
 |-  ( b = B -> ( E. z e. P ( Y e. ( X I z ) /\ ( Y .- z ) = ( A .- b ) ) <-> E. z e. P ( Y e. ( X I z ) /\ ( Y .- z ) = ( A .- B ) ) ) )
41 36 40 rspc2v 
 |-  ( ( A e. P /\ B e. P ) -> ( A. a e. P A. b e. P E. z e. P ( Y e. ( X I z ) /\ ( Y .- z ) = ( a .- b ) ) -> E. z e. P ( Y e. ( X I z ) /\ ( Y .- z ) = ( A .- B ) ) ) )
42 7 8 41 syl2anc 
 |-  ( ph -> ( A. a e. P A. b e. P E. z e. P ( Y e. ( X I z ) /\ ( Y .- z ) = ( a .- b ) ) -> E. z e. P ( Y e. ( X I z ) /\ ( Y .- z ) = ( A .- B ) ) ) )
43 32 42 mpd 
 |-  ( ph -> E. z e. P ( Y e. ( X I z ) /\ ( Y .- z ) = ( A .- B ) ) )