MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axtg5seg Structured version   Visualization version   Unicode version
Theorem axtg5seg 25364
Description: Five segments axiom, Axiom A5 of [Schwabhauser] p. 11. Take two triangles X Z U and A C V, a point Y on X Z, and a point B on A C. If all corresponding line segments except for Z U and C V are congruent ( i.e., X Y .~ A B, Y Z .~ B C, X U .~ A V, and Y U .~ B V), then Z U and C V are also congruent. As noted in Axiom 5 of [Tarski1999] p. 178, "this axiom is similar in character to the well-known theorems of Euclidean geometry that allow one to conclude, from hypotheses about the congruence of certain corresponding sides and angles in two triangles, the congruence of other corresponding sides and angles." (Contributed by Thierry Arnoux, 14-Mar-2019.)
Hypotheses
Ref Expression
axtrkg.p |- P = ( Base ` G )
axtrkg.d |- .- = ( dist ` G )
axtrkg.i |- I = (Itv ` G )
axtrkg.g |- ( ph -> G e. TarskiG )
axtg5seg.1 |- ( ph -> X e. P )
axtg5seg.2 |- ( ph -> Y e. P )
axtg5seg.3 |- ( ph -> Z e. P )
axtg5seg.4 |- ( ph -> A e. P )
axtg5seg.5 |- ( ph -> B e. P )
axtg5seg.6 |- ( ph -> C e. P )
axtg5seg.7 |- ( ph -> U e. P )
axtg5seg.8 |- ( ph -> V e. P )
axtg5seg.9 |- ( ph -> X =/= Y )
axtg5seg.10 |- ( ph -> Y e. ( X I Z ) )
axtg5seg.11 |- ( ph -> B e. ( A I C ) )
axtg5seg.12 |- ( ph -> ( X .- Y ) = ( A .- B ) )
axtg5seg.13 |- ( ph -> ( Y .- Z ) = ( B .- C ) )
axtg5seg.14 |- ( ph -> ( X .- U ) = ( A .- V ) )
axtg5seg.15 |- ( ph -> ( Y .- U ) = ( B .- V ) )
Assertion
Ref Expression
axtg5seg |- ( ph -> ( Z .- U ) = ( C .- V ) )
Proof of Theorem axtg5seg
Dummy variables f i p x y z a b c v u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-trkg 25352 . . . . . . 7 |- 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 ) ) } ) } ) )
2 inss2 3834 . . . . . . . 8 |- ( (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 ) ) } ) } )
3 inss1 3833 . . . . . . . 8 |- (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
42, 3sstri 3612 . . . . . . 7 |- ( (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
51, 4eqsstri 3635 . . . . . 6 |- TarskiG C_ TarskiGCB
6 axtrkg.g . . . . . 6 |- ( ph -> G e. TarskiG )
75, 6sseldi 3601 . . . . 5 |- ( ph -> G e. TarskiGCB )
8 axtrkg.p . . . . . . . 8 |- P = ( Base ` G )
9 axtrkg.d . . . . . . . 8 |- .- = ( dist ` G )
10 axtrkg.i . . . . . . . 8 |- I = (Itv ` G )
118, 9, 10istrkgcb 25355 . . . . . . 7 |- ( 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 ) ) ) ) )
1211simprbi 480 . . . . . 6 |- ( 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 ) ) ) )
1312simpld 475 . . . . 5 |- ( 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 ) ) )
147, 13syl 17 . . . 4 |- ( ph -> 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 ) ) )
15 axtg5seg.1 . . . . 5 |- ( ph -> X e. P )
16 axtg5seg.2 . . . . 5 |- ( ph -> Y e. P )
17 axtg5seg.3 . . . . 5 |- ( ph -> Z e. P )
18 neeq1 2856 . . . . . . . . . . . 12 |- ( x = X -> ( x =/= y <-> X =/= y ) )
19 oveq1 6657 . . . . . . . . . . . . 13 |- ( x = X -> ( x I z ) = ( X I z ) )
2019eleq2d 2687 . . . . . . . . . . . 12 |- ( x = X -> ( y e. ( x I z ) <-> y e. ( X I z ) ) )
2118, 203anbi12d 1400 . . . . . . . . . . 11 |- ( x = X -> ( ( x =/= y /\ y e. ( x I z ) /\ b e. ( a I c ) ) <-> ( X =/= y /\ y e. ( X I z ) /\ b e. ( a I c ) ) ) )
22 oveq1 6657 . . . . . . . . . . . . . 14 |- ( x = X -> ( x .- y ) = ( X .- y ) )
2322eqeq1d 2624 . . . . . . . . . . . . 13 |- ( x = X -> ( ( x .- y ) = ( a .- b ) <-> ( X .- y ) = ( a .- b ) ) )
2423anbi1d 741 . . . . . . . . . . . 12 |- ( x = X -> ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) <-> ( ( X .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) ) )
25 oveq1 6657 . . . . . . . . . . . . . 14 |- ( x = X -> ( x .- u ) = ( X .- u ) )
2625eqeq1d 2624 . . . . . . . . . . . . 13 |- ( x = X -> ( ( x .- u ) = ( a .- v ) <-> ( X .- u ) = ( a .- v ) ) )
2726anbi1d 741 . . . . . . . . . . . 12 |- ( x = X -> ( ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) <-> ( ( X .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) )
2824, 27anbi12d 747 . . . . . . . . . . 11 |- ( x = X -> ( ( ( ( x .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( x .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) <-> ( ( ( X .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) ) )
2921, 28anbi12d 747 . . . . . . . . . 10 |- ( x = X -> ( ( ( 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 ) ) ) ) <-> ( ( 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 ) ) ) ) ) )
3029imbi1d 331 . . . . . . . . 9 |- ( x = X -> ( ( ( ( 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 ) ) <-> ( ( ( 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 ) ) ) )
3130ralbidv 2986 . . . . . . . 8 |- ( x = X -> ( 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. 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 ) ) ) )
32312ralbidv 2989 . . . . . . 7 |- ( x = X -> ( 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. 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 ) ) ) )
33322ralbidv 2989 . . . . . 6 |- ( x = X -> ( 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. 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 ) ) ) )
34 neeq2 2857 . . . . . . . . . . . 12 |- ( y = Y -> ( X =/= y <-> X =/= Y ) )
35 eleq1 2689 . . . . . . . . . . . 12 |- ( y = Y -> ( y e. ( X I z ) <-> Y e. ( X I z ) ) )
3634, 353anbi12d 1400 . . . . . . . . . . 11 |- ( y = Y -> ( ( X =/= y /\ y e. ( X I z ) /\ b e. ( a I c ) ) <-> ( X =/= Y /\ Y e. ( X I z ) /\ b e. ( a I c ) ) ) )
37 oveq2 6658 . . . . . . . . . . . . . 14 |- ( y = Y -> ( X .- y ) = ( X .- Y ) )
3837eqeq1d 2624 . . . . . . . . . . . . 13 |- ( y = Y -> ( ( X .- y ) = ( a .- b ) <-> ( X .- Y ) = ( a .- b ) ) )
39 oveq1 6657 . . . . . . . . . . . . . 14 |- ( y = Y -> ( y .- z ) = ( Y .- z ) )
4039eqeq1d 2624 . . . . . . . . . . . . 13 |- ( y = Y -> ( ( y .- z ) = ( b .- c ) <-> ( Y .- z ) = ( b .- c ) ) )
4138, 40anbi12d 747 . . . . . . . . . . . 12 |- ( y = Y -> ( ( ( X .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) <-> ( ( X .- Y ) = ( a .- b ) /\ ( Y .- z ) = ( b .- c ) ) ) )
42 oveq1 6657 . . . . . . . . . . . . . 14 |- ( y = Y -> ( y .- u ) = ( Y .- u ) )
4342eqeq1d 2624 . . . . . . . . . . . . 13 |- ( y = Y -> ( ( y .- u ) = ( b .- v ) <-> ( Y .- u ) = ( b .- v ) ) )
4443anbi2d 740 . . . . . . . . . . . 12 |- ( y = Y -> ( ( ( X .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) <-> ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) )
4541, 44anbi12d 747 . . . . . . . . . . 11 |- ( y = Y -> ( ( ( ( X .- y ) = ( a .- b ) /\ ( y .- z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( y .- u ) = ( b .- v ) ) ) <-> ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) ) )
4636, 45anbi12d 747 . . . . . . . . . 10 |- ( y = Y -> ( ( ( 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 ) ) ) ) <-> ( ( 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 ) ) ) ) ) )
4746imbi1d 331 . . . . . . . . 9 |- ( y = Y -> ( ( ( ( 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 ) ) <-> ( ( ( 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 ) ) ) )
4847ralbidv 2986 . . . . . . . 8 |- ( y = Y -> ( 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. 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 ) ) ) )
49482ralbidv 2989 . . . . . . 7 |- ( y = Y -> ( 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. 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 ) ) ) )
50492ralbidv 2989 . . . . . 6 |- ( y = Y -> ( 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. 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 ) ) ) )
51 oveq2 6658 . . . . . . . . . . . . 13 |- ( z = Z -> ( X I z ) = ( X I Z ) )
5251eleq2d 2687 . . . . . . . . . . . 12 |- ( z = Z -> ( Y e. ( X I z ) <-> Y e. ( X I Z ) ) )
53523anbi2d 1404 . . . . . . . . . . 11 |- ( z = Z -> ( ( X =/= Y /\ Y e. ( X I z ) /\ b e. ( a I c ) ) <-> ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( a I c ) ) ) )
54 oveq2 6658 . . . . . . . . . . . . . 14 |- ( z = Z -> ( Y .- z ) = ( Y .- Z ) )
5554eqeq1d 2624 . . . . . . . . . . . . 13 |- ( z = Z -> ( ( Y .- z ) = ( b .- c ) <-> ( Y .- Z ) = ( b .- c ) ) )
5655anbi2d 740 . . . . . . . . . . . 12 |- ( z = Z -> ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- z ) = ( b .- c ) ) <-> ( ( X .- Y ) = ( a .- b ) /\ ( Y .- Z ) = ( b .- c ) ) ) )
5756anbi1d 741 . . . . . . . . . . 11 |- ( z = Z -> ( ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) <-> ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) ) )
5853, 57anbi12d 747 . . . . . . . . . 10 |- ( z = Z -> ( ( ( 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 ) ) ) ) <-> ( ( 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 ) ) ) ) ) )
59 oveq1 6657 . . . . . . . . . . 11 |- ( z = Z -> ( z .- u ) = ( Z .- u ) )
6059eqeq1d 2624 . . . . . . . . . 10 |- ( z = Z -> ( ( z .- u ) = ( c .- v ) <-> ( Z .- u ) = ( c .- v ) ) )
6158, 60imbi12d 334 . . . . . . . . 9 |- ( z = Z -> ( ( ( ( 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 ) ) <-> ( ( ( 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 ) ) ) )
6261ralbidv 2986 . . . . . . . 8 |- ( z = Z -> ( 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. 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 ) ) ) )
63622ralbidv 2989 . . . . . . 7 |- ( z = Z -> ( 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. 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 ) ) ) )
64632ralbidv 2989 . . . . . 6 |- ( z = Z -> ( 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. 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 ) ) ) )
6533, 50, 64rspc3v 3325 . . . . 5 |- ( ( X e. P /\ Y e. P /\ Z e. P ) -> ( 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. 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 ) ) ) )
6615, 16, 17, 65syl3anc 1326 . . . 4 |- ( ph -> ( 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. 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 ) ) ) )
6714, 66mpd 15 . . 3 |- ( ph -> 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 ) ) )
68 axtg5seg.7 . . . 4 |- ( ph -> U e. P )
69 axtg5seg.4 . . . 4 |- ( ph -> A e. P )
70 axtg5seg.5 . . . 4 |- ( ph -> B e. P )
71 oveq2 6658 . . . . . . . . . . 11 |- ( u = U -> ( X .- u ) = ( X .- U ) )
7271eqeq1d 2624 . . . . . . . . . 10 |- ( u = U -> ( ( X .- u ) = ( a .- v ) <-> ( X .- U ) = ( a .- v ) ) )
73 oveq2 6658 . . . . . . . . . . 11 |- ( u = U -> ( Y .- u ) = ( Y .- U ) )
7473eqeq1d 2624 . . . . . . . . . 10 |- ( u = U -> ( ( Y .- u ) = ( b .- v ) <-> ( Y .- U ) = ( b .- v ) ) )
7572, 74anbi12d 747 . . . . . . . . 9 |- ( u = U -> ( ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) <-> ( ( X .- U ) = ( a .- v ) /\ ( Y .- U ) = ( b .- v ) ) ) )
7675anbi2d 740 . . . . . . . 8 |- ( u = U -> ( ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- u ) = ( a .- v ) /\ ( Y .- u ) = ( b .- v ) ) ) <-> ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- U ) = ( a .- v ) /\ ( Y .- U ) = ( b .- v ) ) ) ) )
7776anbi2d 740 . . . . . . 7 |- ( u = U -> ( ( ( 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 ) ) ) ) <-> ( ( 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 ) ) ) ) ) )
78 oveq2 6658 . . . . . . . 8 |- ( u = U -> ( Z .- u ) = ( Z .- U ) )
7978eqeq1d 2624 . . . . . . 7 |- ( u = U -> ( ( Z .- u ) = ( c .- v ) <-> ( Z .- U ) = ( c .- v ) ) )
8077, 79imbi12d 334 . . . . . 6 |- ( u = U -> ( ( ( ( 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 ) ) <-> ( ( ( 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 ) ) ) )
81802ralbidv 2989 . . . . 5 |- ( u = U -> ( 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. 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 ) ) ) )
82 oveq1 6657 . . . . . . . . . 10 |- ( a = A -> ( a I c ) = ( A I c ) )
8382eleq2d 2687 . . . . . . . . 9 |- ( a = A -> ( b e. ( a I c ) <-> b e. ( A I c ) ) )
84833anbi3d 1405 . . . . . . . 8 |- ( a = A -> ( ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( a I c ) ) <-> ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( A I c ) ) ) )
85 oveq1 6657 . . . . . . . . . . 11 |- ( a = A -> ( a .- b ) = ( A .- b ) )
8685eqeq2d 2632 . . . . . . . . . 10 |- ( a = A -> ( ( X .- Y ) = ( a .- b ) <-> ( X .- Y ) = ( A .- b ) ) )
8786anbi1d 741 . . . . . . . . 9 |- ( a = A -> ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- Z ) = ( b .- c ) ) <-> ( ( X .- Y ) = ( A .- b ) /\ ( Y .- Z ) = ( b .- c ) ) ) )
88 oveq1 6657 . . . . . . . . . . 11 |- ( a = A -> ( a .- v ) = ( A .- v ) )
8988eqeq2d 2632 . . . . . . . . . 10 |- ( a = A -> ( ( X .- U ) = ( a .- v ) <-> ( X .- U ) = ( A .- v ) ) )
9089anbi1d 741 . . . . . . . . 9 |- ( a = A -> ( ( ( X .- U ) = ( a .- v ) /\ ( Y .- U ) = ( b .- v ) ) <-> ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( b .- v ) ) ) )
9187, 90anbi12d 747 . . . . . . . 8 |- ( a = A -> ( ( ( ( X .- Y ) = ( a .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- U ) = ( a .- v ) /\ ( Y .- U ) = ( b .- v ) ) ) <-> ( ( ( X .- Y ) = ( A .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( b .- v ) ) ) ) )
9284, 91anbi12d 747 . . . . . . 7 |- ( a = A -> ( ( ( 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 ) ) ) ) <-> ( ( 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 ) ) ) ) ) )
9392imbi1d 331 . . . . . 6 |- ( a = A -> ( ( ( ( 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 ) ) <-> ( ( ( 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 ) ) ) )
94932ralbidv 2989 . . . . 5 |- ( a = A -> ( 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. 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 ) ) ) )
95 eleq1 2689 . . . . . . . . 9 |- ( b = B -> ( b e. ( A I c ) <-> B e. ( A I c ) ) )
96953anbi3d 1405 . . . . . . . 8 |- ( b = B -> ( ( X =/= Y /\ Y e. ( X I Z ) /\ b e. ( A I c ) ) <-> ( X =/= Y /\ Y e. ( X I Z ) /\ B e. ( A I c ) ) ) )
97 oveq2 6658 . . . . . . . . . . 11 |- ( b = B -> ( A .- b ) = ( A .- B ) )
9897eqeq2d 2632 . . . . . . . . . 10 |- ( b = B -> ( ( X .- Y ) = ( A .- b ) <-> ( X .- Y ) = ( A .- B ) ) )
99 oveq1 6657 . . . . . . . . . . 11 |- ( b = B -> ( b .- c ) = ( B .- c ) )
10099eqeq2d 2632 . . . . . . . . . 10 |- ( b = B -> ( ( Y .- Z ) = ( b .- c ) <-> ( Y .- Z ) = ( B .- c ) ) )
10198, 100anbi12d 747 . . . . . . . . 9 |- ( b = B -> ( ( ( X .- Y ) = ( A .- b ) /\ ( Y .- Z ) = ( b .- c ) ) <-> ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- c ) ) ) )
102 oveq1 6657 . . . . . . . . . . 11 |- ( b = B -> ( b .- v ) = ( B .- v ) )
103102eqeq2d 2632 . . . . . . . . . 10 |- ( b = B -> ( ( Y .- U ) = ( b .- v ) <-> ( Y .- U ) = ( B .- v ) ) )
104103anbi2d 740 . . . . . . . . 9 |- ( b = B -> ( ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( b .- v ) ) <-> ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( B .- v ) ) ) )
105101, 104anbi12d 747 . . . . . . . 8 |- ( b = B -> ( ( ( ( X .- Y ) = ( A .- b ) /\ ( Y .- Z ) = ( b .- c ) ) /\ ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( b .- v ) ) ) <-> ( ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- c ) ) /\ ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( B .- v ) ) ) ) )
10696, 105anbi12d 747 . . . . . . 7 |- ( b = B -> ( ( ( 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 ) ) ) ) <-> ( ( 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 ) ) ) ) ) )
107106imbi1d 331 . . . . . 6 |- ( b = B -> ( ( ( ( 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 ) ) <-> ( ( ( 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 ) ) ) )
1081072ralbidv 2989 . . . . 5 |- ( b = B -> ( 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. 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 ) ) ) )
10981, 94, 108rspc3v 3325 . . . 4 |- ( ( U e. P /\ A e. P /\ B 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. 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 ) ) ) )
11068, 69, 70, 109syl3anc 1326 . . 3 |- ( ph -> ( 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. 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 ) ) ) )
11167, 110mpd 15 . 2 |- ( ph -> 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 ) ) )
112 axtg5seg.9 . . . 4 |- ( ph -> X =/= Y )
113 axtg5seg.10 . . . 4 |- ( ph -> Y e. ( X I Z ) )
114 axtg5seg.11 . . . 4 |- ( ph -> B e. ( A I C ) )
115112, 113, 1143jca 1242 . . 3 |- ( ph -> ( X =/= Y /\ Y e. ( X I Z ) /\ B e. ( A I C ) ) )
116 axtg5seg.12 . . . 4 |- ( ph -> ( X .- Y ) = ( A .- B ) )
117 axtg5seg.13 . . . 4 |- ( ph -> ( Y .- Z ) = ( B .- C ) )
118116, 117jca 554 . . 3 |- ( ph -> ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- C ) ) )
119 axtg5seg.14 . . . 4 |- ( ph -> ( X .- U ) = ( A .- V ) )
120 axtg5seg.15 . . . 4 |- ( ph -> ( Y .- U ) = ( B .- V ) )
121119, 120jca 554 . . 3 |- ( ph -> ( ( X .- U ) = ( A .- V ) /\ ( Y .- U ) = ( B .- V ) ) )
122115, 118, 121jca32 558 . 2 |- ( ph -> ( ( 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 ) ) ) ) )
123 axtg5seg.6 . . 3 |- ( ph -> C e. P )
124 axtg5seg.8 . . 3 |- ( ph -> V e. P )
125 oveq2 6658 . . . . . . . 8 |- ( c = C -> ( A I c ) = ( A I C ) )
126125eleq2d 2687 . . . . . . 7 |- ( c = C -> ( B e. ( A I c ) <-> B e. ( A I C ) ) )
1271263anbi3d 1405 . . . . . 6 |- ( c = C -> ( ( X =/= Y /\ Y e. ( X I Z ) /\ B e. ( A I c ) ) <-> ( X =/= Y /\ Y e. ( X I Z ) /\ B e. ( A I C ) ) ) )
128 oveq2 6658 . . . . . . . . 9 |- ( c = C -> ( B .- c ) = ( B .- C ) )
129128eqeq2d 2632 . . . . . . . 8 |- ( c = C -> ( ( Y .- Z ) = ( B .- c ) <-> ( Y .- Z ) = ( B .- C ) ) )
130129anbi2d 740 . . . . . . 7 |- ( c = C -> ( ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- c ) ) <-> ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- C ) ) ) )
131130anbi1d 741 . . . . . 6 |- ( c = C -> ( ( ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- c ) ) /\ ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( B .- v ) ) ) <-> ( ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- C ) ) /\ ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( B .- v ) ) ) ) )
132127, 131anbi12d 747 . . . . 5 |- ( c = C -> ( ( ( 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 ) ) ) ) <-> ( ( 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 ) ) ) ) ) )
133 oveq1 6657 . . . . . 6 |- ( c = C -> ( c .- v ) = ( C .- v ) )
134133eqeq2d 2632 . . . . 5 |- ( c = C -> ( ( Z .- U ) = ( c .- v ) <-> ( Z .- U ) = ( C .- v ) ) )
135132, 134imbi12d 334 . . . 4 |- ( c = C -> ( ( ( ( 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 ) ) <-> ( ( ( 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 ) ) ) )
136 oveq2 6658 . . . . . . . . 9 |- ( v = V -> ( A .- v ) = ( A .- V ) )
137136eqeq2d 2632 . . . . . . . 8 |- ( v = V -> ( ( X .- U ) = ( A .- v ) <-> ( X .- U ) = ( A .- V ) ) )
138 oveq2 6658 . . . . . . . . 9 |- ( v = V -> ( B .- v ) = ( B .- V ) )
139138eqeq2d 2632 . . . . . . . 8 |- ( v = V -> ( ( Y .- U ) = ( B .- v ) <-> ( Y .- U ) = ( B .- V ) ) )
140137, 139anbi12d 747 . . . . . . 7 |- ( v = V -> ( ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( B .- v ) ) <-> ( ( X .- U ) = ( A .- V ) /\ ( Y .- U ) = ( B .- V ) ) ) )
141140anbi2d 740 . . . . . 6 |- ( v = V -> ( ( ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- C ) ) /\ ( ( X .- U ) = ( A .- v ) /\ ( Y .- U ) = ( B .- v ) ) ) <-> ( ( ( X .- Y ) = ( A .- B ) /\ ( Y .- Z ) = ( B .- C ) ) /\ ( ( X .- U ) = ( A .- V ) /\ ( Y .- U ) = ( B .- V ) ) ) ) )
142141anbi2d 740 . . . . 5 |- ( v = V -> ( ( ( 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 ) ) ) ) <-> ( ( 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 ) ) ) ) ) )
143 oveq2 6658 . . . . . 6 |- ( v = V -> ( C .- v ) = ( C .- V ) )
144143eqeq2d 2632 . . . . 5 |- ( v = V -> ( ( Z .- U ) = ( C .- v ) <-> ( Z .- U ) = ( C .- V ) ) )
145142, 144imbi12d 334 . . . 4 |- ( v = V -> ( ( ( ( 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 ) ) <-> ( ( ( 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 ) ) ) )
146135, 145rspc2v 3322 . . 3 |- ( ( C e. P /\ V 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 ) ) -> ( ( ( 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 ) ) ) )
147123, 124, 146syl2anc 693 . 2 |- ( ph -> ( 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 ) ) -> ( ( ( 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 ) ) ) )
148111, 122, 147mp2d 49 1 |- ( ph -> ( Z .- U ) = ( C .- V ) )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   /\ wa 384   \/ w3o 1036   /\ w3a 1037   = wceq 1483   e. wcel 1990   {cab 2608   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   [.wsbc 3435   \ cdif 3571   i^i cin 3573   {csn 4177   ` cfv 5888  (class class class)co 6650   |-> cmpt2 6652   Basecbs 15857   distcds 15950  TarskiGcstrkg 25329  TarskiGCcstrkgc 25330  TarskiGBcstrkgb 25331  TarskiGCBcstrkgcb 25332  Itvcitv 25335  LineGclng 25336
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-trkgcb 25349  df-trkg 25352
This theorem is referenced by:  tgcgrextend  25380  tgsegconeq  25381  tgifscgr  25403  tgfscgr  25463  tgbtwnconn1lem2  25468  tgbtwnconn1lem3  25469  miriso  25565  midexlem  25587  ragcgr  25602  footex  25613  lmiisolem  25688  f1otrg  25751  tg5segofs  30751
  Copyright terms: Public domain W3C validator