Metamath Proof Explorer

Theorem gpgprismgr4cycllem3

Description: Lemma 3 for gpgprismgr4cycl0 . (Contributed by AV, 5-Nov-2025)

Ref Expression
Hypothesis gpgprismgr4cycllem1.f 
|- F = <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } ">
Assertion gpgprismgr4cycllem3 
|- ( ( N e. ( ZZ>= ` 3 ) /\ X e. ( 0 ..^ 4 ) ) -> ( ( F ` X ) e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )

Proof

Step Hyp Ref Expression
1 gpgprismgr4cycllem1.f 
 |-  F = <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } ">
2 fzo0to42pr 
 |-  ( 0 ..^ 4 ) = ( { 0 , 1 } u. { 2 , 3 } )
3 2 eleq2i 
 |-  ( X e. ( 0 ..^ 4 ) <-> X e. ( { 0 , 1 } u. { 2 , 3 } ) )
4 elun 
 |-  ( X e. ( { 0 , 1 } u. { 2 , 3 } ) <-> ( X e. { 0 , 1 } \/ X e. { 2 , 3 } ) )
5 3 4 bitri 
 |-  ( X e. ( 0 ..^ 4 ) <-> ( X e. { 0 , 1 } \/ X e. { 2 , 3 } ) )
6 elpri 
 |-  ( X e. { 0 , 1 } -> ( X = 0 \/ X = 1 ) )
7 0elpr01 
 |-  0 e. { 0 , 1 }
8 7 a1i 
 |-  ( N e. ( ZZ>= ` 3 ) -> 0 e. { 0 , 1 } )
9 eluz3nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. NN )
10 lbfzo0 
 |-  ( 0 e. ( 0 ..^ N ) <-> N e. NN )
11 9 10 sylibr 
 |-  ( N e. ( ZZ>= ` 3 ) -> 0 e. ( 0 ..^ N ) )
12 8 11 opelxpd 
 |-  ( N e. ( ZZ>= ` 3 ) -> <. 0 , 0 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) )
13 1nn0 
 |-  1 e. NN0
14 13 a1i 
 |-  ( N e. ( ZZ>= ` 3 ) -> 1 e. NN0 )
15 uzuzle23 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ( ZZ>= ` 2 ) )
16 eluz2gt1 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 < N )
17 15 16 syl 
 |-  ( N e. ( ZZ>= ` 3 ) -> 1 < N )
18 elfzo0 
 |-  ( 1 e. ( 0 ..^ N ) <-> ( 1 e. NN0 /\ N e. NN /\ 1 < N ) )
19 14 9 17 18 syl3anbrc 
 |-  ( N e. ( ZZ>= ` 3 ) -> 1 e. ( 0 ..^ N ) )
20 8 19 opelxpd 
 |-  ( N e. ( ZZ>= ` 3 ) -> <. 0 , 1 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) )
21 prelpwi 
 |-  ( ( <. 0 , 0 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ <. 0 , 1 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) -> { <. 0 , 0 >. , <. 0 , 1 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) )
22 12 20 21 syl2anc 
 |-  ( N e. ( ZZ>= ` 3 ) -> { <. 0 , 0 >. , <. 0 , 1 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) )
23 opeq2 
 |-  ( x = 0 -> <. 0 , x >. = <. 0 , 0 >. )
24 oveq1 
 |-  ( x = 0 -> ( x + 1 ) = ( 0 + 1 ) )
25 24 oveq1d 
 |-  ( x = 0 -> ( ( x + 1 ) mod N ) = ( ( 0 + 1 ) mod N ) )
26 25 opeq2d 
 |-  ( x = 0 -> <. 0 , ( ( x + 1 ) mod N ) >. = <. 0 , ( ( 0 + 1 ) mod N ) >. )
27 23 26 preq12d 
 |-  ( x = 0 -> { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } = { <. 0 , 0 >. , <. 0 , ( ( 0 + 1 ) mod N ) >. } )
28 27 eqeq2d 
 |-  ( x = 0 -> ( { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } <-> { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , 0 >. , <. 0 , ( ( 0 + 1 ) mod N ) >. } ) )
29 opeq2 
 |-  ( x = 0 -> <. 1 , x >. = <. 1 , 0 >. )
30 23 29 preq12d 
 |-  ( x = 0 -> { <. 0 , x >. , <. 1 , x >. } = { <. 0 , 0 >. , <. 1 , 0 >. } )
31 30 eqeq2d 
 |-  ( x = 0 -> ( { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } <-> { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , 0 >. , <. 1 , 0 >. } ) )
32 25 opeq2d 
 |-  ( x = 0 -> <. 1 , ( ( x + 1 ) mod N ) >. = <. 1 , ( ( 0 + 1 ) mod N ) >. )
33 29 32 preq12d 
 |-  ( x = 0 -> { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod N ) >. } )
34 33 eqeq2d 
 |-  ( x = 0 -> ( { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } <-> { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod N ) >. } ) )
35 28 31 34 3orbi123d 
 |-  ( x = 0 -> ( ( { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) <-> ( { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , 0 >. , <. 0 , ( ( 0 + 1 ) mod N ) >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , 0 >. , <. 1 , 0 >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod N ) >. } ) ) )
36 eluzelre 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. RR )
37 1mod 
 |-  ( ( N e. RR /\ 1 < N ) -> ( 1 mod N ) = 1 )
38 36 17 37 syl2anc 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( 1 mod N ) = 1 )
39 1e0p1 
 |-  1 = ( 0 + 1 )
40 39 oveq1i 
 |-  ( 1 mod N ) = ( ( 0 + 1 ) mod N )
41 38 40 eqtr3di 
 |-  ( N e. ( ZZ>= ` 3 ) -> 1 = ( ( 0 + 1 ) mod N ) )
42 41 opeq2d 
 |-  ( N e. ( ZZ>= ` 3 ) -> <. 0 , 1 >. = <. 0 , ( ( 0 + 1 ) mod N ) >. )
43 42 preq2d 
 |-  ( N e. ( ZZ>= ` 3 ) -> { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , 0 >. , <. 0 , ( ( 0 + 1 ) mod N ) >. } )
44 43 3mix1d 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , 0 >. , <. 0 , ( ( 0 + 1 ) mod N ) >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , 0 >. , <. 1 , 0 >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod N ) >. } ) )
45 35 11 44 rspcedvdw 
 |-  ( N e. ( ZZ>= ` 3 ) -> E. x e. ( 0 ..^ N ) ( { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) )
46 22 45 jca 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( { <. 0 , 0 >. , <. 0 , 1 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )
47 fveq2 
 |-  ( X = 0 -> ( F ` X ) = ( F ` 0 ) )
48 1 fveq1i 
 |-  ( F ` 0 ) = ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ` 0 )
49 prex 
 |-  { <. 0 , 0 >. , <. 0 , 1 >. } e. _V
50 s4fv0 
 |-  ( { <. 0 , 0 >. , <. 0 , 1 >. } e. _V -> ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ` 0 ) = { <. 0 , 0 >. , <. 0 , 1 >. } )
51 49 50 ax-mp 
 |-  ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ` 0 ) = { <. 0 , 0 >. , <. 0 , 1 >. }
52 48 51 eqtri 
 |-  ( F ` 0 ) = { <. 0 , 0 >. , <. 0 , 1 >. }
53 47 52 eqtrdi 
 |-  ( X = 0 -> ( F ` X ) = { <. 0 , 0 >. , <. 0 , 1 >. } )
54 53 eleq1d 
 |-  ( X = 0 -> ( ( F ` X ) e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) <-> { <. 0 , 0 >. , <. 0 , 1 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) ) )
55 53 eqeq1d 
 |-  ( X = 0 -> ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } <-> { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } ) )
56 53 eqeq1d 
 |-  ( X = 0 -> ( ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } <-> { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } ) )
57 53 eqeq1d 
 |-  ( X = 0 -> ( ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } <-> { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) )
58 55 56 57 3orbi123d 
 |-  ( X = 0 -> ( ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) <-> ( { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )
59 58 rexbidv 
 |-  ( X = 0 -> ( E. x e. ( 0 ..^ N ) ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) <-> E. x e. ( 0 ..^ N ) ( { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )
60 54 59 anbi12d 
 |-  ( X = 0 -> ( ( ( F ` X ) e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) <-> ( { <. 0 , 0 >. , <. 0 , 1 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) ) )
61 46 60 imbitrrid 
 |-  ( X = 0 -> ( N e. ( ZZ>= ` 3 ) -> ( ( F ` X ) e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) ) )
62 1elpr01 
 |-  1 e. { 0 , 1 }
63 62 a1i 
 |-  ( N e. ( ZZ>= ` 3 ) -> 1 e. { 0 , 1 } )
64 63 19 opelxpd 
 |-  ( N e. ( ZZ>= ` 3 ) -> <. 1 , 1 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) )
65 prelpwi 
 |-  ( ( <. 0 , 1 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ <. 1 , 1 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) -> { <. 0 , 1 >. , <. 1 , 1 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) )
66 20 64 65 syl2anc 
 |-  ( N e. ( ZZ>= ` 3 ) -> { <. 0 , 1 >. , <. 1 , 1 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) )
67 opeq2 
 |-  ( x = 1 -> <. 0 , x >. = <. 0 , 1 >. )
68 oveq1 
 |-  ( x = 1 -> ( x + 1 ) = ( 1 + 1 ) )
69 68 oveq1d 
 |-  ( x = 1 -> ( ( x + 1 ) mod N ) = ( ( 1 + 1 ) mod N ) )
70 69 opeq2d 
 |-  ( x = 1 -> <. 0 , ( ( x + 1 ) mod N ) >. = <. 0 , ( ( 1 + 1 ) mod N ) >. )
71 67 70 preq12d 
 |-  ( x = 1 -> { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } = { <. 0 , 1 >. , <. 0 , ( ( 1 + 1 ) mod N ) >. } )
72 71 eqeq2d 
 |-  ( x = 1 -> ( { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } <-> { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , 1 >. , <. 0 , ( ( 1 + 1 ) mod N ) >. } ) )
73 opeq2 
 |-  ( x = 1 -> <. 1 , x >. = <. 1 , 1 >. )
74 67 73 preq12d 
 |-  ( x = 1 -> { <. 0 , x >. , <. 1 , x >. } = { <. 0 , 1 >. , <. 1 , 1 >. } )
75 74 eqeq2d 
 |-  ( x = 1 -> ( { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } <-> { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , 1 >. , <. 1 , 1 >. } ) )
76 69 opeq2d 
 |-  ( x = 1 -> <. 1 , ( ( x + 1 ) mod N ) >. = <. 1 , ( ( 1 + 1 ) mod N ) >. )
77 73 76 preq12d 
 |-  ( x = 1 -> { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } = { <. 1 , 1 >. , <. 1 , ( ( 1 + 1 ) mod N ) >. } )
78 77 eqeq2d 
 |-  ( x = 1 -> ( { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } <-> { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 1 , 1 >. , <. 1 , ( ( 1 + 1 ) mod N ) >. } ) )
79 72 75 78 3orbi123d 
 |-  ( x = 1 -> ( ( { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) <-> ( { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , 1 >. , <. 0 , ( ( 1 + 1 ) mod N ) >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , 1 >. , <. 1 , 1 >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 1 , 1 >. , <. 1 , ( ( 1 + 1 ) mod N ) >. } ) ) )
80 eqid 
 |-  { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , 1 >. , <. 1 , 1 >. }
81 80 3mix2i 
 |-  ( { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , 1 >. , <. 0 , ( ( 1 + 1 ) mod N ) >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , 1 >. , <. 1 , 1 >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 1 , 1 >. , <. 1 , ( ( 1 + 1 ) mod N ) >. } )
82 81 a1i 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , 1 >. , <. 0 , ( ( 1 + 1 ) mod N ) >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , 1 >. , <. 1 , 1 >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 1 , 1 >. , <. 1 , ( ( 1 + 1 ) mod N ) >. } ) )
83 79 19 82 rspcedvdw 
 |-  ( N e. ( ZZ>= ` 3 ) -> E. x e. ( 0 ..^ N ) ( { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) )
84 66 83 jca 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( { <. 0 , 1 >. , <. 1 , 1 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )
85 fveq2 
 |-  ( X = 1 -> ( F ` X ) = ( F ` 1 ) )
86 1 fveq1i 
 |-  ( F ` 1 ) = ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ` 1 )
87 prex 
 |-  { <. 0 , 1 >. , <. 1 , 1 >. } e. _V
88 s4fv1 
 |-  ( { <. 0 , 1 >. , <. 1 , 1 >. } e. _V -> ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ` 1 ) = { <. 0 , 1 >. , <. 1 , 1 >. } )
89 87 88 ax-mp 
 |-  ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ` 1 ) = { <. 0 , 1 >. , <. 1 , 1 >. }
90 86 89 eqtri 
 |-  ( F ` 1 ) = { <. 0 , 1 >. , <. 1 , 1 >. }
91 85 90 eqtrdi 
 |-  ( X = 1 -> ( F ` X ) = { <. 0 , 1 >. , <. 1 , 1 >. } )
92 91 eleq1d 
 |-  ( X = 1 -> ( ( F ` X ) e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) <-> { <. 0 , 1 >. , <. 1 , 1 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) ) )
93 91 eqeq1d 
 |-  ( X = 1 -> ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } <-> { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } ) )
94 91 eqeq1d 
 |-  ( X = 1 -> ( ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } <-> { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } ) )
95 91 eqeq1d 
 |-  ( X = 1 -> ( ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } <-> { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) )
96 93 94 95 3orbi123d 
 |-  ( X = 1 -> ( ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) <-> ( { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )
97 96 rexbidv 
 |-  ( X = 1 -> ( E. x e. ( 0 ..^ N ) ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) <-> E. x e. ( 0 ..^ N ) ( { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )
98 92 97 anbi12d 
 |-  ( X = 1 -> ( ( ( F ` X ) e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) <-> ( { <. 0 , 1 >. , <. 1 , 1 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , 1 >. , <. 1 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) ) )
99 84 98 imbitrrid 
 |-  ( X = 1 -> ( N e. ( ZZ>= ` 3 ) -> ( ( F ` X ) e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) ) )
100 61 99 jaoi 
 |-  ( ( X = 0 \/ X = 1 ) -> ( N e. ( ZZ>= ` 3 ) -> ( ( F ` X ) e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) ) )
101 6 100 syl 
 |-  ( X e. { 0 , 1 } -> ( N e. ( ZZ>= ` 3 ) -> ( ( F ` X ) e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) ) )
102 elpri 
 |-  ( X e. { 2 , 3 } -> ( X = 2 \/ X = 3 ) )
103 63 11 opelxpd 
 |-  ( N e. ( ZZ>= ` 3 ) -> <. 1 , 0 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) )
104 64 103 jca 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( <. 1 , 1 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ <. 1 , 0 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) )
105 104 adantr 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ X = 2 ) -> ( <. 1 , 1 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ <. 1 , 0 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) )
106 prelpwi 
 |-  ( ( <. 1 , 1 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ <. 1 , 0 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) -> { <. 1 , 1 >. , <. 1 , 0 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) )
107 105 106 syl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ X = 2 ) -> { <. 1 , 1 >. , <. 1 , 0 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) )
108 27 eqeq2d 
 |-  ( x = 0 -> ( { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } <-> { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , 0 >. , <. 0 , ( ( 0 + 1 ) mod N ) >. } ) )
109 30 eqeq2d 
 |-  ( x = 0 -> ( { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } <-> { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , 0 >. , <. 1 , 0 >. } ) )
110 33 eqeq2d 
 |-  ( x = 0 -> ( { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } <-> { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod N ) >. } ) )
111 108 109 110 3orbi123d 
 |-  ( x = 0 -> ( ( { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) <-> ( { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , 0 >. , <. 0 , ( ( 0 + 1 ) mod N ) >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , 0 >. , <. 1 , 0 >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod N ) >. } ) ) )
112 prcom 
 |-  { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , 0 >. , <. 1 , 1 >. }
113 41 opeq2d 
 |-  ( N e. ( ZZ>= ` 3 ) -> <. 1 , 1 >. = <. 1 , ( ( 0 + 1 ) mod N ) >. )
114 113 preq2d 
 |-  ( N e. ( ZZ>= ` 3 ) -> { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod N ) >. } )
115 112 114 eqtrid 
 |-  ( N e. ( ZZ>= ` 3 ) -> { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod N ) >. } )
116 115 3mix3d 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , 0 >. , <. 0 , ( ( 0 + 1 ) mod N ) >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , 0 >. , <. 1 , 0 >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod N ) >. } ) )
117 111 11 116 rspcedvdw 
 |-  ( N e. ( ZZ>= ` 3 ) -> E. x e. ( 0 ..^ N ) ( { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) )
118 117 adantr 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ X = 2 ) -> E. x e. ( 0 ..^ N ) ( { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) )
119 107 118 jca 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ X = 2 ) -> ( { <. 1 , 1 >. , <. 1 , 0 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )
120 fveq2 
 |-  ( X = 2 -> ( F ` X ) = ( F ` 2 ) )
121 1 fveq1i 
 |-  ( F ` 2 ) = ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ` 2 )
122 prex 
 |-  { <. 1 , 1 >. , <. 1 , 0 >. } e. _V
123 s4fv2 
 |-  ( { <. 1 , 1 >. , <. 1 , 0 >. } e. _V -> ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ` 2 ) = { <. 1 , 1 >. , <. 1 , 0 >. } )
124 122 123 ax-mp 
 |-  ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ` 2 ) = { <. 1 , 1 >. , <. 1 , 0 >. }
125 121 124 eqtri 
 |-  ( F ` 2 ) = { <. 1 , 1 >. , <. 1 , 0 >. }
126 120 125 eqtrdi 
 |-  ( X = 2 -> ( F ` X ) = { <. 1 , 1 >. , <. 1 , 0 >. } )
127 126 eleq1d 
 |-  ( X = 2 -> ( ( F ` X ) e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) <-> { <. 1 , 1 >. , <. 1 , 0 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) ) )
128 126 eqeq1d 
 |-  ( X = 2 -> ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } <-> { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } ) )
129 126 eqeq1d 
 |-  ( X = 2 -> ( ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } <-> { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } ) )
130 126 eqeq1d 
 |-  ( X = 2 -> ( ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } <-> { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) )
131 128 129 130 3orbi123d 
 |-  ( X = 2 -> ( ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) <-> ( { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )
132 131 rexbidv 
 |-  ( X = 2 -> ( E. x e. ( 0 ..^ N ) ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) <-> E. x e. ( 0 ..^ N ) ( { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )
133 127 132 anbi12d 
 |-  ( X = 2 -> ( ( ( F ` X ) e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) <-> ( { <. 1 , 1 >. , <. 1 , 0 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) ) )
134 133 adantl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ X = 2 ) -> ( ( ( F ` X ) e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) <-> ( { <. 1 , 1 >. , <. 1 , 0 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) ) )
135 119 134 mpbird 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ X = 2 ) -> ( ( F ` X ) e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )
136 135 expcom 
 |-  ( X = 2 -> ( N e. ( ZZ>= ` 3 ) -> ( ( F ` X ) e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) ) )
137 prelpwi 
 |-  ( ( <. 1 , 0 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ <. 0 , 0 >. e. ( { 0 , 1 } X. ( 0 ..^ N ) ) ) -> { <. 1 , 0 >. , <. 0 , 0 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) )
138 103 12 137 syl2anc 
 |-  ( N e. ( ZZ>= ` 3 ) -> { <. 1 , 0 >. , <. 0 , 0 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) )
139 27 eqeq2d 
 |-  ( x = 0 -> ( { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } <-> { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , 0 >. , <. 0 , ( ( 0 + 1 ) mod N ) >. } ) )
140 30 eqeq2d 
 |-  ( x = 0 -> ( { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } <-> { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , 0 >. , <. 1 , 0 >. } ) )
141 33 eqeq2d 
 |-  ( x = 0 -> ( { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } <-> { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod N ) >. } ) )
142 139 140 141 3orbi123d 
 |-  ( x = 0 -> ( ( { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) <-> ( { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , 0 >. , <. 0 , ( ( 0 + 1 ) mod N ) >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , 0 >. , <. 1 , 0 >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod N ) >. } ) ) )
143 prcom 
 |-  { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , 0 >. , <. 1 , 0 >. }
144 143 3mix2i 
 |-  ( { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , 0 >. , <. 0 , ( ( 0 + 1 ) mod N ) >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , 0 >. , <. 1 , 0 >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod N ) >. } )
145 144 a1i 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , 0 >. , <. 0 , ( ( 0 + 1 ) mod N ) >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , 0 >. , <. 1 , 0 >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 1 , 0 >. , <. 1 , ( ( 0 + 1 ) mod N ) >. } ) )
146 142 11 145 rspcedvdw 
 |-  ( N e. ( ZZ>= ` 3 ) -> E. x e. ( 0 ..^ N ) ( { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) )
147 138 146 jca 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( { <. 1 , 0 >. , <. 0 , 0 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )
148 fveq2 
 |-  ( X = 3 -> ( F ` X ) = ( F ` 3 ) )
149 1 fveq1i 
 |-  ( F ` 3 ) = ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ` 3 )
150 prex 
 |-  { <. 1 , 0 >. , <. 0 , 0 >. } e. _V
151 s4fv3 
 |-  ( { <. 1 , 0 >. , <. 0 , 0 >. } e. _V -> ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ` 3 ) = { <. 1 , 0 >. , <. 0 , 0 >. } )
152 150 151 ax-mp 
 |-  ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> ` 3 ) = { <. 1 , 0 >. , <. 0 , 0 >. }
153 149 152 eqtri 
 |-  ( F ` 3 ) = { <. 1 , 0 >. , <. 0 , 0 >. }
154 148 153 eqtrdi 
 |-  ( X = 3 -> ( F ` X ) = { <. 1 , 0 >. , <. 0 , 0 >. } )
155 154 eleq1d 
 |-  ( X = 3 -> ( ( F ` X ) e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) <-> { <. 1 , 0 >. , <. 0 , 0 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) ) )
156 154 eqeq1d 
 |-  ( X = 3 -> ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } <-> { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } ) )
157 154 eqeq1d 
 |-  ( X = 3 -> ( ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } <-> { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } ) )
158 154 eqeq1d 
 |-  ( X = 3 -> ( ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } <-> { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) )
159 156 157 158 3orbi123d 
 |-  ( X = 3 -> ( ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) <-> ( { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )
160 159 rexbidv 
 |-  ( X = 3 -> ( E. x e. ( 0 ..^ N ) ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) <-> E. x e. ( 0 ..^ N ) ( { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )
161 155 160 anbi12d 
 |-  ( X = 3 -> ( ( ( F ` X ) e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) <-> ( { <. 1 , 0 >. , <. 0 , 0 >. } e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) ) )
162 147 161 imbitrrid 
 |-  ( X = 3 -> ( N e. ( ZZ>= ` 3 ) -> ( ( F ` X ) e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) ) )
163 136 162 jaoi 
 |-  ( ( X = 2 \/ X = 3 ) -> ( N e. ( ZZ>= ` 3 ) -> ( ( F ` X ) e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) ) )
164 102 163 syl 
 |-  ( X e. { 2 , 3 } -> ( N e. ( ZZ>= ` 3 ) -> ( ( F ` X ) e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) ) )
165 101 164 jaoi 
 |-  ( ( X e. { 0 , 1 } \/ X e. { 2 , 3 } ) -> ( N e. ( ZZ>= ` 3 ) -> ( ( F ` X ) e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) ) )
166 5 165 sylbi 
 |-  ( X e. ( 0 ..^ 4 ) -> ( N e. ( ZZ>= ` 3 ) -> ( ( F ` X ) e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) ) )
167 166 impcom 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ X e. ( 0 ..^ 4 ) ) -> ( ( F ` X ) e. ~P ( { 0 , 1 } X. ( 0 ..^ N ) ) /\ E. x e. ( 0 ..^ N ) ( ( F ` X ) = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ ( F ` X ) = { <. 0 , x >. , <. 1 , x >. } \/ ( F ` X ) = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )