Metamath Proof Explorer

Theorem elcgrabasi

Description: Helper theorem for the membership in the base set of the angle addition monoid. (Contributed by Thierry Arnoux, 23-Aug-2026)

Ref Expression
Hypotheses elcgrabasi.1 
|- P e. _V
elcgrabasi.2 
|- A = { d e. ( P ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) }
elcgrabasi.3 
|- ( ph -> E e. A )
Assertion elcgrabasi 
|- ( ph -> E. x e. P E. y e. P E. z e. P ( E = <" x y z "> /\ ( x =/= y /\ y =/= z ) ) )

Proof

Step Hyp Ref Expression
1 elcgrabasi.1 
 |-  P e. _V
2 elcgrabasi.2 
 |-  A = { d e. ( P ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) }
3 elcgrabasi.3 
 |-  ( ph -> E e. A )
4 id 
 |-  ( x = ( E ` 0 ) -> x = ( E ` 0 ) )
5 eqidd 
 |-  ( x = ( E ` 0 ) -> y = y )
6 eqidd 
 |-  ( x = ( E ` 0 ) -> z = z )
7 4 5 6 s3eqd 
 |-  ( x = ( E ` 0 ) -> <" x y z "> = <" ( E ` 0 ) y z "> )
8 7 eqeq2d 
 |-  ( x = ( E ` 0 ) -> ( E = <" x y z "> <-> E = <" ( E ` 0 ) y z "> ) )
9 4 neeq1d 
 |-  ( x = ( E ` 0 ) -> ( x =/= y <-> ( E ` 0 ) =/= y ) )
10 9 anbi1d 
 |-  ( x = ( E ` 0 ) -> ( ( x =/= y /\ y =/= z ) <-> ( ( E ` 0 ) =/= y /\ y =/= z ) ) )
11 8 10 anbi12d 
 |-  ( x = ( E ` 0 ) -> ( ( E = <" x y z "> /\ ( x =/= y /\ y =/= z ) ) <-> ( E = <" ( E ` 0 ) y z "> /\ ( ( E ` 0 ) =/= y /\ y =/= z ) ) ) )
12 s3eq2 
 |-  ( y = ( E ` 1 ) -> <" ( E ` 0 ) y z "> = <" ( E ` 0 ) ( E ` 1 ) z "> )
13 12 eqeq2d 
 |-  ( y = ( E ` 1 ) -> ( E = <" ( E ` 0 ) y z "> <-> E = <" ( E ` 0 ) ( E ` 1 ) z "> ) )
14 neeq2 
 |-  ( y = ( E ` 1 ) -> ( ( E ` 0 ) =/= y <-> ( E ` 0 ) =/= ( E ` 1 ) ) )
15 neeq1 
 |-  ( y = ( E ` 1 ) -> ( y =/= z <-> ( E ` 1 ) =/= z ) )
16 14 15 anbi12d 
 |-  ( y = ( E ` 1 ) -> ( ( ( E ` 0 ) =/= y /\ y =/= z ) <-> ( ( E ` 0 ) =/= ( E ` 1 ) /\ ( E ` 1 ) =/= z ) ) )
17 13 16 anbi12d 
 |-  ( y = ( E ` 1 ) -> ( ( E = <" ( E ` 0 ) y z "> /\ ( ( E ` 0 ) =/= y /\ y =/= z ) ) <-> ( E = <" ( E ` 0 ) ( E ` 1 ) z "> /\ ( ( E ` 0 ) =/= ( E ` 1 ) /\ ( E ` 1 ) =/= z ) ) ) )
18 eqidd 
 |-  ( z = ( E ` 2 ) -> ( E ` 0 ) = ( E ` 0 ) )
19 eqidd 
 |-  ( z = ( E ` 2 ) -> ( E ` 1 ) = ( E ` 1 ) )
20 id 
 |-  ( z = ( E ` 2 ) -> z = ( E ` 2 ) )
21 18 19 20 s3eqd 
 |-  ( z = ( E ` 2 ) -> <" ( E ` 0 ) ( E ` 1 ) z "> = <" ( E ` 0 ) ( E ` 1 ) ( E ` 2 ) "> )
22 21 eqeq2d 
 |-  ( z = ( E ` 2 ) -> ( E = <" ( E ` 0 ) ( E ` 1 ) z "> <-> E = <" ( E ` 0 ) ( E ` 1 ) ( E ` 2 ) "> ) )
23 biidd 
 |-  ( z = ( E ` 2 ) -> ( ( E ` 0 ) =/= ( E ` 1 ) <-> ( E ` 0 ) =/= ( E ` 1 ) ) )
24 20 neeq2d 
 |-  ( z = ( E ` 2 ) -> ( ( E ` 1 ) =/= z <-> ( E ` 1 ) =/= ( E ` 2 ) ) )
25 23 24 anbi12d 
 |-  ( z = ( E ` 2 ) -> ( ( ( E ` 0 ) =/= ( E ` 1 ) /\ ( E ` 1 ) =/= z ) <-> ( ( E ` 0 ) =/= ( E ` 1 ) /\ ( E ` 1 ) =/= ( E ` 2 ) ) ) )
26 22 25 anbi12d 
 |-  ( z = ( E ` 2 ) -> ( ( E = <" ( E ` 0 ) ( E ` 1 ) z "> /\ ( ( E ` 0 ) =/= ( E ` 1 ) /\ ( E ` 1 ) =/= z ) ) <-> ( E = <" ( E ` 0 ) ( E ` 1 ) ( E ` 2 ) "> /\ ( ( E ` 0 ) =/= ( E ` 1 ) /\ ( E ` 1 ) =/= ( E ` 2 ) ) ) ) )
27 fzo0to3tp 
 |-  ( 0 ..^ 3 ) = { 0 , 1 , 2 }
28 27 a1i 
 |-  ( ph -> ( 0 ..^ 3 ) = { 0 , 1 , 2 } )
29 2 ssrab3 
 |-  A C_ ( P ^m ( 0 ..^ 3 ) )
30 29 3 sselid 
 |-  ( ph -> E e. ( P ^m ( 0 ..^ 3 ) ) )
31 30 elmaprd 
 |-  ( ph -> E : ( 0 ..^ 3 ) --> P )
32 28 31 feq2dd 
 |-  ( ph -> E : { 0 , 1 , 2 } --> P )
33 c0ex 
 |-  0 e. _V
34 33 tpid1 
 |-  0 e. { 0 , 1 , 2 }
35 34 a1i 
 |-  ( ph -> 0 e. { 0 , 1 , 2 } )
36 32 35 ffvelcdmd 
 |-  ( ph -> ( E ` 0 ) e. P )
37 1eltp012 
 |-  1 e. { 0 , 1 , 2 }
38 37 a1i 
 |-  ( ph -> 1 e. { 0 , 1 , 2 } )
39 32 38 ffvelcdmd 
 |-  ( ph -> ( E ` 1 ) e. P )
40 2ex 
 |-  2 e. _V
41 40 tpid3 
 |-  2 e. { 0 , 1 , 2 }
42 41 a1i 
 |-  ( ph -> 2 e. { 0 , 1 , 2 } )
43 32 42 ffvelcdmd 
 |-  ( ph -> ( E ` 2 ) e. P )
44 iswrdi 
 |-  ( E : ( 0 ..^ 3 ) --> P -> E e. Word P )
45 31 44 syl 
 |-  ( ph -> E e. Word P )
46 31 ffnd 
 |-  ( ph -> E Fn ( 0 ..^ 3 ) )
47 hashfn 
 |-  ( E Fn ( 0 ..^ 3 ) -> ( # ` E ) = ( # ` ( 0 ..^ 3 ) ) )
48 46 47 syl 
 |-  ( ph -> ( # ` E ) = ( # ` ( 0 ..^ 3 ) ) )
49 3nn0 
 |-  3 e. NN0
50 hashfzo0 
 |-  ( 3 e. NN0 -> ( # ` ( 0 ..^ 3 ) ) = 3 )
51 49 50 ax-mp 
 |-  ( # ` ( 0 ..^ 3 ) ) = 3
52 48 51 eqtrdi 
 |-  ( ph -> ( # ` E ) = 3 )
53 wrdlen3s3 
 |-  ( ( E e. Word P /\ ( # ` E ) = 3 ) -> E = <" ( E ` 0 ) ( E ` 1 ) ( E ` 2 ) "> )
54 45 52 53 syl2anc 
 |-  ( ph -> E = <" ( E ` 0 ) ( E ` 1 ) ( E ` 2 ) "> )
55 fveq1 
 |-  ( d = E -> ( d ` 0 ) = ( E ` 0 ) )
56 fveq1 
 |-  ( d = E -> ( d ` 1 ) = ( E ` 1 ) )
57 55 56 neeq12d 
 |-  ( d = E -> ( ( d ` 0 ) =/= ( d ` 1 ) <-> ( E ` 0 ) =/= ( E ` 1 ) ) )
58 fveq1 
 |-  ( d = E -> ( d ` 2 ) = ( E ` 2 ) )
59 56 58 neeq12d 
 |-  ( d = E -> ( ( d ` 1 ) =/= ( d ` 2 ) <-> ( E ` 1 ) =/= ( E ` 2 ) ) )
60 57 59 anbi12d 
 |-  ( d = E -> ( ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) <-> ( ( E ` 0 ) =/= ( E ` 1 ) /\ ( E ` 1 ) =/= ( E ` 2 ) ) ) )
61 2 eleq2i 
 |-  ( E e. A <-> E e. { d e. ( P ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) } )
62 3 61 sylib 
 |-  ( ph -> E e. { d e. ( P ^m ( 0 ..^ 3 ) ) | ( ( d ` 0 ) =/= ( d ` 1 ) /\ ( d ` 1 ) =/= ( d ` 2 ) ) } )
63 60 62 elrabrd 
 |-  ( ph -> ( ( E ` 0 ) =/= ( E ` 1 ) /\ ( E ` 1 ) =/= ( E ` 2 ) ) )
64 54 63 jca 
 |-  ( ph -> ( E = <" ( E ` 0 ) ( E ` 1 ) ( E ` 2 ) "> /\ ( ( E ` 0 ) =/= ( E ` 1 ) /\ ( E ` 1 ) =/= ( E ` 2 ) ) ) )
65 11 17 26 36 39 43 64 3rspcedvdw 
 |-  ( ph -> E. x e. P E. y e. P E. z e. P ( E = <" x y z "> /\ ( x =/= y /\ y =/= z ) ) )