Metamath Proof Explorer

Theorem gpgprismgriedgdmss

Description: A subset of the index of edges of the generalized Petersen graph GPG(N,1). (Contributed by AV, 2-Nov-2025)

Ref Expression
Assertion gpgprismgriedgdmss 
|- ( N e. ( ZZ>= ` 3 ) -> ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } u. { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } ) C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) )

Proof

Step Hyp Ref Expression
1 eluzge3nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. NN )
2 lbfzo0 
 |-  ( 0 e. ( 0 ..^ N ) <-> N e. NN )
3 1 2 sylibr 
 |-  ( N e. ( ZZ>= ` 3 ) -> 0 e. ( 0 ..^ N ) )
4 opeq2 
 |-  ( x = 0 -> <. 0 , x >. = <. 0 , 0 >. )
5 oveq1 
 |-  ( x = 0 -> ( x + 1 ) = ( 0 + 1 ) )
6 0p1e1 
 |-  ( 0 + 1 ) = 1
7 5 6 eqtrdi 
 |-  ( x = 0 -> ( x + 1 ) = 1 )
8 7 oveq1d 
 |-  ( x = 0 -> ( ( x + 1 ) mod N ) = ( 1 mod N ) )
9 8 opeq2d 
 |-  ( x = 0 -> <. 0 , ( ( x + 1 ) mod N ) >. = <. 0 , ( 1 mod N ) >. )
10 4 9 preq12d 
 |-  ( x = 0 -> { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } = { <. 0 , 0 >. , <. 0 , ( 1 mod N ) >. } )
11 10 eqeq2d 
 |-  ( x = 0 -> ( { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } <-> { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , 0 >. , <. 0 , ( 1 mod N ) >. } ) )
12 11 adantl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ x = 0 ) -> ( { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } <-> { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , 0 >. , <. 0 , ( 1 mod N ) >. } ) )
13 uzuzle23 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ( ZZ>= ` 2 ) )
14 eluz2b1 
 |-  ( N e. ( ZZ>= ` 2 ) <-> ( N e. ZZ /\ 1 < N ) )
15 zre 
 |-  ( N e. ZZ -> N e. RR )
16 15 anim1i 
 |-  ( ( N e. ZZ /\ 1 < N ) -> ( N e. RR /\ 1 < N ) )
17 14 16 sylbi 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N e. RR /\ 1 < N ) )
18 1mod 
 |-  ( ( N e. RR /\ 1 < N ) -> ( 1 mod N ) = 1 )
19 13 17 18 3syl 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( 1 mod N ) = 1 )
20 19 eqcomd 
 |-  ( N e. ( ZZ>= ` 3 ) -> 1 = ( 1 mod N ) )
21 20 opeq2d 
 |-  ( N e. ( ZZ>= ` 3 ) -> <. 0 , 1 >. = <. 0 , ( 1 mod N ) >. )
22 21 preq2d 
 |-  ( N e. ( ZZ>= ` 3 ) -> { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , 0 >. , <. 0 , ( 1 mod N ) >. } )
23 3 12 22 rspcedvd 
 |-  ( N e. ( ZZ>= ` 3 ) -> E. x e. ( 0 ..^ N ) { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } )
24 23 3mix1d 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( E. x e. ( 0 ..^ N ) { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ E. x e. ( 0 ..^ N ) { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ E. x e. ( 0 ..^ N ) { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) )
25 3r19.43 
 |-  ( 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 ) >. } ) <-> ( E. x e. ( 0 ..^ N ) { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ E. x e. ( 0 ..^ N ) { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ E. x e. ( 0 ..^ N ) { <. 0 , 0 >. , <. 0 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) )
26 24 25 sylibr 
 |-  ( 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 ) >. } ) )
27 eqid 
 |-  ( 0 ..^ N ) = ( 0 ..^ N )
28 eqid 
 |-  ( N gPetersenGr 1 ) = ( N gPetersenGr 1 )
29 27 28 gpgprismgriedgdmel 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) <-> 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 ) >. } ) ) )
30 26 29 mpbird 
 |-  ( N e. ( ZZ>= ` 3 ) -> { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) )
31 opeq2 
 |-  ( x = 0 -> <. 1 , x >. = <. 1 , 0 >. )
32 4 31 preq12d 
 |-  ( x = 0 -> { <. 0 , x >. , <. 1 , x >. } = { <. 0 , 0 >. , <. 1 , 0 >. } )
33 32 eqeq2d 
 |-  ( x = 0 -> ( { <. 0 , 0 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } <-> { <. 0 , 0 >. , <. 1 , 0 >. } = { <. 0 , 0 >. , <. 1 , 0 >. } ) )
34 33 adantl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ x = 0 ) -> ( { <. 0 , 0 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } <-> { <. 0 , 0 >. , <. 1 , 0 >. } = { <. 0 , 0 >. , <. 1 , 0 >. } ) )
35 eqid 
 |-  { <. 0 , 0 >. , <. 1 , 0 >. } = { <. 0 , 0 >. , <. 1 , 0 >. }
36 35 a1i 
 |-  ( N e. ( ZZ>= ` 3 ) -> { <. 0 , 0 >. , <. 1 , 0 >. } = { <. 0 , 0 >. , <. 1 , 0 >. } )
37 3 34 36 rspcedvd 
 |-  ( N e. ( ZZ>= ` 3 ) -> E. x e. ( 0 ..^ N ) { <. 0 , 0 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } )
38 37 3mix2d 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( E. x e. ( 0 ..^ N ) { <. 0 , 0 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ E. x e. ( 0 ..^ N ) { <. 0 , 0 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ E. x e. ( 0 ..^ N ) { <. 0 , 0 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) )
39 3r19.43 
 |-  ( E. x e. ( 0 ..^ N ) ( { <. 0 , 0 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , 0 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , 0 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) <-> ( E. x e. ( 0 ..^ N ) { <. 0 , 0 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ E. x e. ( 0 ..^ N ) { <. 0 , 0 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ E. x e. ( 0 ..^ N ) { <. 0 , 0 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) )
40 38 39 sylibr 
 |-  ( N e. ( ZZ>= ` 3 ) -> E. x e. ( 0 ..^ N ) ( { <. 0 , 0 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , 0 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , 0 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) )
41 27 28 gpgprismgriedgdmel 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( { <. 0 , 0 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) <-> E. x e. ( 0 ..^ N ) ( { <. 0 , 0 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , 0 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , 0 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )
42 40 41 mpbird 
 |-  ( N e. ( ZZ>= ` 3 ) -> { <. 0 , 0 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) )
43 30 42 prssd 
 |-  ( N e. ( ZZ>= ` 3 ) -> { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) )
44 1nn0 
 |-  1 e. NN0
45 44 a1i 
 |-  ( N e. ( ZZ>= ` 3 ) -> 1 e. NN0 )
46 eluz2gt1 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 < N )
47 13 46 syl 
 |-  ( N e. ( ZZ>= ` 3 ) -> 1 < N )
48 elfzo0 
 |-  ( 1 e. ( 0 ..^ N ) <-> ( 1 e. NN0 /\ N e. NN /\ 1 < N ) )
49 45 1 47 48 syl3anbrc 
 |-  ( N e. ( ZZ>= ` 3 ) -> 1 e. ( 0 ..^ N ) )
50 opeq2 
 |-  ( x = 1 -> <. 0 , x >. = <. 0 , 1 >. )
51 opeq2 
 |-  ( x = 1 -> <. 1 , x >. = <. 1 , 1 >. )
52 50 51 preq12d 
 |-  ( x = 1 -> { <. 0 , x >. , <. 1 , x >. } = { <. 0 , 1 >. , <. 1 , 1 >. } )
53 52 eqeq2d 
 |-  ( x = 1 -> ( { <. 1 , 1 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } <-> { <. 1 , 1 >. , <. 0 , 1 >. } = { <. 0 , 1 >. , <. 1 , 1 >. } ) )
54 53 adantl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ x = 1 ) -> ( { <. 1 , 1 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } <-> { <. 1 , 1 >. , <. 0 , 1 >. } = { <. 0 , 1 >. , <. 1 , 1 >. } ) )
55 prcom 
 |-  { <. 1 , 1 >. , <. 0 , 1 >. } = { <. 0 , 1 >. , <. 1 , 1 >. }
56 55 a1i 
 |-  ( N e. ( ZZ>= ` 3 ) -> { <. 1 , 1 >. , <. 0 , 1 >. } = { <. 0 , 1 >. , <. 1 , 1 >. } )
57 49 54 56 rspcedvd 
 |-  ( N e. ( ZZ>= ` 3 ) -> E. x e. ( 0 ..^ N ) { <. 1 , 1 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } )
58 57 3mix2d 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( E. x e. ( 0 ..^ N ) { <. 1 , 1 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ E. x e. ( 0 ..^ N ) { <. 1 , 1 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ E. x e. ( 0 ..^ N ) { <. 1 , 1 >. , <. 0 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) )
59 3r19.43 
 |-  ( E. x e. ( 0 ..^ N ) ( { <. 1 , 1 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 1 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 1 >. , <. 0 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) <-> ( E. x e. ( 0 ..^ N ) { <. 1 , 1 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ E. x e. ( 0 ..^ N ) { <. 1 , 1 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ E. x e. ( 0 ..^ N ) { <. 1 , 1 >. , <. 0 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) )
60 58 59 sylibr 
 |-  ( N e. ( ZZ>= ` 3 ) -> E. x e. ( 0 ..^ N ) ( { <. 1 , 1 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 1 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 1 >. , <. 0 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) )
61 27 28 gpgprismgriedgdmel 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( { <. 1 , 1 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) <-> E. x e. ( 0 ..^ N ) ( { <. 1 , 1 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 1 , 1 >. , <. 0 , 1 >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 1 , 1 >. , <. 0 , 1 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) ) )
62 60 61 mpbird 
 |-  ( N e. ( ZZ>= ` 3 ) -> { <. 1 , 1 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) )
63 8 opeq2d 
 |-  ( x = 0 -> <. 1 , ( ( x + 1 ) mod N ) >. = <. 1 , ( 1 mod N ) >. )
64 31 63 preq12d 
 |-  ( x = 0 -> { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } = { <. 1 , 0 >. , <. 1 , ( 1 mod N ) >. } )
65 64 eqeq2d 
 |-  ( x = 0 -> ( { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } <-> { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , 0 >. , <. 1 , ( 1 mod N ) >. } ) )
66 65 adantl 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ x = 0 ) -> ( { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } <-> { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , 0 >. , <. 1 , ( 1 mod N ) >. } ) )
67 prcom 
 |-  { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , 0 >. , <. 1 , 1 >. }
68 20 opeq2d 
 |-  ( N e. ( ZZ>= ` 3 ) -> <. 1 , 1 >. = <. 1 , ( 1 mod N ) >. )
69 68 preq2d 
 |-  ( N e. ( ZZ>= ` 3 ) -> { <. 1 , 0 >. , <. 1 , 1 >. } = { <. 1 , 0 >. , <. 1 , ( 1 mod N ) >. } )
70 67 69 eqtrid 
 |-  ( N e. ( ZZ>= ` 3 ) -> { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , 0 >. , <. 1 , ( 1 mod N ) >. } )
71 3 66 70 rspcedvd 
 |-  ( N e. ( ZZ>= ` 3 ) -> E. x e. ( 0 ..^ N ) { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } )
72 71 3mix3d 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( E. x e. ( 0 ..^ N ) { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ E. x e. ( 0 ..^ N ) { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ E. x e. ( 0 ..^ N ) { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) )
73 3r19.43 
 |-  ( 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 ) >. } ) <-> ( E. x e. ( 0 ..^ N ) { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ E. x e. ( 0 ..^ N ) { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 0 , x >. , <. 1 , x >. } \/ E. x e. ( 0 ..^ N ) { <. 1 , 1 >. , <. 1 , 0 >. } = { <. 1 , x >. , <. 1 , ( ( x + 1 ) mod N ) >. } ) )
74 72 73 sylibr 
 |-  ( 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 ) >. } ) )
75 27 28 gpgprismgriedgdmel 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) <-> 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 ) >. } ) ) )
76 74 75 mpbird 
 |-  ( N e. ( ZZ>= ` 3 ) -> { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) )
77 62 76 prssd 
 |-  ( N e. ( ZZ>= ` 3 ) -> { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) )
78 43 77 unssd 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } u. { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } ) C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) )