Metamath Proof Explorer

Theorem iscgra

Description: Property for two angles ABC and DEF to be congruent. This is a modified version of the definition 11.3 of Schwabhauser p. 95. where the number of constructed points has been reduced to two. We chose this version rather than the textbook version because it is shorter and therefore simpler to work with. Theorem dfcgra2 shows that those definitions are indeed equivalent. (Contributed by Thierry Arnoux, 31-Jul-2020)

Ref Expression
Hypotheses iscgra.p 
|- P = ( Base ` G )
iscgra.i 
|- I = ( Itv ` G )
iscgra.k 
|- K = ( hlG ` G )
iscgra.g 
|- ( ph -> G e. TarskiG )
iscgra.a 
|- ( ph -> A e. P )
iscgra.b 
|- ( ph -> B e. P )
iscgra.c 
|- ( ph -> C e. P )
iscgra.d 
|- ( ph -> D e. P )
iscgra.e 
|- ( ph -> E e. P )
iscgra.f 
|- ( ph -> F e. P )
Assertion iscgra 
|- ( ph -> ( <" A B C "> ( cgrA ` G ) <" D E F "> <-> E. x e. P E. y e. P ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) )

Proof

Step Hyp Ref Expression
1 iscgra.p 
 |-  P = ( Base ` G )
2 iscgra.i 
 |-  I = ( Itv ` G )
3 iscgra.k 
 |-  K = ( hlG ` G )
4 iscgra.g 
 |-  ( ph -> G e. TarskiG )
5 iscgra.a 
 |-  ( ph -> A e. P )
6 iscgra.b 
 |-  ( ph -> B e. P )
7 iscgra.c 
 |-  ( ph -> C e. P )
8 iscgra.d 
 |-  ( ph -> D e. P )
9 iscgra.e 
 |-  ( ph -> E e. P )
10 iscgra.f 
 |-  ( ph -> F e. P )
11 simpl 
 |-  ( ( a = <" A B C "> /\ b = <" D E F "> ) -> a = <" A B C "> )
12 eqidd 
 |-  ( ( a = <" A B C "> /\ b = <" D E F "> ) -> x = x )
13 simpr 
 |-  ( ( a = <" A B C "> /\ b = <" D E F "> ) -> b = <" D E F "> )
14 13 fveq1d 
 |-  ( ( a = <" A B C "> /\ b = <" D E F "> ) -> ( b ` 1 ) = ( <" D E F "> ` 1 ) )
15 eqidd 
 |-  ( ( a = <" A B C "> /\ b = <" D E F "> ) -> y = y )
16 12 14 15 s3eqd 
 |-  ( ( a = <" A B C "> /\ b = <" D E F "> ) -> <" x ( b ` 1 ) y "> = <" x ( <" D E F "> ` 1 ) y "> )
17 11 16 breq12d 
 |-  ( ( a = <" A B C "> /\ b = <" D E F "> ) -> ( a ( cgrG ` G ) <" x ( b ` 1 ) y "> <-> <" A B C "> ( cgrG ` G ) <" x ( <" D E F "> ` 1 ) y "> ) )
18 14 fveq2d 
 |-  ( ( a = <" A B C "> /\ b = <" D E F "> ) -> ( K ` ( b ` 1 ) ) = ( K ` ( <" D E F "> ` 1 ) ) )
19 13 fveq1d 
 |-  ( ( a = <" A B C "> /\ b = <" D E F "> ) -> ( b ` 0 ) = ( <" D E F "> ` 0 ) )
20 12 18 19 breq123d 
 |-  ( ( a = <" A B C "> /\ b = <" D E F "> ) -> ( x ( K ` ( b ` 1 ) ) ( b ` 0 ) <-> x ( K ` ( <" D E F "> ` 1 ) ) ( <" D E F "> ` 0 ) ) )
21 13 fveq1d 
 |-  ( ( a = <" A B C "> /\ b = <" D E F "> ) -> ( b ` 2 ) = ( <" D E F "> ` 2 ) )
22 15 18 21 breq123d 
 |-  ( ( a = <" A B C "> /\ b = <" D E F "> ) -> ( y ( K ` ( b ` 1 ) ) ( b ` 2 ) <-> y ( K ` ( <" D E F "> ` 1 ) ) ( <" D E F "> ` 2 ) ) )
23 17 20 22 3anbi123d 
 |-  ( ( a = <" A B C "> /\ b = <" D E F "> ) -> ( ( a ( cgrG ` G ) <" x ( b ` 1 ) y "> /\ x ( K ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( K ` ( b ` 1 ) ) ( b ` 2 ) ) <-> ( <" A B C "> ( cgrG ` G ) <" x ( <" D E F "> ` 1 ) y "> /\ x ( K ` ( <" D E F "> ` 1 ) ) ( <" D E F "> ` 0 ) /\ y ( K ` ( <" D E F "> ` 1 ) ) ( <" D E F "> ` 2 ) ) ) )
24 23 2rexbidv 
 |-  ( ( a = <" A B C "> /\ b = <" D E F "> ) -> ( E. x e. P E. y e. P ( a ( cgrG ` G ) <" x ( b ` 1 ) y "> /\ x ( K ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( K ` ( b ` 1 ) ) ( b ` 2 ) ) <-> E. x e. P E. y e. P ( <" A B C "> ( cgrG ` G ) <" x ( <" D E F "> ` 1 ) y "> /\ x ( K ` ( <" D E F "> ` 1 ) ) ( <" D E F "> ` 0 ) /\ y ( K ` ( <" D E F "> ` 1 ) ) ( <" D E F "> ` 2 ) ) ) )
25 eqid 
 |-  { <. a , b >. | ( ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ b e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P E. y e. P ( a ( cgrG ` G ) <" x ( b ` 1 ) y "> /\ x ( K ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( K ` ( b ` 1 ) ) ( b ` 2 ) ) ) } = { <. a , b >. | ( ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ b e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P E. y e. P ( a ( cgrG ` G ) <" x ( b ` 1 ) y "> /\ x ( K ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( K ` ( b ` 1 ) ) ( b ` 2 ) ) ) }
26 24 25 brab2a 
 |-  ( <" A B C "> { <. a , b >. | ( ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ b e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P E. y e. P ( a ( cgrG ` G ) <" x ( b ` 1 ) y "> /\ x ( K ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( K ` ( b ` 1 ) ) ( b ` 2 ) ) ) } <" D E F "> <-> ( ( <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) /\ <" D E F "> e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P E. y e. P ( <" A B C "> ( cgrG ` G ) <" x ( <" D E F "> ` 1 ) y "> /\ x ( K ` ( <" D E F "> ` 1 ) ) ( <" D E F "> ` 0 ) /\ y ( K ` ( <" D E F "> ` 1 ) ) ( <" D E F "> ` 2 ) ) ) )
27 eqidd 
 |-  ( ( ph /\ ( x e. P /\ y e. P ) ) -> x = x )
28 s3fv1 
 |-  ( E e. P -> ( <" D E F "> ` 1 ) = E )
29 9 28 syl 
 |-  ( ph -> ( <" D E F "> ` 1 ) = E )
30 29 adantr 
 |-  ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( <" D E F "> ` 1 ) = E )
31 eqidd 
 |-  ( ( ph /\ ( x e. P /\ y e. P ) ) -> y = y )
32 27 30 31 s3eqd 
 |-  ( ( ph /\ ( x e. P /\ y e. P ) ) -> <" x ( <" D E F "> ` 1 ) y "> = <" x E y "> )
33 32 breq2d 
 |-  ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( <" A B C "> ( cgrG ` G ) <" x ( <" D E F "> ` 1 ) y "> <-> <" A B C "> ( cgrG ` G ) <" x E y "> ) )
34 30 fveq2d 
 |-  ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( K ` ( <" D E F "> ` 1 ) ) = ( K ` E ) )
35 s3fv0 
 |-  ( D e. P -> ( <" D E F "> ` 0 ) = D )
36 8 35 syl 
 |-  ( ph -> ( <" D E F "> ` 0 ) = D )
37 36 adantr 
 |-  ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( <" D E F "> ` 0 ) = D )
38 27 34 37 breq123d 
 |-  ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( x ( K ` ( <" D E F "> ` 1 ) ) ( <" D E F "> ` 0 ) <-> x ( K ` E ) D ) )
39 s3fv2 
 |-  ( F e. P -> ( <" D E F "> ` 2 ) = F )
40 10 39 syl 
 |-  ( ph -> ( <" D E F "> ` 2 ) = F )
41 40 adantr 
 |-  ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( <" D E F "> ` 2 ) = F )
42 31 34 41 breq123d 
 |-  ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( y ( K ` ( <" D E F "> ` 1 ) ) ( <" D E F "> ` 2 ) <-> y ( K ` E ) F ) )
43 33 38 42 3anbi123d 
 |-  ( ( ph /\ ( x e. P /\ y e. P ) ) -> ( ( <" A B C "> ( cgrG ` G ) <" x ( <" D E F "> ` 1 ) y "> /\ x ( K ` ( <" D E F "> ` 1 ) ) ( <" D E F "> ` 0 ) /\ y ( K ` ( <" D E F "> ` 1 ) ) ( <" D E F "> ` 2 ) ) <-> ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) )
44 43 2rexbidva 
 |-  ( ph -> ( E. x e. P E. y e. P ( <" A B C "> ( cgrG ` G ) <" x ( <" D E F "> ` 1 ) y "> /\ x ( K ` ( <" D E F "> ` 1 ) ) ( <" D E F "> ` 0 ) /\ y ( K ` ( <" D E F "> ` 1 ) ) ( <" D E F "> ` 2 ) ) <-> E. x e. P E. y e. P ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) )
45 44 anbi2d 
 |-  ( ph -> ( ( ( <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) /\ <" D E F "> e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P E. y e. P ( <" A B C "> ( cgrG ` G ) <" x ( <" D E F "> ` 1 ) y "> /\ x ( K ` ( <" D E F "> ` 1 ) ) ( <" D E F "> ` 0 ) /\ y ( K ` ( <" D E F "> ` 1 ) ) ( <" D E F "> ` 2 ) ) ) <-> ( ( <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) /\ <" D E F "> e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P E. y e. P ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) ) )
46 26 45 syl5bb 
 |-  ( ph -> ( <" A B C "> { <. a , b >. | ( ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ b e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P E. y e. P ( a ( cgrG ` G ) <" x ( b ` 1 ) y "> /\ x ( K ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( K ` ( b ` 1 ) ) ( b ` 2 ) ) ) } <" D E F "> <-> ( ( <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) /\ <" D E F "> e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P E. y e. P ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) ) )
47 elex 
 |-  ( G e. TarskiG -> G e. _V )
48 simpl 
 |-  ( ( p = P /\ k = K ) -> p = P )
49 48 eqcomd 
 |-  ( ( p = P /\ k = K ) -> P = p )
50 49 oveq1d 
 |-  ( ( p = P /\ k = K ) -> ( P ^m ( 0 ..^ 3 ) ) = ( p ^m ( 0 ..^ 3 ) ) )
51 50 eleq2d 
 |-  ( ( p = P /\ k = K ) -> ( a e. ( P ^m ( 0 ..^ 3 ) ) <-> a e. ( p ^m ( 0 ..^ 3 ) ) ) )
52 50 eleq2d 
 |-  ( ( p = P /\ k = K ) -> ( b e. ( P ^m ( 0 ..^ 3 ) ) <-> b e. ( p ^m ( 0 ..^ 3 ) ) ) )
53 51 52 anbi12d 
 |-  ( ( p = P /\ k = K ) -> ( ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ b e. ( P ^m ( 0 ..^ 3 ) ) ) <-> ( a e. ( p ^m ( 0 ..^ 3 ) ) /\ b e. ( p ^m ( 0 ..^ 3 ) ) ) ) )
54 simpr 
 |-  ( ( p = P /\ k = K ) -> k = K )
55 54 fveq1d 
 |-  ( ( p = P /\ k = K ) -> ( k ` ( b ` 1 ) ) = ( K ` ( b ` 1 ) ) )
56 55 breqd 
 |-  ( ( p = P /\ k = K ) -> ( x ( k ` ( b ` 1 ) ) ( b ` 0 ) <-> x ( K ` ( b ` 1 ) ) ( b ` 0 ) ) )
57 55 breqd 
 |-  ( ( p = P /\ k = K ) -> ( y ( k ` ( b ` 1 ) ) ( b ` 2 ) <-> y ( K ` ( b ` 1 ) ) ( b ` 2 ) ) )
58 56 57 3anbi23d 
 |-  ( ( p = P /\ k = K ) -> ( ( a ( cgrG ` g ) <" x ( b ` 1 ) y "> /\ x ( k ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( k ` ( b ` 1 ) ) ( b ` 2 ) ) <-> ( a ( cgrG ` g ) <" x ( b ` 1 ) y "> /\ x ( K ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( K ` ( b ` 1 ) ) ( b ` 2 ) ) ) )
59 58 bicomd 
 |-  ( ( p = P /\ k = K ) -> ( ( a ( cgrG ` g ) <" x ( b ` 1 ) y "> /\ x ( K ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( K ` ( b ` 1 ) ) ( b ` 2 ) ) <-> ( a ( cgrG ` g ) <" x ( b ` 1 ) y "> /\ x ( k ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( k ` ( b ` 1 ) ) ( b ` 2 ) ) ) )
60 49 59 rexeqbidv 
 |-  ( ( p = P /\ k = K ) -> ( E. y e. P ( a ( cgrG ` g ) <" x ( b ` 1 ) y "> /\ x ( K ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( K ` ( b ` 1 ) ) ( b ` 2 ) ) <-> E. y e. p ( a ( cgrG ` g ) <" x ( b ` 1 ) y "> /\ x ( k ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( k ` ( b ` 1 ) ) ( b ` 2 ) ) ) )
61 49 60 rexeqbidv 
 |-  ( ( p = P /\ k = K ) -> ( E. x e. P E. y e. P ( a ( cgrG ` g ) <" x ( b ` 1 ) y "> /\ x ( K ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( K ` ( b ` 1 ) ) ( b ` 2 ) ) <-> E. x e. p E. y e. p ( a ( cgrG ` g ) <" x ( b ` 1 ) y "> /\ x ( k ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( k ` ( b ` 1 ) ) ( b ` 2 ) ) ) )
62 53 61 anbi12d 
 |-  ( ( p = P /\ k = K ) -> ( ( ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ b e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P E. y e. P ( a ( cgrG ` g ) <" x ( b ` 1 ) y "> /\ x ( K ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( K ` ( b ` 1 ) ) ( b ` 2 ) ) ) <-> ( ( a e. ( p ^m ( 0 ..^ 3 ) ) /\ b e. ( p ^m ( 0 ..^ 3 ) ) ) /\ E. x e. p E. y e. p ( a ( cgrG ` g ) <" x ( b ` 1 ) y "> /\ x ( k ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( k ` ( b ` 1 ) ) ( b ` 2 ) ) ) ) )
63 1 3 62 sbcie2s 
 |-  ( g = G -> ( [. ( Base ` g ) / p ]. [. ( hlG ` g ) / k ]. ( ( a e. ( p ^m ( 0 ..^ 3 ) ) /\ b e. ( p ^m ( 0 ..^ 3 ) ) ) /\ E. x e. p E. y e. p ( a ( cgrG ` g ) <" x ( b ` 1 ) y "> /\ x ( k ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( k ` ( b ` 1 ) ) ( b ` 2 ) ) ) <-> ( ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ b e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P E. y e. P ( a ( cgrG ` g ) <" x ( b ` 1 ) y "> /\ x ( K ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( K ` ( b ` 1 ) ) ( b ` 2 ) ) ) ) )
64 63 opabbidv 
 |-  ( g = G -> { <. a , b >. | [. ( Base ` g ) / p ]. [. ( hlG ` g ) / k ]. ( ( a e. ( p ^m ( 0 ..^ 3 ) ) /\ b e. ( p ^m ( 0 ..^ 3 ) ) ) /\ E. x e. p E. y e. p ( a ( cgrG ` g ) <" x ( b ` 1 ) y "> /\ x ( k ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( k ` ( b ` 1 ) ) ( b ` 2 ) ) ) } = { <. a , b >. | ( ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ b e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P E. y e. P ( a ( cgrG ` g ) <" x ( b ` 1 ) y "> /\ x ( K ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( K ` ( b ` 1 ) ) ( b ` 2 ) ) ) } )
65 fveq2 
 |-  ( g = G -> ( cgrG ` g ) = ( cgrG ` G ) )
66 65 breqd 
 |-  ( g = G -> ( a ( cgrG ` g ) <" x ( b ` 1 ) y "> <-> a ( cgrG ` G ) <" x ( b ` 1 ) y "> ) )
67 66 3anbi1d 
 |-  ( g = G -> ( ( a ( cgrG ` g ) <" x ( b ` 1 ) y "> /\ x ( K ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( K ` ( b ` 1 ) ) ( b ` 2 ) ) <-> ( a ( cgrG ` G ) <" x ( b ` 1 ) y "> /\ x ( K ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( K ` ( b ` 1 ) ) ( b ` 2 ) ) ) )
68 67 2rexbidv 
 |-  ( g = G -> ( E. x e. P E. y e. P ( a ( cgrG ` g ) <" x ( b ` 1 ) y "> /\ x ( K ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( K ` ( b ` 1 ) ) ( b ` 2 ) ) <-> E. x e. P E. y e. P ( a ( cgrG ` G ) <" x ( b ` 1 ) y "> /\ x ( K ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( K ` ( b ` 1 ) ) ( b ` 2 ) ) ) )
69 68 anbi2d 
 |-  ( g = G -> ( ( ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ b e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P E. y e. P ( a ( cgrG ` g ) <" x ( b ` 1 ) y "> /\ x ( K ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( K ` ( b ` 1 ) ) ( b ` 2 ) ) ) <-> ( ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ b e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P E. y e. P ( a ( cgrG ` G ) <" x ( b ` 1 ) y "> /\ x ( K ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( K ` ( b ` 1 ) ) ( b ` 2 ) ) ) ) )
70 69 opabbidv 
 |-  ( g = G -> { <. a , b >. | ( ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ b e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P E. y e. P ( a ( cgrG ` g ) <" x ( b ` 1 ) y "> /\ x ( K ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( K ` ( b ` 1 ) ) ( b ` 2 ) ) ) } = { <. a , b >. | ( ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ b e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P E. y e. P ( a ( cgrG ` G ) <" x ( b ` 1 ) y "> /\ x ( K ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( K ` ( b ` 1 ) ) ( b ` 2 ) ) ) } )
71 64 70 eqtrd 
 |-  ( g = G -> { <. a , b >. | [. ( Base ` g ) / p ]. [. ( hlG ` g ) / k ]. ( ( a e. ( p ^m ( 0 ..^ 3 ) ) /\ b e. ( p ^m ( 0 ..^ 3 ) ) ) /\ E. x e. p E. y e. p ( a ( cgrG ` g ) <" x ( b ` 1 ) y "> /\ x ( k ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( k ` ( b ` 1 ) ) ( b ` 2 ) ) ) } = { <. a , b >. | ( ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ b e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P E. y e. P ( a ( cgrG ` G ) <" x ( b ` 1 ) y "> /\ x ( K ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( K ` ( b ` 1 ) ) ( b ` 2 ) ) ) } )
72 df-cgra 
 |-  cgrA = ( g e. _V |-> { <. a , b >. | [. ( Base ` g ) / p ]. [. ( hlG ` g ) / k ]. ( ( a e. ( p ^m ( 0 ..^ 3 ) ) /\ b e. ( p ^m ( 0 ..^ 3 ) ) ) /\ E. x e. p E. y e. p ( a ( cgrG ` g ) <" x ( b ` 1 ) y "> /\ x ( k ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( k ` ( b ` 1 ) ) ( b ` 2 ) ) ) } )
73 ovex 
 |-  ( P ^m ( 0 ..^ 3 ) ) e. _V
74 73 73 xpex 
 |-  ( ( P ^m ( 0 ..^ 3 ) ) X. ( P ^m ( 0 ..^ 3 ) ) ) e. _V
75 opabssxp 
 |-  { <. a , b >. | ( ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ b e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P E. y e. P ( a ( cgrG ` G ) <" x ( b ` 1 ) y "> /\ x ( K ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( K ` ( b ` 1 ) ) ( b ` 2 ) ) ) } C_ ( ( P ^m ( 0 ..^ 3 ) ) X. ( P ^m ( 0 ..^ 3 ) ) )
76 74 75 ssexi 
 |-  { <. a , b >. | ( ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ b e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P E. y e. P ( a ( cgrG ` G ) <" x ( b ` 1 ) y "> /\ x ( K ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( K ` ( b ` 1 ) ) ( b ` 2 ) ) ) } e. _V
77 71 72 76 fvmpt 
 |-  ( G e. _V -> ( cgrA ` G ) = { <. a , b >. | ( ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ b e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P E. y e. P ( a ( cgrG ` G ) <" x ( b ` 1 ) y "> /\ x ( K ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( K ` ( b ` 1 ) ) ( b ` 2 ) ) ) } )
78 4 47 77 3syl 
 |-  ( ph -> ( cgrA ` G ) = { <. a , b >. | ( ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ b e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P E. y e. P ( a ( cgrG ` G ) <" x ( b ` 1 ) y "> /\ x ( K ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( K ` ( b ` 1 ) ) ( b ` 2 ) ) ) } )
79 78 breqd 
 |-  ( ph -> ( <" A B C "> ( cgrA ` G ) <" D E F "> <-> <" A B C "> { <. a , b >. | ( ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ b e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P E. y e. P ( a ( cgrG ` G ) <" x ( b ` 1 ) y "> /\ x ( K ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( K ` ( b ` 1 ) ) ( b ` 2 ) ) ) } <" D E F "> ) )
80 5 6 7 s3cld 
 |-  ( ph -> <" A B C "> e. Word P )
81 s3len 
 |-  ( # ` <" A B C "> ) = 3
82 1 fvexi 
 |-  P e. _V
83 3nn0 
 |-  3 e. NN0
84 wrdmap 
 |-  ( ( P e. _V /\ 3 e. NN0 ) -> ( ( <" A B C "> e. Word P /\ ( # ` <" A B C "> ) = 3 ) <-> <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) ) )
85 82 83 84 mp2an 
 |-  ( ( <" A B C "> e. Word P /\ ( # ` <" A B C "> ) = 3 ) <-> <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) )
86 80 81 85 sylanblc 
 |-  ( ph -> <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) )
87 8 9 10 s3cld 
 |-  ( ph -> <" D E F "> e. Word P )
88 s3len 
 |-  ( # ` <" D E F "> ) = 3
89 wrdmap 
 |-  ( ( P e. _V /\ 3 e. NN0 ) -> ( ( <" D E F "> e. Word P /\ ( # ` <" D E F "> ) = 3 ) <-> <" D E F "> e. ( P ^m ( 0 ..^ 3 ) ) ) )
90 82 83 89 mp2an 
 |-  ( ( <" D E F "> e. Word P /\ ( # ` <" D E F "> ) = 3 ) <-> <" D E F "> e. ( P ^m ( 0 ..^ 3 ) ) )
91 87 88 90 sylanblc 
 |-  ( ph -> <" D E F "> e. ( P ^m ( 0 ..^ 3 ) ) )
92 86 91 jca 
 |-  ( ph -> ( <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) /\ <" D E F "> e. ( P ^m ( 0 ..^ 3 ) ) ) )
93 92 biantrurd 
 |-  ( ph -> ( E. x e. P E. y e. P ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) <-> ( ( <" A B C "> e. ( P ^m ( 0 ..^ 3 ) ) /\ <" D E F "> e. ( P ^m ( 0 ..^ 3 ) ) ) /\ E. x e. P E. y e. P ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) ) )
94 46 79 93 3bitr4d 
 |-  ( ph -> ( <" A B C "> ( cgrA ` G ) <" D E F "> <-> E. x e. P E. y e. P ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) )