Metamath Proof Explorer

Theorem afsval

Description: Value of the AFS relation for a given geometry structure. (Contributed by Thierry Arnoux, 20-Mar-2019)

Ref Expression
Hypotheses brafs.p 
|- P = ( Base ` G )
brafs.d 
|- .- = ( dist ` G )
brafs.i 
|- I = ( Itv ` G )
brafs.g 
|- ( ph -> G e. TarskiG )
Assertion afsval 
|- ( ph -> ( AFS ` G ) = { <. e , f >. | E. a e. P E. b e. P E. c e. P E. d e. P E. x e. P E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a I c ) /\ y e. ( x I z ) ) /\ ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) ) } )

Proof

Step Hyp Ref Expression
1 brafs.p 
 |-  P = ( Base ` G )
2 brafs.d 
 |-  .- = ( dist ` G )
3 brafs.i 
 |-  I = ( Itv ` G )
4 brafs.g 
 |-  ( ph -> G e. TarskiG )
5 df-afs 
 |-  AFS = ( g e. TarskiG |-> { <. e , f >. | [. ( Base ` g ) / p ]. [. ( dist ` g ) / h ]. [. ( Itv ` g ) / i ]. E. a e. p E. b e. p E. c e. p E. d e. p E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) ) } )
6 5 a1i 
 |-  ( ph -> AFS = ( g e. TarskiG |-> { <. e , f >. | [. ( Base ` g ) / p ]. [. ( dist ` g ) / h ]. [. ( Itv ` g ) / i ]. E. a e. p E. b e. p E. c e. p E. d e. p E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) ) } ) )
7 simp1 
 |-  ( ( p = P /\ h = .- /\ i = I ) -> p = P )
8 7 eqcomd 
 |-  ( ( p = P /\ h = .- /\ i = I ) -> P = p )
9 8 adantr 
 |-  ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) -> P = p )
10 9 adantr 
 |-  ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) -> P = p )
11 10 adantr 
 |-  ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) -> P = p )
12 11 adantr 
 |-  ( ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ d e. P ) -> P = p )
13 12 adantr 
 |-  ( ( ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) -> P = p )
14 13 adantr 
 |-  ( ( ( ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) -> P = p )
15 8 ad7antr 
 |-  ( ( ( ( ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) -> P = p )
16 simp3 
 |-  ( ( p = P /\ h = .- /\ i = I ) -> i = I )
17 16 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) -> i = I )
18 17 eqcomd 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) -> I = i )
19 18 oveqd 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) -> ( a I c ) = ( a i c ) )
20 19 eleq2d 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) -> ( b e. ( a I c ) <-> b e. ( a i c ) ) )
21 18 oveqd 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) -> ( x I z ) = ( x i z ) )
22 21 eleq2d 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) -> ( y e. ( x I z ) <-> y e. ( x i z ) ) )
23 20 22 anbi12d 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) -> ( ( b e. ( a I c ) /\ y e. ( x I z ) ) <-> ( b e. ( a i c ) /\ y e. ( x i z ) ) ) )
24 simp2 
 |-  ( ( p = P /\ h = .- /\ i = I ) -> h = .- )
25 24 eqcomd 
 |-  ( ( p = P /\ h = .- /\ i = I ) -> .- = h )
26 25 ad8antr 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) -> .- = h )
27 26 oveqd 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) -> ( a .- b ) = ( a h b ) )
28 26 oveqd 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) -> ( x .- y ) = ( x h y ) )
29 27 28 eqeq12d 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) -> ( ( a .- b ) = ( x .- y ) <-> ( a h b ) = ( x h y ) ) )
30 26 oveqd 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) -> ( b .- c ) = ( b h c ) )
31 26 oveqd 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) -> ( y .- z ) = ( y h z ) )
32 30 31 eqeq12d 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) -> ( ( b .- c ) = ( y .- z ) <-> ( b h c ) = ( y h z ) ) )
33 29 32 anbi12d 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) -> ( ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) <-> ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) ) )
34 26 oveqd 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) -> ( a .- d ) = ( a h d ) )
35 26 oveqd 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) -> ( x .- w ) = ( x h w ) )
36 34 35 eqeq12d 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) -> ( ( a .- d ) = ( x .- w ) <-> ( a h d ) = ( x h w ) ) )
37 26 oveqd 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) -> ( b .- d ) = ( b h d ) )
38 26 oveqd 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) -> ( y .- w ) = ( y h w ) )
39 37 38 eqeq12d 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) -> ( ( b .- d ) = ( y .- w ) <-> ( b h d ) = ( y h w ) ) )
40 36 39 anbi12d 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) -> ( ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) <-> ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) )
41 23 33 40 3anbi123d 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) -> ( ( ( b e. ( a I c ) /\ y e. ( x I z ) ) /\ ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) <-> ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) ) )
42 41 3anbi3d 
 |-  ( ( ( ( ( ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) -> ( ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a I c ) /\ y e. ( x I z ) ) /\ ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) ) <-> ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) ) ) )
43 15 42 rexeqbidva 
 |-  ( ( ( ( ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) -> ( E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a I c ) /\ y e. ( x I z ) ) /\ ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) ) <-> E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) ) ) )
44 14 43 rexeqbidva 
 |-  ( ( ( ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) -> ( E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a I c ) /\ y e. ( x I z ) ) /\ ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) ) <-> E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) ) ) )
45 13 44 rexeqbidva 
 |-  ( ( ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) -> ( E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a I c ) /\ y e. ( x I z ) ) /\ ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) ) <-> E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) ) ) )
46 12 45 rexeqbidva 
 |-  ( ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) /\ d e. P ) -> ( E. x e. P E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a I c ) /\ y e. ( x I z ) ) /\ ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) ) <-> E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) ) ) )
47 11 46 rexeqbidva 
 |-  ( ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) /\ c e. P ) -> ( E. d e. P E. x e. P E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a I c ) /\ y e. ( x I z ) ) /\ ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) ) <-> E. d e. p E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) ) ) )
48 10 47 rexeqbidva 
 |-  ( ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) /\ b e. P ) -> ( E. c e. P E. d e. P E. x e. P E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a I c ) /\ y e. ( x I z ) ) /\ ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) ) <-> E. c e. p E. d e. p E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) ) ) )
49 9 48 rexeqbidva 
 |-  ( ( ( p = P /\ h = .- /\ i = I ) /\ a e. P ) -> ( E. b e. P E. c e. P E. d e. P E. x e. P E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a I c ) /\ y e. ( x I z ) ) /\ ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) ) <-> E. b e. p E. c e. p E. d e. p E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) ) ) )
50 8 49 rexeqbidva 
 |-  ( ( p = P /\ h = .- /\ i = I ) -> ( E. a e. P E. b e. P E. c e. P E. d e. P E. x e. P E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a I c ) /\ y e. ( x I z ) ) /\ ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) ) <-> E. a e. p E. b e. p E. c e. p E. d e. p E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) ) ) )
51 1 2 3 50 sbcie3s 
 |-  ( g = G -> ( [. ( Base ` g ) / p ]. [. ( dist ` g ) / h ]. [. ( Itv ` g ) / i ]. E. a e. p E. b e. p E. c e. p E. d e. p E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) ) <-> E. a e. P E. b e. P E. c e. P E. d e. P E. x e. P E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a I c ) /\ y e. ( x I z ) ) /\ ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) ) ) )
52 51 adantl 
 |-  ( ( ph /\ g = G ) -> ( [. ( Base ` g ) / p ]. [. ( dist ` g ) / h ]. [. ( Itv ` g ) / i ]. E. a e. p E. b e. p E. c e. p E. d e. p E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) ) <-> E. a e. P E. b e. P E. c e. P E. d e. P E. x e. P E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a I c ) /\ y e. ( x I z ) ) /\ ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) ) ) )
53 52 opabbidv 
 |-  ( ( ph /\ g = G ) -> { <. e , f >. | [. ( Base ` g ) / p ]. [. ( dist ` g ) / h ]. [. ( Itv ` g ) / i ]. E. a e. p E. b e. p E. c e. p E. d e. p E. x e. p E. y e. p E. z e. p E. w e. p ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a i c ) /\ y e. ( x i z ) ) /\ ( ( a h b ) = ( x h y ) /\ ( b h c ) = ( y h z ) ) /\ ( ( a h d ) = ( x h w ) /\ ( b h d ) = ( y h w ) ) ) ) } = { <. e , f >. | E. a e. P E. b e. P E. c e. P E. d e. P E. x e. P E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a I c ) /\ y e. ( x I z ) ) /\ ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) ) } )
54 df-xp 
 |-  ( ( ( P X. P ) X. ( P X. P ) ) X. ( ( P X. P ) X. ( P X. P ) ) ) = { <. e , f >. | ( e e. ( ( P X. P ) X. ( P X. P ) ) /\ f e. ( ( P X. P ) X. ( P X. P ) ) ) }
55 1 fvexi 
 |-  P e. _V
56 55 55 xpex 
 |-  ( P X. P ) e. _V
57 56 56 xpex 
 |-  ( ( P X. P ) X. ( P X. P ) ) e. _V
58 57 57 xpex 
 |-  ( ( ( P X. P ) X. ( P X. P ) ) X. ( ( P X. P ) X. ( P X. P ) ) ) e. _V
59 54 58 eqeltrri 
 |-  { <. e , f >. | ( e e. ( ( P X. P ) X. ( P X. P ) ) /\ f e. ( ( P X. P ) X. ( P X. P ) ) ) } e. _V
60 3simpa 
 |-  ( ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a I c ) /\ y e. ( x I z ) ) /\ ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) ) -> ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. ) )
61 60 reximi 
 |-  ( E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a I c ) /\ y e. ( x I z ) ) /\ ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) ) -> E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. ) )
62 61 reximi 
 |-  ( E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a I c ) /\ y e. ( x I z ) ) /\ ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) ) -> E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. ) )
63 62 reximi 
 |-  ( E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a I c ) /\ y e. ( x I z ) ) /\ ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) ) -> E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. ) )
64 63 reximi 
 |-  ( E. x e. P E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a I c ) /\ y e. ( x I z ) ) /\ ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) ) -> E. x e. P E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. ) )
65 64 reximi 
 |-  ( E. d e. P E. x e. P E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a I c ) /\ y e. ( x I z ) ) /\ ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) ) -> E. d e. P E. x e. P E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. ) )
66 65 reximi 
 |-  ( E. c e. P E. d e. P E. x e. P E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a I c ) /\ y e. ( x I z ) ) /\ ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) ) -> E. c e. P E. d e. P E. x e. P E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. ) )
67 66 reximi 
 |-  ( E. b e. P E. c e. P E. d e. P E. x e. P E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a I c ) /\ y e. ( x I z ) ) /\ ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) ) -> E. b e. P E. c e. P E. d e. P E. x e. P E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. ) )
68 67 reximi 
 |-  ( E. a e. P E. b e. P E. c e. P E. d e. P E. x e. P E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a I c ) /\ y e. ( x I z ) ) /\ ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) ) -> E. a e. P E. b e. P E. c e. P E. d e. P E. x e. P E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. ) )
69 simpr 
 |-  ( ( ( ( ( ( ( ( ( a e. P /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) /\ e = <. <. a , b >. , <. c , d >. >. ) -> e = <. <. a , b >. , <. c , d >. >. )
70 opelxpi 
 |-  ( ( a e. P /\ b e. P ) -> <. a , b >. e. ( P X. P ) )
71 70 ad7antr 
 |-  ( ( ( ( ( ( ( ( ( a e. P /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) /\ e = <. <. a , b >. , <. c , d >. >. ) -> <. a , b >. e. ( P X. P ) )
72 simp-7r 
 |-  ( ( ( ( ( ( ( ( ( a e. P /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) /\ e = <. <. a , b >. , <. c , d >. >. ) -> c e. P )
73 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( a e. P /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) /\ e = <. <. a , b >. , <. c , d >. >. ) -> d e. P )
74 opelxpi 
 |-  ( ( c e. P /\ d e. P ) -> <. c , d >. e. ( P X. P ) )
75 72 73 74 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( a e. P /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) /\ e = <. <. a , b >. , <. c , d >. >. ) -> <. c , d >. e. ( P X. P ) )
76 opelxpi 
 |-  ( ( <. a , b >. e. ( P X. P ) /\ <. c , d >. e. ( P X. P ) ) -> <. <. a , b >. , <. c , d >. >. e. ( ( P X. P ) X. ( P X. P ) ) )
77 71 75 76 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( a e. P /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) /\ e = <. <. a , b >. , <. c , d >. >. ) -> <. <. a , b >. , <. c , d >. >. e. ( ( P X. P ) X. ( P X. P ) ) )
78 69 77 eqeltrd 
 |-  ( ( ( ( ( ( ( ( ( a e. P /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) /\ e = <. <. a , b >. , <. c , d >. >. ) -> e e. ( ( P X. P ) X. ( P X. P ) ) )
79 simpr 
 |-  ( ( ( ( ( ( ( ( ( a e. P /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) /\ f = <. <. x , y >. , <. z , w >. >. ) -> f = <. <. x , y >. , <. z , w >. >. )
80 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( a e. P /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) /\ f = <. <. x , y >. , <. z , w >. >. ) -> x e. P )
81 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( a e. P /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) /\ f = <. <. x , y >. , <. z , w >. >. ) -> y e. P )
82 opelxpi 
 |-  ( ( x e. P /\ y e. P ) -> <. x , y >. e. ( P X. P ) )
83 80 81 82 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( a e. P /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) /\ f = <. <. x , y >. , <. z , w >. >. ) -> <. x , y >. e. ( P X. P ) )
84 simpllr 
 |-  ( ( ( ( ( ( ( ( ( a e. P /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) /\ f = <. <. x , y >. , <. z , w >. >. ) -> z e. P )
85 simplr 
 |-  ( ( ( ( ( ( ( ( ( a e. P /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) /\ f = <. <. x , y >. , <. z , w >. >. ) -> w e. P )
86 opelxpi 
 |-  ( ( z e. P /\ w e. P ) -> <. z , w >. e. ( P X. P ) )
87 84 85 86 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( a e. P /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) /\ f = <. <. x , y >. , <. z , w >. >. ) -> <. z , w >. e. ( P X. P ) )
88 opelxpi 
 |-  ( ( <. x , y >. e. ( P X. P ) /\ <. z , w >. e. ( P X. P ) ) -> <. <. x , y >. , <. z , w >. >. e. ( ( P X. P ) X. ( P X. P ) ) )
89 83 87 88 syl2anc 
 |-  ( ( ( ( ( ( ( ( ( a e. P /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) /\ f = <. <. x , y >. , <. z , w >. >. ) -> <. <. x , y >. , <. z , w >. >. e. ( ( P X. P ) X. ( P X. P ) ) )
90 79 89 eqeltrd 
 |-  ( ( ( ( ( ( ( ( ( a e. P /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) /\ f = <. <. x , y >. , <. z , w >. >. ) -> f e. ( ( P X. P ) X. ( P X. P ) ) )
91 78 90 anim12dan 
 |-  ( ( ( ( ( ( ( ( ( a e. P /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ w e. P ) /\ ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. ) ) -> ( e e. ( ( P X. P ) X. ( P X. P ) ) /\ f e. ( ( P X. P ) X. ( P X. P ) ) ) )
92 91 rexlimdva2 
 |-  ( ( ( ( ( ( ( a e. P /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) /\ z e. P ) -> ( E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. ) -> ( e e. ( ( P X. P ) X. ( P X. P ) ) /\ f e. ( ( P X. P ) X. ( P X. P ) ) ) ) )
93 92 rexlimdva 
 |-  ( ( ( ( ( ( a e. P /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) /\ y e. P ) -> ( E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. ) -> ( e e. ( ( P X. P ) X. ( P X. P ) ) /\ f e. ( ( P X. P ) X. ( P X. P ) ) ) ) )
94 93 rexlimdva 
 |-  ( ( ( ( ( a e. P /\ b e. P ) /\ c e. P ) /\ d e. P ) /\ x e. P ) -> ( E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. ) -> ( e e. ( ( P X. P ) X. ( P X. P ) ) /\ f e. ( ( P X. P ) X. ( P X. P ) ) ) ) )
95 94 rexlimdva 
 |-  ( ( ( ( a e. P /\ b e. P ) /\ c e. P ) /\ d e. P ) -> ( E. x e. P E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. ) -> ( e e. ( ( P X. P ) X. ( P X. P ) ) /\ f e. ( ( P X. P ) X. ( P X. P ) ) ) ) )
96 95 rexlimdva 
 |-  ( ( ( a e. P /\ b e. P ) /\ c e. P ) -> ( E. d e. P E. x e. P E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. ) -> ( e e. ( ( P X. P ) X. ( P X. P ) ) /\ f e. ( ( P X. P ) X. ( P X. P ) ) ) ) )
97 96 rexlimdva 
 |-  ( ( a e. P /\ b e. P ) -> ( E. c e. P E. d e. P E. x e. P E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. ) -> ( e e. ( ( P X. P ) X. ( P X. P ) ) /\ f e. ( ( P X. P ) X. ( P X. P ) ) ) ) )
98 97 rexlimivv 
 |-  ( E. a e. P E. b e. P E. c e. P E. d e. P E. x e. P E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. ) -> ( e e. ( ( P X. P ) X. ( P X. P ) ) /\ f e. ( ( P X. P ) X. ( P X. P ) ) ) )
99 68 98 syl 
 |-  ( E. a e. P E. b e. P E. c e. P E. d e. P E. x e. P E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a I c ) /\ y e. ( x I z ) ) /\ ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) ) -> ( e e. ( ( P X. P ) X. ( P X. P ) ) /\ f e. ( ( P X. P ) X. ( P X. P ) ) ) )
100 99 ssopab2i 
 |-  { <. e , f >. | E. a e. P E. b e. P E. c e. P E. d e. P E. x e. P E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a I c ) /\ y e. ( x I z ) ) /\ ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) ) } C_ { <. e , f >. | ( e e. ( ( P X. P ) X. ( P X. P ) ) /\ f e. ( ( P X. P ) X. ( P X. P ) ) ) }
101 59 100 ssexi 
 |-  { <. e , f >. | E. a e. P E. b e. P E. c e. P E. d e. P E. x e. P E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a I c ) /\ y e. ( x I z ) ) /\ ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) ) } e. _V
102 101 a1i 
 |-  ( ph -> { <. e , f >. | E. a e. P E. b e. P E. c e. P E. d e. P E. x e. P E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a I c ) /\ y e. ( x I z ) ) /\ ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) ) } e. _V )
103 6 53 4 102 fvmptd 
 |-  ( ph -> ( AFS ` G ) = { <. e , f >. | E. a e. P E. b e. P E. c e. P E. d e. P E. x e. P E. y e. P E. z e. P E. w e. P ( e = <. <. a , b >. , <. c , d >. >. /\ f = <. <. x , y >. , <. z , w >. >. /\ ( ( b e. ( a I c ) /\ y e. ( x I z ) ) /\ ( ( a .- b ) = ( x .- y ) /\ ( b .- c ) = ( y .- z ) ) /\ ( ( a .- d ) = ( x .- w ) /\ ( b .- d ) = ( y .- w ) ) ) ) } )