Metamath Proof Explorer

Theorem cgrabasimass

Description: The angle congruence relation is hereditary. (Contributed by Thierry Arnoux, 31-Aug-2026)

Ref Expression
Hypotheses cgraer.p 
|- P = ( Base ` G )
cgraer.a 
|- A = { d e. ( P ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) }
cgraer.c 
|- .~ = ( cgrA ` G )
cgraer.g 
|- ( ph -> G e. TarskiG )
Assertion cgrabasimass 
|- ( ph -> ( .~ " A ) C_ A )

Proof

Step Hyp Ref Expression
1 cgraer.p 
 |-  P = ( Base ` G )
2 cgraer.a 
 |-  A = { d e. ( P ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) }
3 cgraer.c 
 |-  .~ = ( cgrA ` G )
4 cgraer.g 
 |-  ( ph -> G e. TarskiG )
5 fveq1 
 |-  ( d = e -> ( d ` 0 ) = ( e ` 0 ) )
6 fveq1 
 |-  ( d = e -> ( d ` 1 ) = ( e ` 1 ) )
7 5 6 neeq12d 
 |-  ( d = e -> ( ( d ` 0 ) =/= ( d ` 1 ) <-> ( e ` 0 ) =/= ( e ` 1 ) ) )
8 fveq1 
 |-  ( d = e -> ( d ` 2 ) = ( e ` 2 ) )
9 6 8 neeq12d 
 |-  ( d = e -> ( ( d ` 1 ) =/= ( d ` 2 ) <-> ( e ` 1 ) =/= ( e ` 2 ) ) )
10 7 9 anbi12d 
 |-  ( d = e -> ( ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) <-> ( ( e ` 0 ) =/= ( e ` 1 ) /\ ( e ` 1 ) =/= ( e ` 2 ) ) ) )
11 imassrn 
 |-  ( .~ " A ) C_ ran .~
12 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 ) ) ) } )
13 fvexd 
 |-  ( g = G -> ( Base ` g ) e. _V )
14 fveq2 
 |-  ( g = G -> ( Base ` g ) = ( Base ` G ) )
15 14 1 eqtr4di 
 |-  ( g = G -> ( Base ` g ) = P )
16 fvexd 
 |-  ( ( g = G /\ p = P ) -> ( hlG ` g ) e. _V )
17 fveq2 
 |-  ( g = G -> ( hlG ` g ) = ( hlG ` G ) )
18 17 adantr 
 |-  ( ( g = G /\ p = P ) -> ( hlG ` g ) = ( hlG ` G ) )
19 oveq1 
 |-  ( p = P -> ( p ^m ( 0 ..^ 3 ) ) = ( P ^m ( 0 ..^ 3 ) ) )
20 19 ad2antlr 
 |-  ( ( ( g = G /\ p = P ) /\ k = ( hlG ` G ) ) -> ( p ^m ( 0 ..^ 3 ) ) = ( P ^m ( 0 ..^ 3 ) ) )
21 20 eleq2d 
 |-  ( ( ( g = G /\ p = P ) /\ k = ( hlG ` G ) ) -> ( a e. ( p ^m ( 0 ..^ 3 ) ) <-> a e. ( P ^m ( 0 ..^ 3 ) ) ) )
22 20 eleq2d 
 |-  ( ( ( g = G /\ p = P ) /\ k = ( hlG ` G ) ) -> ( b e. ( p ^m ( 0 ..^ 3 ) ) <-> b e. ( P ^m ( 0 ..^ 3 ) ) ) )
23 21 22 anbi12d 
 |-  ( ( ( g = G /\ p = P ) /\ k = ( hlG ` G ) ) -> ( ( a e. ( p ^m ( 0 ..^ 3 ) ) /\ b e. ( p ^m ( 0 ..^ 3 ) ) ) <-> ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ b e. ( P ^m ( 0 ..^ 3 ) ) ) ) )
24 simplr 
 |-  ( ( ( g = G /\ p = P ) /\ k = ( hlG ` G ) ) -> p = P )
25 fveq2 
 |-  ( g = G -> ( cgrG ` g ) = ( cgrG ` G ) )
26 25 ad2antrr 
 |-  ( ( ( g = G /\ p = P ) /\ k = ( hlG ` G ) ) -> ( cgrG ` g ) = ( cgrG ` G ) )
27 26 breqd 
 |-  ( ( ( g = G /\ p = P ) /\ k = ( hlG ` G ) ) -> ( a ( cgrG ` g ) <" x ( b ` 1 ) y "> <-> a ( cgrG ` G ) <" x ( b ` 1 ) y "> ) )
28 fveq1 
 |-  ( k = ( hlG ` G ) -> ( k ` ( b ` 1 ) ) = ( ( hlG ` G ) ` ( b ` 1 ) ) )
29 28 adantl 
 |-  ( ( ( g = G /\ p = P ) /\ k = ( hlG ` G ) ) -> ( k ` ( b ` 1 ) ) = ( ( hlG ` G ) ` ( b ` 1 ) ) )
30 29 breqd 
 |-  ( ( ( g = G /\ p = P ) /\ k = ( hlG ` G ) ) -> ( x ( k ` ( b ` 1 ) ) ( b ` 0 ) <-> x ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 0 ) ) )
31 29 breqd 
 |-  ( ( ( g = G /\ p = P ) /\ k = ( hlG ` G ) ) -> ( y ( k ` ( b ` 1 ) ) ( b ` 2 ) <-> y ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 2 ) ) )
32 27 30 31 3anbi123d 
 |-  ( ( ( g = G /\ p = P ) /\ k = ( hlG ` 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 ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 2 ) ) ) )
33 24 32 rexeqbidv 
 |-  ( ( ( g = G /\ p = P ) /\ k = ( hlG ` G ) ) -> ( 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 ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 2 ) ) ) )
34 24 33 rexeqbidv 
 |-  ( ( ( g = G /\ p = P ) /\ k = ( hlG ` 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 ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 2 ) ) ) )
35 23 34 anbi12d 
 |-  ( ( ( g = G /\ p = P ) /\ k = ( hlG ` 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 ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 2 ) ) ) ) )
36 16 18 35 sbcied2 
 |-  ( ( g = G /\ p = 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 ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 2 ) ) ) ) )
37 13 15 36 sbcied2 
 |-  ( 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 ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 2 ) ) ) ) )
38 an21 
 |-  ( ( ( 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 ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 2 ) ) ) <-> ( b e. ( P ^m ( 0 ..^ 3 ) ) /\ ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ E. x e. P E. y e. P ( a ( cgrG ` G ) <" x ( b ` 1 ) y "> /\ x ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 2 ) ) ) ) )
39 37 38 bitrdi 
 |-  ( 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 ) ) ) <-> ( b e. ( P ^m ( 0 ..^ 3 ) ) /\ ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ E. x e. P E. y e. P ( a ( cgrG ` G ) <" x ( b ` 1 ) y "> /\ x ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 2 ) ) ) ) ) )
40 39 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 >. | ( b e. ( P ^m ( 0 ..^ 3 ) ) /\ ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ E. x e. P E. y e. P ( a ( cgrG ` G ) <" x ( b ` 1 ) y "> /\ x ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 2 ) ) ) ) } )
41 4 elexd 
 |-  ( ph -> G e. _V )
42 ovexd 
 |-  ( ph -> ( P ^m ( 0 ..^ 3 ) ) e. _V )
43 simprrl 
 |-  ( ( ph /\ ( b e. ( P ^m ( 0 ..^ 3 ) ) /\ ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ E. x e. P E. y e. P ( a ( cgrG ` G ) <" x ( b ` 1 ) y "> /\ x ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 2 ) ) ) ) ) -> a e. ( P ^m ( 0 ..^ 3 ) ) )
44 simprl 
 |-  ( ( ph /\ ( b e. ( P ^m ( 0 ..^ 3 ) ) /\ ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ E. x e. P E. y e. P ( a ( cgrG ` G ) <" x ( b ` 1 ) y "> /\ x ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 2 ) ) ) ) ) -> b e. ( P ^m ( 0 ..^ 3 ) ) )
45 42 42 43 44 opabex2 
 |-  ( ph -> { <. a , b >. | ( b e. ( P ^m ( 0 ..^ 3 ) ) /\ ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ E. x e. P E. y e. P ( a ( cgrG ` G ) <" x ( b ` 1 ) y "> /\ x ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 2 ) ) ) ) } e. _V )
46 12 40 41 45 fvmptd3 
 |-  ( ph -> ( cgrA ` G ) = { <. a , b >. | ( b e. ( P ^m ( 0 ..^ 3 ) ) /\ ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ E. x e. P E. y e. P ( a ( cgrG ` G ) <" x ( b ` 1 ) y "> /\ x ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 2 ) ) ) ) } )
47 3 46 eqtrid 
 |-  ( ph -> .~ = { <. a , b >. | ( b e. ( P ^m ( 0 ..^ 3 ) ) /\ ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ E. x e. P E. y e. P ( a ( cgrG ` G ) <" x ( b ` 1 ) y "> /\ x ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 2 ) ) ) ) } )
48 47 rneqd 
 |-  ( ph -> ran .~ = ran { <. a , b >. | ( b e. ( P ^m ( 0 ..^ 3 ) ) /\ ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ E. x e. P E. y e. P ( a ( cgrG ` G ) <" x ( b ` 1 ) y "> /\ x ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 2 ) ) ) ) } )
49 rnopabss 
 |-  ran { <. a , b >. | ( b e. ( P ^m ( 0 ..^ 3 ) ) /\ ( a e. ( P ^m ( 0 ..^ 3 ) ) /\ E. x e. P E. y e. P ( a ( cgrG ` G ) <" x ( b ` 1 ) y "> /\ x ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 0 ) /\ y ( ( hlG ` G ) ` ( b ` 1 ) ) ( b ` 2 ) ) ) ) } C_ ( P ^m ( 0 ..^ 3 ) )
50 48 49 eqsstrdi 
 |-  ( ph -> ran .~ C_ ( P ^m ( 0 ..^ 3 ) ) )
51 11 50 sstrid 
 |-  ( ph -> ( .~ " A ) C_ ( P ^m ( 0 ..^ 3 ) ) )
52 51 sselda 
 |-  ( ( ph /\ e e. ( .~ " A ) ) -> e e. ( P ^m ( 0 ..^ 3 ) ) )
53 52 ad10antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) -> e e. ( P ^m ( 0 ..^ 3 ) ) )
54 eqid 
 |-  ( Itv ` G ) = ( Itv ` G )
55 eqid 
 |-  ( hlG ` G ) = ( hlG ` G )
56 4 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) -> G e. TarskiG )
57 56 ad4antr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) -> G e. TarskiG )
58 simp-4r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) -> u e. P )
59 simpllr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) -> v e. P )
60 simplr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) -> w e. P )
61 simp-8r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) -> x e. P )
62 simp-7r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) -> y e. P )
63 simp-6r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) -> z e. P )
64 3 a1i 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) -> .~ = ( cgrA ` G ) )
65 simp-9r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) -> f .~ e )
66 64 65 breqdi 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) -> f ( cgrA ` G ) e )
67 simpr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) -> f = <" u v w "> )
68 simp-5r 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) -> e = <" x y z "> )
69 66 67 68 3brtr3d 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) -> <" u v w "> ( cgrA ` G ) <" x y z "> )
70 1 54 55 57 58 59 60 61 62 63 69 cgrane3 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) -> y =/= x )
71 70 necomd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) -> x =/= y )
72 68 fveq1d 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) -> ( e ` 0 ) = ( <" x y z "> ` 0 ) )
73 s3fv0 
 |-  ( x e. P -> ( <" x y z "> ` 0 ) = x )
74 61 73 syl 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) -> ( <" x y z "> ` 0 ) = x )
75 72 74 eqtrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) -> ( e ` 0 ) = x )
76 68 fveq1d 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) -> ( e ` 1 ) = ( <" x y z "> ` 1 ) )
77 s3fv1 
 |-  ( y e. P -> ( <" x y z "> ` 1 ) = y )
78 77 ad7antlr 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) -> ( <" x y z "> ` 1 ) = y )
79 76 78 eqtrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) -> ( e ` 1 ) = y )
80 71 75 79 3netr4d 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) -> ( e ` 0 ) =/= ( e ` 1 ) )
81 1 54 55 57 58 59 60 61 62 63 69 cgrane4 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) -> y =/= z )
82 68 fveq1d 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) -> ( e ` 2 ) = ( <" x y z "> ` 2 ) )
83 s3fv2 
 |-  ( z e. P -> ( <" x y z "> ` 2 ) = z )
84 63 83 syl 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) -> ( <" x y z "> ` 2 ) = z )
85 82 84 eqtrd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) -> ( e ` 2 ) = z )
86 81 79 85 3netr4d 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) -> ( e ` 1 ) =/= ( e ` 2 ) )
87 80 86 jca 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) -> ( ( e ` 0 ) =/= ( e ` 1 ) /\ ( e ` 1 ) =/= ( e ` 2 ) ) )
88 10 53 87 elrabd 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) -> e e. { d e. ( P ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) } )
89 88 2 eleqtrrdi 
 |-  ( ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ u e. P ) /\ v e. P ) /\ w e. P ) /\ f = <" u v w "> ) -> e e. A )
90 89 r19.29an 
 |-  ( ( ( ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) /\ u e. P ) /\ v e. P ) /\ E. w e. P f = <" u v w "> ) -> e e. A )
91 1 fvexi 
 |-  P e. _V
92 simp-6r 
 |-  ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) -> f e. A )
93 91 2 92 elcgrabasi 
 |-  ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) -> E. u e. P E. v e. P E. w e. P ( f = <" u v w "> /\ ( u =/= v /\ v =/= w ) ) )
94 simpl 
 |-  ( ( f = <" u v w "> /\ ( u =/= v /\ v =/= w ) ) -> f = <" u v w "> )
95 94 reximi 
 |-  ( E. w e. P ( f = <" u v w "> /\ ( u =/= v /\ v =/= w ) ) -> E. w e. P f = <" u v w "> )
96 95 reximi 
 |-  ( E. v e. P E. w e. P ( f = <" u v w "> /\ ( u =/= v /\ v =/= w ) ) -> E. v e. P E. w e. P f = <" u v w "> )
97 96 reximi 
 |-  ( E. u e. P E. v e. P E. w e. P ( f = <" u v w "> /\ ( u =/= v /\ v =/= w ) ) -> E. u e. P E. v e. P E. w e. P f = <" u v w "> )
98 93 97 syl 
 |-  ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) -> E. u e. P E. v e. P E. w e. P f = <" u v w "> )
99 90 98 r19.29vva 
 |-  ( ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ z e. P ) /\ e = <" x y z "> ) -> e e. A )
100 99 r19.29an 
 |-  ( ( ( ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) /\ x e. P ) /\ y e. P ) /\ E. z e. P e = <" x y z "> ) -> e e. A )
101 52 ad2antrr 
 |-  ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) -> e e. ( P ^m ( 0 ..^ 3 ) ) )
102 91 s3rex 
 |-  ( e e. ( P ^m ( 0 ..^ 3 ) ) <-> E. x e. P E. y e. P E. z e. P e = <" x y z "> )
103 101 102 sylib 
 |-  ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) -> E. x e. P E. y e. P E. z e. P e = <" x y z "> )
104 100 103 r19.29vva 
 |-  ( ( ( ( ph /\ e e. ( .~ " A ) ) /\ f e. A ) /\ f .~ e ) -> e e. A )
105 vex 
 |-  e e. _V
106 105 elima 
 |-  ( e e. ( .~ " A ) <-> E. f e. A f .~ e )
107 106 bilani 
 |-  ( ( ph /\ e e. ( .~ " A ) ) -> E. f e. A f .~ e )
108 104 107 r19.29a 
 |-  ( ( ph /\ e e. ( .~ " A ) ) -> e e. A )
109 108 ex 
 |-  ( ph -> ( e e. ( .~ " A ) -> e e. A ) )
110 109 ssrdv 
 |-  ( ph -> ( .~ " A ) C_ A )