Theorem smndex1mndlem

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

	Ref	Expression
Hypotheses	smndex1ibas.m	No typesetting found for |- M = ( EndoFMnd ` NN0 ) with typecode |-
	smndex1ibas.n	$$⊢N\in \mathbb{N}$$
	smndex1ibas.i	$$⊢I=\left(x\in {\mathbb{N}}_0⟼x\mathrm{mod}N\right)$$
	smndex1ibas.g	$$⊢G=\left(n\in \left(0..^N\right)⟼\left(x\in {\mathbb{N}}_0⟼n\right)\right)$$
	smndex1mgm.b	$$⊢B=\left\{I\right\}\cup \bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}$$
	smndex1mgm.s	$$⊢S=M{\upharpoonright }_{𝑠}B$$
Assertion	smndex1mndlem	$$⊢X\in B\to \left(I\circ X=X\wedge X\circ I=X\right)$$

Proof

Step	Hyp	Ref	Expression
1		smndex1ibas.m	Could not format M = ( EndoFMnd ` NN0 ) : No typesetting found for |- M = ( EndoFMnd ` NN0 ) with typecode |-
2		smndex1ibas.n	$$⊢N\in \mathbb{N}$$
3		smndex1ibas.i	$$⊢I=\left(x\in {\mathbb{N}}_0⟼x\mathrm{mod}N\right)$$
4		smndex1ibas.g	$$⊢G=\left(n\in \left(0..^N\right)⟼\left(x\in {\mathbb{N}}_0⟼n\right)\right)$$
5		smndex1mgm.b	$$⊢B=\left\{I\right\}\cup \bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}$$
6		smndex1mgm.s	$$⊢S=M{\upharpoonright }_{𝑠}B$$
7		elun	$$⊢X\in \left(\left\{I\right\}\cup \bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}\right)\leftrightarrow \left(X\in \left\{I\right\}\vee X\in \bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}\right)$$
8		elsni	$$⊢X\in \left\{I\right\}\to X=I$$
9	1 2 3	smndex1iidm	$$⊢I\circ I=I$$
10		coeq2	$$⊢X=I\to I\circ X=I\circ I$$
11		id	$$⊢X=I\to X=I$$
12	9 10 11	3eqtr4a	$$⊢X=I\to I\circ X=X$$
13		coeq1	$$⊢X=I\to X\circ I=I\circ I$$
14	9 13 11	3eqtr4a	$$⊢X=I\to X\circ I=X$$
15	12 14	jca	$$⊢X=I\to \left(I\circ X=X\wedge X\circ I=X\right)$$
16	8 15	syl	$$⊢X\in \left\{I\right\}\to \left(I\circ X=X\wedge X\circ I=X\right)$$
17		eliun	$$⊢X\in \bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}\leftrightarrow \exists n\in \left(0..^N\right)X\in \left\{G\left(n\right)\right\}$$
18		fveq2	$$⊢n=k\to G\left(n\right)=G\left(k\right)$$
19	18	sneqd	$$⊢n=k\to \left\{G\left(n\right)\right\}=\left\{G\left(k\right)\right\}$$
20	19	eleq2d	$$⊢n=k\to \left(X\in \left\{G\left(n\right)\right\}\leftrightarrow X\in \left\{G\left(k\right)\right\}\right)$$
21	20	cbvrexvw	$$⊢\exists n\in \left(0..^N\right)X\in \left\{G\left(n\right)\right\}\leftrightarrow \exists k\in \left(0..^N\right)X\in \left\{G\left(k\right)\right\}$$
22		elsni	$$⊢X\in \left\{G\left(k\right)\right\}\to X=G\left(k\right)$$
23	1 2 3 4	smndex1igid	$$⊢k\in \left(0..^N\right)\to I\circ G\left(k\right)=G\left(k\right)$$
24	1 2 3	smndex1ibas	$$⊢I\in {\mathrm{Base}}_M$$
25	1 2 3 4	smndex1gid	$$⊢\left(I\in {\mathrm{Base}}_M\wedge k\in \left(0..^N\right)\right)\to G\left(k\right)\circ I=G\left(k\right)$$
26	24 25	mpan	$$⊢k\in \left(0..^N\right)\to G\left(k\right)\circ I=G\left(k\right)$$
27	23 26	jca	$$⊢k\in \left(0..^N\right)\to \left(I\circ G\left(k\right)=G\left(k\right)\wedge G\left(k\right)\circ I=G\left(k\right)\right)$$
28		coeq2	$$⊢X=G\left(k\right)\to I\circ X=I\circ G\left(k\right)$$
29		id	$$⊢X=G\left(k\right)\to X=G\left(k\right)$$
30	28 29	eqeq12d	$$⊢X=G\left(k\right)\to \left(I\circ X=X\leftrightarrow I\circ G\left(k\right)=G\left(k\right)\right)$$
31		coeq1	$$⊢X=G\left(k\right)\to X\circ I=G\left(k\right)\circ I$$
32	31 29	eqeq12d	$$⊢X=G\left(k\right)\to \left(X\circ I=X\leftrightarrow G\left(k\right)\circ I=G\left(k\right)\right)$$
33	30 32	anbi12d	$$⊢X=G\left(k\right)\to \left(\left(I\circ X=X\wedge X\circ I=X\right)\leftrightarrow \left(I\circ G\left(k\right)=G\left(k\right)\wedge G\left(k\right)\circ I=G\left(k\right)\right)\right)$$
34	27 33	imbitrrid	$$⊢X=G\left(k\right)\to \left(k\in \left(0..^N\right)\to \left(I\circ X=X\wedge X\circ I=X\right)\right)$$
35	22 34	syl	$$⊢X\in \left\{G\left(k\right)\right\}\to \left(k\in \left(0..^N\right)\to \left(I\circ X=X\wedge X\circ I=X\right)\right)$$
36	35	impcom	$$⊢\left(k\in \left(0..^N\right)\wedge X\in \left\{G\left(k\right)\right\}\right)\to \left(I\circ X=X\wedge X\circ I=X\right)$$
37	36	rexlimiva	$$⊢\exists k\in \left(0..^N\right)X\in \left\{G\left(k\right)\right\}\to \left(I\circ X=X\wedge X\circ I=X\right)$$
38	21 37	sylbi	$$⊢\exists n\in \left(0..^N\right)X\in \left\{G\left(n\right)\right\}\to \left(I\circ X=X\wedge X\circ I=X\right)$$
39	17 38	sylbi	$$⊢X\in \bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}\to \left(I\circ X=X\wedge X\circ I=X\right)$$
40	16 39	jaoi	$$⊢\left(X\in \left\{I\right\}\vee X\in \bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}\right)\to \left(I\circ X=X\wedge X\circ I=X\right)$$
41	7 40	sylbi	$$⊢X\in \left(\left\{I\right\}\cup \bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}\right)\to \left(I\circ X=X\wedge X\circ I=X\right)$$
42	41 5	eleq2s	$$⊢X\in B\to \left(I\circ X=X\wedge X\circ I=X\right)$$