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	⊢ ( 𝑋 ∈ 𝐵 → ( ( 𝐼 ∘ 𝑋 ) = 𝑋 ∧ ( 𝑋 ∘ 𝐼 ) = 𝑋 ) )