This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem smndex1mndlem

Description: Lemma for smndex1mnd and smndex1id . (Contributed by AV, 16-Feb-2024)

Ref Expression
Hypotheses smndex1ibas.m ⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
smndex1ibas.n ⊢ 𝑁 ∈ ℕ
smndex1ibas.i ⊢ 𝐼 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) )
smndex1ibas.g ⊢ 𝐺 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) )
smndex1mgm.b ⊢ 𝐵 = ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } )
smndex1mgm.s ⊢ 𝑆 = ( 𝑀 ↾s 𝐵 )
Assertion smndex1mndlem ( 𝑋 ∈ 𝐵 → ( ( 𝐼 ∘ 𝑋 ) = 𝑋 ∧ ( 𝑋 ∘ 𝐼 ) = 𝑋 ) )

Proof

Step Hyp Ref Expression
1 smndex1ibas.m ⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
2 smndex1ibas.n ⊢ 𝑁 ∈ ℕ
3 smndex1ibas.i ⊢ 𝐼 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) )
4 smndex1ibas.g ⊢ 𝐺 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) )
5 smndex1mgm.b ⊢ 𝐵 = ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } )
6 smndex1mgm.s ⊢ 𝑆 = ( 𝑀 ↾s 𝐵 )
7 elun ⊢ ( 𝑋 ∈ ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ) ↔ ( 𝑋 ∈ { 𝐼 } ∨ 𝑋 ∈ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ) )
8 elsni ⊢ ( 𝑋 ∈ { 𝐼 } → 𝑋 = 𝐼 )
9 1 2 3 smndex1iidm ⊢ ( 𝐼 ∘ 𝐼 ) = 𝐼
10 coeq2 ⊢ ( 𝑋 = 𝐼 → ( 𝐼 ∘ 𝑋 ) = ( 𝐼 ∘ 𝐼 ) )
11 id ⊢ ( 𝑋 = 𝐼 → 𝑋 = 𝐼 )
12 9 10 11 3eqtr4a ⊢ ( 𝑋 = 𝐼 → ( 𝐼 ∘ 𝑋 ) = 𝑋 )
13 coeq1 ⊢ ( 𝑋 = 𝐼 → ( 𝑋 ∘ 𝐼 ) = ( 𝐼 ∘ 𝐼 ) )
14 9 13 11 3eqtr4a ⊢ ( 𝑋 = 𝐼 → ( 𝑋 ∘ 𝐼 ) = 𝑋 )
15 12 14 jca ⊢ ( 𝑋 = 𝐼 → ( ( 𝐼 ∘ 𝑋 ) = 𝑋 ∧ ( 𝑋 ∘ 𝐼 ) = 𝑋 ) )
16 8 15 syl ⊢ ( 𝑋 ∈ { 𝐼 } → ( ( 𝐼 ∘ 𝑋 ) = 𝑋 ∧ ( 𝑋 ∘ 𝐼 ) = 𝑋 ) )
17 eliun ⊢ ( 𝑋 ∈ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ↔ ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑋 ∈ { ( 𝐺 ‘ 𝑛 ) } )
18 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑘 ) )
19 18 sneqd ⊢ ( 𝑛 = 𝑘 → { ( 𝐺 ‘ 𝑛 ) } = { ( 𝐺 ‘ 𝑘 ) } )
20 19 eleq2d ⊢ ( 𝑛 = 𝑘 → ( 𝑋 ∈ { ( 𝐺 ‘ 𝑛 ) } ↔ 𝑋 ∈ { ( 𝐺 ‘ 𝑘 ) } ) )
21 20 cbvrexvw ⊢ ( ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑋 ∈ { ( 𝐺 ‘ 𝑛 ) } ↔ ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑋 ∈ { ( 𝐺 ‘ 𝑘 ) } )
22 elsni ⊢ ( 𝑋 ∈ { ( 𝐺 ‘ 𝑘 ) } → 𝑋 = ( 𝐺 ‘ 𝑘 ) )
23 1 2 3 4 smndex1igid ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → ( 𝐼 ∘ ( 𝐺 ‘ 𝑘 ) ) = ( 𝐺 ‘ 𝑘 ) )
24 1 2 3 smndex1ibas ⊢ 𝐼 ∈ ( Base ‘ 𝑀 )
25 1 2 3 4 smndex1gid ⊢ ( ( 𝐼 ∈ ( Base ‘ 𝑀 ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐺 ‘ 𝑘 ) ∘ 𝐼 ) = ( 𝐺 ‘ 𝑘 ) )
26 24 25 mpan ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝐺 ‘ 𝑘 ) ∘ 𝐼 ) = ( 𝐺 ‘ 𝑘 ) )
27 23 26 jca ⊢ ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝐼 ∘ ( 𝐺 ‘ 𝑘 ) ) = ( 𝐺 ‘ 𝑘 ) ∧ ( ( 𝐺 ‘ 𝑘 ) ∘ 𝐼 ) = ( 𝐺 ‘ 𝑘 ) ) )
28 coeq2 ⊢ ( 𝑋 = ( 𝐺 ‘ 𝑘 ) → ( 𝐼 ∘ 𝑋 ) = ( 𝐼 ∘ ( 𝐺 ‘ 𝑘 ) ) )
29 id ⊢ ( 𝑋 = ( 𝐺 ‘ 𝑘 ) → 𝑋 = ( 𝐺 ‘ 𝑘 ) )
30 28 29 eqeq12d ⊢ ( 𝑋 = ( 𝐺 ‘ 𝑘 ) → ( ( 𝐼 ∘ 𝑋 ) = 𝑋 ↔ ( 𝐼 ∘ ( 𝐺 ‘ 𝑘 ) ) = ( 𝐺 ‘ 𝑘 ) ) )
31 coeq1 ⊢ ( 𝑋 = ( 𝐺 ‘ 𝑘 ) → ( 𝑋 ∘ 𝐼 ) = ( ( 𝐺 ‘ 𝑘 ) ∘ 𝐼 ) )
32 31 29 eqeq12d ⊢ ( 𝑋 = ( 𝐺 ‘ 𝑘 ) → ( ( 𝑋 ∘ 𝐼 ) = 𝑋 ↔ ( ( 𝐺 ‘ 𝑘 ) ∘ 𝐼 ) = ( 𝐺 ‘ 𝑘 ) ) )
33 30 32 anbi12d ⊢ ( 𝑋 = ( 𝐺 ‘ 𝑘 ) → ( ( ( 𝐼 ∘ 𝑋 ) = 𝑋 ∧ ( 𝑋 ∘ 𝐼 ) = 𝑋 ) ↔ ( ( 𝐼 ∘ ( 𝐺 ‘ 𝑘 ) ) = ( 𝐺 ‘ 𝑘 ) ∧ ( ( 𝐺 ‘ 𝑘 ) ∘ 𝐼 ) = ( 𝐺 ‘ 𝑘 ) ) ) )
34 27 33 imbitrrid ⊢ ( 𝑋 = ( 𝐺 ‘ 𝑘 ) → ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝐼 ∘ 𝑋 ) = 𝑋 ∧ ( 𝑋 ∘ 𝐼 ) = 𝑋 ) ) )
35 22 34 syl ⊢ ( 𝑋 ∈ { ( 𝐺 ‘ 𝑘 ) } → ( 𝑘 ∈ ( 0 ..^ 𝑁 ) → ( ( 𝐼 ∘ 𝑋 ) = 𝑋 ∧ ( 𝑋 ∘ 𝐼 ) = 𝑋 ) ) )
36 35 impcom ⊢ ( ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑋 ∈ { ( 𝐺 ‘ 𝑘 ) } ) → ( ( 𝐼 ∘ 𝑋 ) = 𝑋 ∧ ( 𝑋 ∘ 𝐼 ) = 𝑋 ) )
37 36 rexlimiva ⊢ ( ∃ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝑋 ∈ { ( 𝐺 ‘ 𝑘 ) } → ( ( 𝐼 ∘ 𝑋 ) = 𝑋 ∧ ( 𝑋 ∘ 𝐼 ) = 𝑋 ) )
38 21 37 sylbi ⊢ ( ∃ 𝑛 ∈ ( 0 ..^ 𝑁 ) 𝑋 ∈ { ( 𝐺 ‘ 𝑛 ) } → ( ( 𝐼 ∘ 𝑋 ) = 𝑋 ∧ ( 𝑋 ∘ 𝐼 ) = 𝑋 ) )
39 17 38 sylbi ⊢ ( 𝑋 ∈ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } → ( ( 𝐼 ∘ 𝑋 ) = 𝑋 ∧ ( 𝑋 ∘ 𝐼 ) = 𝑋 ) )
40 16 39 jaoi ⊢ ( ( 𝑋 ∈ { 𝐼 } ∨ 𝑋 ∈ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ) → ( ( 𝐼 ∘ 𝑋 ) = 𝑋 ∧ ( 𝑋 ∘ 𝐼 ) = 𝑋 ) )
41 7 40 sylbi ⊢ ( 𝑋 ∈ ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ) → ( ( 𝐼 ∘ 𝑋 ) = 𝑋 ∧ ( 𝑋 ∘ 𝐼 ) = 𝑋 ) )
42 41 5 eleq2s ⊢ ( 𝑋 ∈ 𝐵 → ( ( 𝐼 ∘ 𝑋 ) = 𝑋 ∧ ( 𝑋 ∘ 𝐼 ) = 𝑋 ) )