Metamath Proof Explorer

Theorem gpgprismgr4cycllem8

Description: Lemma 8 for gpgprismgr4cycl0 . (Contributed by AV, 2-Nov-2025)

Ref Expression
Hypotheses gpgprismgr4cycl.p ⊢ 𝑃 = ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩
gpgprismgr4cycl.f ⊢ 𝐹 = ⟨“ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ”⟩
gpgprismgr4cycl.g ⊢ 𝐺 = ( 𝑁 gPetersenGr 1 )
Assertion gpgprismgr4cycllem8 ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 gpgprismgr4cycl.p ⊢ 𝑃 = ⟨“ ⟨ 0 , 0 ⟩ ⟨ 0 , 1 ⟩ ⟨ 1 , 1 ⟩ ⟨ 1 , 0 ⟩ ⟨ 0 , 0 ⟩ ”⟩
2 gpgprismgr4cycl.f ⊢ 𝐹 = ⟨“ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ”⟩
3 gpgprismgr4cycl.g ⊢ 𝐺 = ( 𝑁 gPetersenGr 1 )
4 df-s4 ⊢ ⟨“ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ”⟩ = ( ⟨“ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ”⟩ ++ ⟨“ { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ”⟩ )
5 2 4 eqtri ⊢ 𝐹 = ( ⟨“ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ”⟩ ++ ⟨“ { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ”⟩ )
6 gpgprismgriedgdmss ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } } ∪ { { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } } ) ⊆ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) )
7 unss ⊢ ( ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } } ⊆ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ∧ { { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } } ⊆ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ) ↔ ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } } ∪ { { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } } ) ⊆ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) )
8 prex ⊢ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ∈ V
9 prex ⊢ { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } ∈ V
10 8 9 prss ⊢ ( ( { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ∧ { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ) ↔ { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } } ⊆ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) )
11 3 eqcomi ⊢ ( 𝑁 gPetersenGr 1 ) = 𝐺
12 11 fveq2i ⊢ ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) = ( iEdg ‘ 𝐺 )
13 12 dmeqi ⊢ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) = dom ( iEdg ‘ 𝐺 )
14 13 eleq2i ⊢ ( { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ↔ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
15 14 biimpi ⊢ ( { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) → { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
16 15 adantr ⊢ ( ( { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ∧ { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ) → { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
17 10 16 sylbir ⊢ ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } } ⊆ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) → { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
18 17 adantr ⊢ ( ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } } ⊆ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ∧ { { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } } ⊆ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ) → { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
19 7 18 sylbir ⊢ ( ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } } ∪ { { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } } ) ⊆ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) → { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
20 6 19 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
21 prex ⊢ { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } ∈ V
22 prex ⊢ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∈ V
23 21 22 prss ⊢ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ∧ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ) ↔ { { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } } ⊆ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) )
24 prcom ⊢ { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ }
25 24 13 eleq12i ⊢ ( { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ↔ { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
26 25 biimpi ⊢ ( { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) → { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
27 26 adantr ⊢ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ∧ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ) → { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
28 23 27 sylbir ⊢ ( { { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } } ⊆ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) → { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
29 28 adantl ⊢ ( ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } } ⊆ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ∧ { { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } } ⊆ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ) → { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
30 7 29 sylbir ⊢ ( ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } } ∪ { { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } } ) ⊆ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) → { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
31 6 30 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
32 13 eleq2i ⊢ ( { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ↔ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
33 32 biimpi ⊢ ( { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) → { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
34 33 adantl ⊢ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ∧ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ) → { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
35 23 34 sylbir ⊢ ( { { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } } ⊆ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) → { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
36 35 adantl ⊢ ( ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } } ⊆ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ∧ { { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } } ⊆ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ) → { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
37 7 36 sylbir ⊢ ( ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } } ∪ { { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } } ) ⊆ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) → { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
38 6 37 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
39 20 31 38 s3cld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ⟨“ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ”⟩ ∈ Word dom ( iEdg ‘ 𝐺 ) )
40 simpr ⊢ ( ( { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ∧ { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ) → { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) )
41 10 40 sylbir ⊢ ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } } ⊆ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) → { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) )
42 prcom ⊢ { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ }
43 3 fveq2i ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) )
44 43 dmeqi ⊢ dom ( iEdg ‘ 𝐺 ) = dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) )
45 41 42 44 3eltr4g ⊢ ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } } ⊆ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) → { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
46 45 adantr ⊢ ( ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } } ⊆ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ∧ { { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } } ⊆ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ) → { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
47 7 46 sylbir ⊢ ( ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } } ∪ { { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } } ) ⊆ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) → { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
48 6 47 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
49 5 39 48 cats1cld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) )