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 birani ⊢ ( ( { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ∧ { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ) → { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
16 10 15 sylbir ⊢ ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } } ⊆ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) → { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
17 16 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 ‘ 𝐺 ) )
18 7 17 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 ‘ 𝐺 ) )
19 6 18 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
20 prex ⊢ { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } ∈ V
21 prex ⊢ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∈ V
22 20 21 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 ) ) )
23 prcom ⊢ { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } = { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ }
24 23 13 eleq12i ⊢ ( { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ↔ { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
25 24 birani ⊢ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ∧ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ) → { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
26 22 25 sylbir ⊢ ( { { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } } ⊆ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) → { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
27 26 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 ‘ 𝐺 ) )
28 7 27 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 ‘ 𝐺 ) )
29 6 28 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
30 13 eleq2i ⊢ ( { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ↔ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
31 30 bilani ⊢ ( ( { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ∧ { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) ) → { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
32 22 31 sylbir ⊢ ( { { ⟨ 1 , 1 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } } ⊆ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) → { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
33 32 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 ‘ 𝐺 ) )
34 7 33 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 ‘ 𝐺 ) )
35 6 34 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
36 19 29 35 s3cld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → ⟨“ { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } { ⟨ 0 , 1 ⟩ , ⟨ 1 , 1 ⟩ } { ⟨ 1 , 1 ⟩ , ⟨ 1 , 0 ⟩ } ”⟩ ∈ Word dom ( iEdg ‘ 𝐺 ) )
37 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 ) ) )
38 10 37 sylbir ⊢ ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } } ⊆ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) → { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } ∈ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) )
39 prcom ⊢ { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ }
40 3 fveq2i ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) )
41 40 dmeqi ⊢ dom ( iEdg ‘ 𝐺 ) = dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) )
42 38 39 41 3eltr4g ⊢ ( { { ⟨ 0 , 0 ⟩ , ⟨ 0 , 1 ⟩ } , { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } } ⊆ dom ( iEdg ‘ ( 𝑁 gPetersenGr 1 ) ) → { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
43 42 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 ‘ 𝐺 ) )
44 7 43 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 ‘ 𝐺 ) )
45 6 44 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → { ⟨ 1 , 0 ⟩ , ⟨ 0 , 0 ⟩ } ∈ dom ( iEdg ‘ 𝐺 ) )
46 5 36 45 cats1cld ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 3 ) → 𝐹 ∈ Word dom ( iEdg ‘ 𝐺 ) )