MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axtgupdim2 Structured version   Unicode version

Theorem axtgupdim2 24070
Description: Upper dimension axiom for dimension 2, Axiom A9 of [Schwabhauser] p. 13. (Contributed by Thierry Arnoux, 29-May-2019.)
Hypotheses
Ref Expression
axtrkge.p  |-  P  =  ( Base `  G
)
axtrkge.d  |-  .-  =  ( dist `  G )
axtrkge.i  |-  I  =  (Itv `  G )
axtgupdim2.g  |-  ( ph  ->  G  e. TarskiG2D )
axtgupdim2.x  |-  ( ph  ->  X  e.  P )
axtgupdim2.y  |-  ( ph  ->  Y  e.  P )
axtgupdim2.z  |-  ( ph  ->  Z  e.  P )
axtgupdim2.u  |-  ( ph  ->  U  e.  P )
axtgupdim2.v  |-  ( ph  ->  V  e.  P )
axtgupdim2.0  |-  ( ph  ->  U  =/=  V )
axtgupdim2.1  |-  ( ph  ->  ( X  .-  U
)  =  ( X 
.-  V ) )
axtgupdim2.2  |-  ( ph  ->  ( Y  .-  U
)  =  ( Y 
.-  V ) )
axtgupdim2.3  |-  ( ph  ->  ( Z  .-  U
)  =  ( Z 
.-  V ) )
Assertion
Ref Expression
axtgupdim2  |-  ( ph  ->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) )

Proof of Theorem axtgupdim2
Dummy variables  v  u  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 axtgupdim2.1 . . 3  |-  ( ph  ->  ( X  .-  U
)  =  ( X 
.-  V ) )
2 axtgupdim2.2 . . 3  |-  ( ph  ->  ( Y  .-  U
)  =  ( Y 
.-  V ) )
3 axtgupdim2.3 . . 3  |-  ( ph  ->  ( Z  .-  U
)  =  ( Z 
.-  V ) )
41, 2, 33jca 1174 . 2  |-  ( ph  ->  ( ( X  .-  U )  =  ( X  .-  V )  /\  ( Y  .-  U )  =  ( Y  .-  V )  /\  ( Z  .-  U )  =  ( Z  .-  V ) ) )
5 axtgupdim2.0 . 2  |-  ( ph  ->  U  =/=  V )
6 axtgupdim2.g . . . . . 6  |-  ( ph  ->  G  e. TarskiG2D )
7 axtrkge.p . . . . . . 7  |-  P  =  ( Base `  G
)
8 axtrkge.d . . . . . . 7  |-  .-  =  ( dist `  G )
9 axtrkge.i . . . . . . 7  |-  I  =  (Itv `  G )
107, 8, 9istrkg2d 24057 . . . . . 6  |-  ( G  e. TarskiG2D  <->  ( G  e.  _V  /\  ( E. x  e.  P  E. y  e.  P  E. z  e.  P  -.  ( z  e.  ( x I y )  \/  x  e.  ( z I y )  \/  y  e.  ( x I z ) )  /\  A. x  e.  P  A. y  e.  P  A. z  e.  P  A. u  e.  P  A. v  e.  P  ( (
( ( x  .-  u )  =  ( x  .-  v )  /\  ( y  .-  u )  =  ( y  .-  v )  /\  ( z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  ->  (
z  e.  ( x I y )  \/  x  e.  ( z I y )  \/  y  e.  ( x I z ) ) ) ) ) )
116, 10sylib 196 . . . . 5  |-  ( ph  ->  ( G  e.  _V  /\  ( E. x  e.  P  E. y  e.  P  E. z  e.  P  -.  ( z  e.  ( x I y )  \/  x  e.  ( z I y )  \/  y  e.  ( x I z ) )  /\  A. x  e.  P  A. y  e.  P  A. z  e.  P  A. u  e.  P  A. v  e.  P  (
( ( ( x 
.-  u )  =  ( x  .-  v
)  /\  ( y  .-  u )  =  ( y  .-  v )  /\  ( z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  ->  (
z  e.  ( x I y )  \/  x  e.  ( z I y )  \/  y  e.  ( x I z ) ) ) ) ) )
1211simprrd 756 . . . 4  |-  ( ph  ->  A. x  e.  P  A. y  e.  P  A. z  e.  P  A. u  e.  P  A. v  e.  P  ( ( ( ( x  .-  u )  =  ( x  .-  v )  /\  (
y  .-  u )  =  ( y  .-  v )  /\  (
z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  -> 
( z  e.  ( x I y )  \/  x  e.  ( z I y )  \/  y  e.  ( x I z ) ) ) )
13 axtgupdim2.x . . . . 5  |-  ( ph  ->  X  e.  P )
14 axtgupdim2.y . . . . 5  |-  ( ph  ->  Y  e.  P )
15 axtgupdim2.z . . . . 5  |-  ( ph  ->  Z  e.  P )
16 oveq1 6277 . . . . . . . . . . 11  |-  ( x  =  X  ->  (
x  .-  u )  =  ( X  .-  u ) )
17 oveq1 6277 . . . . . . . . . . 11  |-  ( x  =  X  ->  (
x  .-  v )  =  ( X  .-  v ) )
1816, 17eqeq12d 2476 . . . . . . . . . 10  |-  ( x  =  X  ->  (
( x  .-  u
)  =  ( x 
.-  v )  <->  ( X  .-  u )  =  ( X  .-  v ) ) )
19183anbi1d 1301 . . . . . . . . 9  |-  ( x  =  X  ->  (
( ( x  .-  u )  =  ( x  .-  v )  /\  ( y  .-  u )  =  ( y  .-  v )  /\  ( z  .-  u )  =  ( z  .-  v ) )  <->  ( ( X 
.-  u )  =  ( X  .-  v
)  /\  ( y  .-  u )  =  ( y  .-  v )  /\  ( z  .-  u )  =  ( z  .-  v ) ) ) )
2019anbi1d 702 . . . . . . . 8  |-  ( x  =  X  ->  (
( ( ( x 
.-  u )  =  ( x  .-  v
)  /\  ( y  .-  u )  =  ( y  .-  v )  /\  ( z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  <->  ( (
( X  .-  u
)  =  ( X 
.-  v )  /\  ( y  .-  u
)  =  ( y 
.-  v )  /\  ( z  .-  u
)  =  ( z 
.-  v ) )  /\  u  =/=  v
) ) )
21 oveq1 6277 . . . . . . . . . 10  |-  ( x  =  X  ->  (
x I y )  =  ( X I y ) )
2221eleq2d 2524 . . . . . . . . 9  |-  ( x  =  X  ->  (
z  e.  ( x I y )  <->  z  e.  ( X I y ) ) )
23 eleq1 2526 . . . . . . . . 9  |-  ( x  =  X  ->  (
x  e.  ( z I y )  <->  X  e.  ( z I y ) ) )
24 oveq1 6277 . . . . . . . . . 10  |-  ( x  =  X  ->  (
x I z )  =  ( X I z ) )
2524eleq2d 2524 . . . . . . . . 9  |-  ( x  =  X  ->  (
y  e.  ( x I z )  <->  y  e.  ( X I z ) ) )
2622, 23, 253orbi123d 1296 . . . . . . . 8  |-  ( x  =  X  ->  (
( z  e.  ( x I y )  \/  x  e.  ( z I y )  \/  y  e.  ( x I z ) )  <->  ( z  e.  ( X I y )  \/  X  e.  ( z I y )  \/  y  e.  ( X I z ) ) ) )
2720, 26imbi12d 318 . . . . . . 7  |-  ( x  =  X  ->  (
( ( ( ( x  .-  u )  =  ( x  .-  v )  /\  (
y  .-  u )  =  ( y  .-  v )  /\  (
z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  -> 
( z  e.  ( x I y )  \/  x  e.  ( z I y )  \/  y  e.  ( x I z ) ) )  <->  ( (
( ( X  .-  u )  =  ( X  .-  v )  /\  ( y  .-  u )  =  ( y  .-  v )  /\  ( z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  ->  (
z  e.  ( X I y )  \/  X  e.  ( z I y )  \/  y  e.  ( X I z ) ) ) ) )
28272ralbidv 2898 . . . . . 6  |-  ( x  =  X  ->  ( A. u  e.  P  A. v  e.  P  ( ( ( ( x  .-  u )  =  ( x  .-  v )  /\  (
y  .-  u )  =  ( y  .-  v )  /\  (
z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  -> 
( z  e.  ( x I y )  \/  x  e.  ( z I y )  \/  y  e.  ( x I z ) ) )  <->  A. u  e.  P  A. v  e.  P  ( (
( ( X  .-  u )  =  ( X  .-  v )  /\  ( y  .-  u )  =  ( y  .-  v )  /\  ( z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  ->  (
z  e.  ( X I y )  \/  X  e.  ( z I y )  \/  y  e.  ( X I z ) ) ) ) )
29 oveq1 6277 . . . . . . . . . . 11  |-  ( y  =  Y  ->  (
y  .-  u )  =  ( Y  .-  u ) )
30 oveq1 6277 . . . . . . . . . . 11  |-  ( y  =  Y  ->  (
y  .-  v )  =  ( Y  .-  v ) )
3129, 30eqeq12d 2476 . . . . . . . . . 10  |-  ( y  =  Y  ->  (
( y  .-  u
)  =  ( y 
.-  v )  <->  ( Y  .-  u )  =  ( Y  .-  v ) ) )
32313anbi2d 1302 . . . . . . . . 9  |-  ( y  =  Y  ->  (
( ( X  .-  u )  =  ( X  .-  v )  /\  ( y  .-  u )  =  ( y  .-  v )  /\  ( z  .-  u )  =  ( z  .-  v ) )  <->  ( ( X 
.-  u )  =  ( X  .-  v
)  /\  ( Y  .-  u )  =  ( Y  .-  v )  /\  ( z  .-  u )  =  ( z  .-  v ) ) ) )
3332anbi1d 702 . . . . . . . 8  |-  ( y  =  Y  ->  (
( ( ( X 
.-  u )  =  ( X  .-  v
)  /\  ( y  .-  u )  =  ( y  .-  v )  /\  ( z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  <->  ( (
( X  .-  u
)  =  ( X 
.-  v )  /\  ( Y  .-  u )  =  ( Y  .-  v )  /\  (
z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v ) ) )
34 oveq2 6278 . . . . . . . . . 10  |-  ( y  =  Y  ->  ( X I y )  =  ( X I Y ) )
3534eleq2d 2524 . . . . . . . . 9  |-  ( y  =  Y  ->  (
z  e.  ( X I y )  <->  z  e.  ( X I Y ) ) )
36 oveq2 6278 . . . . . . . . . 10  |-  ( y  =  Y  ->  (
z I y )  =  ( z I Y ) )
3736eleq2d 2524 . . . . . . . . 9  |-  ( y  =  Y  ->  ( X  e.  ( z
I y )  <->  X  e.  ( z I Y ) ) )
38 eleq1 2526 . . . . . . . . 9  |-  ( y  =  Y  ->  (
y  e.  ( X I z )  <->  Y  e.  ( X I z ) ) )
3935, 37, 383orbi123d 1296 . . . . . . . 8  |-  ( y  =  Y  ->  (
( z  e.  ( X I y )  \/  X  e.  ( z I y )  \/  y  e.  ( X I z ) )  <->  ( z  e.  ( X I Y )  \/  X  e.  ( z I Y )  \/  Y  e.  ( X I z ) ) ) )
4033, 39imbi12d 318 . . . . . . 7  |-  ( y  =  Y  ->  (
( ( ( ( X  .-  u )  =  ( X  .-  v )  /\  (
y  .-  u )  =  ( y  .-  v )  /\  (
z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  -> 
( z  e.  ( X I y )  \/  X  e.  ( z I y )  \/  y  e.  ( X I z ) ) )  <->  ( (
( ( X  .-  u )  =  ( X  .-  v )  /\  ( Y  .-  u )  =  ( Y  .-  v )  /\  ( z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  ->  (
z  e.  ( X I Y )  \/  X  e.  ( z I Y )  \/  Y  e.  ( X I z ) ) ) ) )
41402ralbidv 2898 . . . . . 6  |-  ( y  =  Y  ->  ( A. u  e.  P  A. v  e.  P  ( ( ( ( X  .-  u )  =  ( X  .-  v )  /\  (
y  .-  u )  =  ( y  .-  v )  /\  (
z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  -> 
( z  e.  ( X I y )  \/  X  e.  ( z I y )  \/  y  e.  ( X I z ) ) )  <->  A. u  e.  P  A. v  e.  P  ( (
( ( X  .-  u )  =  ( X  .-  v )  /\  ( Y  .-  u )  =  ( Y  .-  v )  /\  ( z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  ->  (
z  e.  ( X I Y )  \/  X  e.  ( z I Y )  \/  Y  e.  ( X I z ) ) ) ) )
42 oveq1 6277 . . . . . . . . . . 11  |-  ( z  =  Z  ->  (
z  .-  u )  =  ( Z  .-  u ) )
43 oveq1 6277 . . . . . . . . . . 11  |-  ( z  =  Z  ->  (
z  .-  v )  =  ( Z  .-  v ) )
4442, 43eqeq12d 2476 . . . . . . . . . 10  |-  ( z  =  Z  ->  (
( z  .-  u
)  =  ( z 
.-  v )  <->  ( Z  .-  u )  =  ( Z  .-  v ) ) )
45443anbi3d 1303 . . . . . . . . 9  |-  ( z  =  Z  ->  (
( ( X  .-  u )  =  ( X  .-  v )  /\  ( Y  .-  u )  =  ( Y  .-  v )  /\  ( z  .-  u )  =  ( z  .-  v ) )  <->  ( ( X 
.-  u )  =  ( X  .-  v
)  /\  ( Y  .-  u )  =  ( Y  .-  v )  /\  ( Z  .-  u )  =  ( Z  .-  v ) ) ) )
4645anbi1d 702 . . . . . . . 8  |-  ( z  =  Z  ->  (
( ( ( X 
.-  u )  =  ( X  .-  v
)  /\  ( Y  .-  u )  =  ( Y  .-  v )  /\  ( z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  <->  ( (
( X  .-  u
)  =  ( X 
.-  v )  /\  ( Y  .-  u )  =  ( Y  .-  v )  /\  ( Z  .-  u )  =  ( Z  .-  v
) )  /\  u  =/=  v ) ) )
47 eleq1 2526 . . . . . . . . 9  |-  ( z  =  Z  ->  (
z  e.  ( X I Y )  <->  Z  e.  ( X I Y ) ) )
48 oveq1 6277 . . . . . . . . . 10  |-  ( z  =  Z  ->  (
z I Y )  =  ( Z I Y ) )
4948eleq2d 2524 . . . . . . . . 9  |-  ( z  =  Z  ->  ( X  e.  ( z
I Y )  <->  X  e.  ( Z I Y ) ) )
50 oveq2 6278 . . . . . . . . . 10  |-  ( z  =  Z  ->  ( X I z )  =  ( X I Z ) )
5150eleq2d 2524 . . . . . . . . 9  |-  ( z  =  Z  ->  ( Y  e.  ( X I z )  <->  Y  e.  ( X I Z ) ) )
5247, 49, 513orbi123d 1296 . . . . . . . 8  |-  ( z  =  Z  ->  (
( z  e.  ( X I Y )  \/  X  e.  ( z I Y )  \/  Y  e.  ( X I z ) )  <->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) ) )
5346, 52imbi12d 318 . . . . . . 7  |-  ( z  =  Z  ->  (
( ( ( ( X  .-  u )  =  ( X  .-  v )  /\  ( Y  .-  u )  =  ( Y  .-  v
)  /\  ( z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  ->  (
z  e.  ( X I Y )  \/  X  e.  ( z I Y )  \/  Y  e.  ( X I z ) ) )  <->  ( ( ( ( X  .-  u
)  =  ( X 
.-  v )  /\  ( Y  .-  u )  =  ( Y  .-  v )  /\  ( Z  .-  u )  =  ( Z  .-  v
) )  /\  u  =/=  v )  ->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) ) ) )
54532ralbidv 2898 . . . . . 6  |-  ( z  =  Z  ->  ( A. u  e.  P  A. v  e.  P  ( ( ( ( X  .-  u )  =  ( X  .-  v )  /\  ( Y  .-  u )  =  ( Y  .-  v
)  /\  ( z  .-  u )  =  ( z  .-  v ) )  /\  u  =/=  v )  ->  (
z  e.  ( X I Y )  \/  X  e.  ( z I Y )  \/  Y  e.  ( X I z ) ) )  <->  A. u  e.  P  A. v  e.  P  ( ( ( ( X  .-  u )  =  ( X  .-  v )  /\  ( Y  .-  u )  =  ( Y  .-  v
)  /\  ( Z  .-  u )  =  ( Z  .-  v ) )  /\  u  =/=  v )  ->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) ) ) )
5528, 41, 54rspc3v 3219 . . . . 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. v  e.  P  ( ( ( ( x  .-  u
)  =  ( x 
.-  v )  /\  ( y  .-  u
)  =  ( y 
.-  v )  /\  ( z  .-  u
)  =  ( z 
.-  v ) )  /\  u  =/=  v
)  ->  ( z  e.  ( x I y )  \/  x  e.  ( z I y )  \/  y  e.  ( x I z ) ) )  ->  A. u  e.  P  A. v  e.  P  ( ( ( ( X  .-  u )  =  ( X  .-  v )  /\  ( Y  .-  u )  =  ( Y  .-  v
)  /\  ( Z  .-  u )  =  ( Z  .-  v ) )  /\  u  =/=  v )  ->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) ) ) )
5613, 14, 15, 55syl3anc 1226 . . . 4  |-  ( ph  ->  ( A. x  e.  P  A. y  e.  P  A. z  e.  P  A. u  e.  P  A. v  e.  P  ( ( ( ( x  .-  u
)  =  ( x 
.-  v )  /\  ( y  .-  u
)  =  ( y 
.-  v )  /\  ( z  .-  u
)  =  ( z 
.-  v ) )  /\  u  =/=  v
)  ->  ( z  e.  ( x I y )  \/  x  e.  ( z I y )  \/  y  e.  ( x I z ) ) )  ->  A. u  e.  P  A. v  e.  P  ( ( ( ( X  .-  u )  =  ( X  .-  v )  /\  ( Y  .-  u )  =  ( Y  .-  v
)  /\  ( Z  .-  u )  =  ( Z  .-  v ) )  /\  u  =/=  v )  ->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) ) ) )
5712, 56mpd 15 . . 3  |-  ( ph  ->  A. u  e.  P  A. v  e.  P  ( ( ( ( X  .-  u )  =  ( X  .-  v )  /\  ( Y  .-  u )  =  ( Y  .-  v
)  /\  ( Z  .-  u )  =  ( Z  .-  v ) )  /\  u  =/=  v )  ->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) ) )
58 axtgupdim2.u . . . 4  |-  ( ph  ->  U  e.  P )
59 axtgupdim2.v . . . 4  |-  ( ph  ->  V  e.  P )
60 oveq2 6278 . . . . . . . . 9  |-  ( u  =  U  ->  ( X  .-  u )  =  ( X  .-  U
) )
6160eqeq1d 2456 . . . . . . . 8  |-  ( u  =  U  ->  (
( X  .-  u
)  =  ( X 
.-  v )  <->  ( X  .-  U )  =  ( X  .-  v ) ) )
62 oveq2 6278 . . . . . . . . 9  |-  ( u  =  U  ->  ( Y  .-  u )  =  ( Y  .-  U
) )
6362eqeq1d 2456 . . . . . . . 8  |-  ( u  =  U  ->  (
( Y  .-  u
)  =  ( Y 
.-  v )  <->  ( Y  .-  U )  =  ( Y  .-  v ) ) )
64 oveq2 6278 . . . . . . . . 9  |-  ( u  =  U  ->  ( Z  .-  u )  =  ( Z  .-  U
) )
6564eqeq1d 2456 . . . . . . . 8  |-  ( u  =  U  ->  (
( Z  .-  u
)  =  ( Z 
.-  v )  <->  ( Z  .-  U )  =  ( Z  .-  v ) ) )
6661, 63, 653anbi123d 1297 . . . . . . 7  |-  ( u  =  U  ->  (
( ( X  .-  u )  =  ( X  .-  v )  /\  ( Y  .-  u )  =  ( Y  .-  v )  /\  ( Z  .-  u )  =  ( Z  .-  v ) )  <->  ( ( X 
.-  U )  =  ( X  .-  v
)  /\  ( Y  .-  U )  =  ( Y  .-  v )  /\  ( Z  .-  U )  =  ( Z  .-  v ) ) ) )
67 neeq1 2735 . . . . . . 7  |-  ( u  =  U  ->  (
u  =/=  v  <->  U  =/=  v ) )
6866, 67anbi12d 708 . . . . . 6  |-  ( u  =  U  ->  (
( ( ( X 
.-  u )  =  ( X  .-  v
)  /\  ( Y  .-  u )  =  ( Y  .-  v )  /\  ( Z  .-  u )  =  ( Z  .-  v ) )  /\  u  =/=  v )  <->  ( (
( X  .-  U
)  =  ( X 
.-  v )  /\  ( Y  .-  U )  =  ( Y  .-  v )  /\  ( Z  .-  U )  =  ( Z  .-  v
) )  /\  U  =/=  v ) ) )
6968imbi1d 315 . . . . 5  |-  ( u  =  U  ->  (
( ( ( ( X  .-  u )  =  ( X  .-  v )  /\  ( Y  .-  u )  =  ( Y  .-  v
)  /\  ( Z  .-  u )  =  ( Z  .-  v ) )  /\  u  =/=  v )  ->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) )  <->  ( (
( ( X  .-  U )  =  ( X  .-  v )  /\  ( Y  .-  U )  =  ( Y  .-  v )  /\  ( Z  .-  U )  =  ( Z  .-  v ) )  /\  U  =/=  v )  ->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) ) ) )
70 oveq2 6278 . . . . . . . . 9  |-  ( v  =  V  ->  ( X  .-  v )  =  ( X  .-  V
) )
7170eqeq2d 2468 . . . . . . . 8  |-  ( v  =  V  ->  (
( X  .-  U
)  =  ( X 
.-  v )  <->  ( X  .-  U )  =  ( X  .-  V ) ) )
72 oveq2 6278 . . . . . . . . 9  |-  ( v  =  V  ->  ( Y  .-  v )  =  ( Y  .-  V
) )
7372eqeq2d 2468 . . . . . . . 8  |-  ( v  =  V  ->  (
( Y  .-  U
)  =  ( Y 
.-  v )  <->  ( Y  .-  U )  =  ( Y  .-  V ) ) )
74 oveq2 6278 . . . . . . . . 9  |-  ( v  =  V  ->  ( Z  .-  v )  =  ( Z  .-  V
) )
7574eqeq2d 2468 . . . . . . . 8  |-  ( v  =  V  ->  (
( Z  .-  U
)  =  ( Z 
.-  v )  <->  ( Z  .-  U )  =  ( Z  .-  V ) ) )
7671, 73, 753anbi123d 1297 . . . . . . 7  |-  ( v  =  V  ->  (
( ( X  .-  U )  =  ( X  .-  v )  /\  ( Y  .-  U )  =  ( Y  .-  v )  /\  ( Z  .-  U )  =  ( Z  .-  v ) )  <->  ( ( X 
.-  U )  =  ( X  .-  V
)  /\  ( Y  .-  U )  =  ( Y  .-  V )  /\  ( Z  .-  U )  =  ( Z  .-  V ) ) ) )
77 neeq2 2737 . . . . . . 7  |-  ( v  =  V  ->  ( U  =/=  v  <->  U  =/=  V ) )
7876, 77anbi12d 708 . . . . . 6  |-  ( v  =  V  ->  (
( ( ( X 
.-  U )  =  ( X  .-  v
)  /\  ( Y  .-  U )  =  ( Y  .-  v )  /\  ( Z  .-  U )  =  ( Z  .-  v ) )  /\  U  =/=  v )  <->  ( (
( X  .-  U
)  =  ( X 
.-  V )  /\  ( Y  .-  U )  =  ( Y  .-  V )  /\  ( Z  .-  U )  =  ( Z  .-  V
) )  /\  U  =/=  V ) ) )
7978imbi1d 315 . . . . 5  |-  ( v  =  V  ->  (
( ( ( ( X  .-  U )  =  ( X  .-  v )  /\  ( Y  .-  U )  =  ( Y  .-  v
)  /\  ( Z  .-  U )  =  ( Z  .-  v ) )  /\  U  =/=  v )  ->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) )  <->  ( (
( ( X  .-  U )  =  ( X  .-  V )  /\  ( Y  .-  U )  =  ( Y  .-  V )  /\  ( Z  .-  U )  =  ( Z  .-  V ) )  /\  U  =/= 
V )  ->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) ) ) )
8069, 79rspc2v 3216 . . . 4  |-  ( ( U  e.  P  /\  V  e.  P )  ->  ( A. u  e.  P  A. v  e.  P  ( ( ( ( X  .-  u
)  =  ( X 
.-  v )  /\  ( Y  .-  u )  =  ( Y  .-  v )  /\  ( Z  .-  u )  =  ( Z  .-  v
) )  /\  u  =/=  v )  ->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) )  -> 
( ( ( ( X  .-  U )  =  ( X  .-  V )  /\  ( Y  .-  U )  =  ( Y  .-  V
)  /\  ( Z  .-  U )  =  ( Z  .-  V ) )  /\  U  =/= 
V )  ->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) ) ) )
8158, 59, 80syl2anc 659 . . 3  |-  ( ph  ->  ( A. u  e.  P  A. v  e.  P  ( ( ( ( X  .-  u
)  =  ( X 
.-  v )  /\  ( Y  .-  u )  =  ( Y  .-  v )  /\  ( Z  .-  u )  =  ( Z  .-  v
) )  /\  u  =/=  v )  ->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) )  -> 
( ( ( ( X  .-  U )  =  ( X  .-  V )  /\  ( Y  .-  U )  =  ( Y  .-  V
)  /\  ( Z  .-  U )  =  ( Z  .-  V ) )  /\  U  =/= 
V )  ->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) ) ) )
8257, 81mpd 15 . 2  |-  ( ph  ->  ( ( ( ( X  .-  U )  =  ( X  .-  V )  /\  ( Y  .-  U )  =  ( Y  .-  V
)  /\  ( Z  .-  U )  =  ( Z  .-  V ) )  /\  U  =/= 
V )  ->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) ) )
834, 5, 82mp2and 677 1  |-  ( ph  ->  ( Z  e.  ( X I Y )  \/  X  e.  ( Z I Y )  \/  Y  e.  ( X I Z ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 367    \/ w3o 970    /\ w3a 971    = wceq 1398    e. wcel 1823    =/= wne 2649   A.wral 2804   E.wrex 2805   _Vcvv 3106   ` cfv 5570  (class class class)co 6270   Basecbs 14719   distcds 14796  TarskiG2Dcstrkg2d 24031  Itvcitv 24033
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-nul 4568
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-iota 5534  df-fv 5578  df-ov 6273  df-trkg2d 24050
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator