Metamath Proof Explorer

Theorem smndex1mndlem

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

Ref Expression
Hypotheses smndex1ibas.m 
|- M = ( EndoFMnd ` NN0 )
smndex1ibas.n 
|- N e. NN
smndex1ibas.i 
|- I = ( x e. NN0 |-> ( x mod N ) )
smndex1ibas.g 
|- G = ( n e. ( 0 ..^ N ) |-> ( x e. NN0 |-> n ) )
smndex1mgm.b 
|- B = ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } )
smndex1mgm.s 
|- S = ( M |`s B )
Assertion smndex1mndlem 
|- ( X e. B -> ( ( I o. X ) = X /\ ( X o. I ) = X ) )

Proof

Step Hyp Ref Expression
1 smndex1ibas.m 
 |-  M = ( EndoFMnd ` NN0 )
2 smndex1ibas.n 
 |-  N e. NN
3 smndex1ibas.i 
 |-  I = ( x e. NN0 |-> ( x mod N ) )
4 smndex1ibas.g 
 |-  G = ( n e. ( 0 ..^ N ) |-> ( x e. NN0 |-> n ) )
5 smndex1mgm.b 
 |-  B = ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } )
6 smndex1mgm.s 
 |-  S = ( M |`s B )
7 elun 
 |-  ( X e. ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) <-> ( X e. { I } \/ X e. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) )
8 elsni 
 |-  ( X e. { I } -> X = I )
9 1 2 3 smndex1iidm 
 |-  ( I o. I ) = I
10 coeq2 
 |-  ( X = I -> ( I o. X ) = ( I o. I ) )
11 id 
 |-  ( X = I -> X = I )
12 9 10 11 3eqtr4a 
 |-  ( X = I -> ( I o. X ) = X )
13 coeq1 
 |-  ( X = I -> ( X o. I ) = ( I o. I ) )
14 9 13 11 3eqtr4a 
 |-  ( X = I -> ( X o. I ) = X )
15 12 14 jca 
 |-  ( X = I -> ( ( I o. X ) = X /\ ( X o. I ) = X ) )
16 8 15 syl 
 |-  ( X e. { I } -> ( ( I o. X ) = X /\ ( X o. I ) = X ) )
17 eliun 
 |-  ( X e. U_ n e. ( 0 ..^ N ) { ( G ` n ) } <-> E. n e. ( 0 ..^ N ) X e. { ( G ` n ) } )
18 fveq2 
 |-  ( n = k -> ( G ` n ) = ( G ` k ) )
19 18 sneqd 
 |-  ( n = k -> { ( G ` n ) } = { ( G ` k ) } )
20 19 eleq2d 
 |-  ( n = k -> ( X e. { ( G ` n ) } <-> X e. { ( G ` k ) } ) )
21 20 cbvrexvw 
 |-  ( E. n e. ( 0 ..^ N ) X e. { ( G ` n ) } <-> E. k e. ( 0 ..^ N ) X e. { ( G ` k ) } )
22 elsni 
 |-  ( X e. { ( G ` k ) } -> X = ( G ` k ) )
23 1 2 3 4 smndex1igid 
 |-  ( k e. ( 0 ..^ N ) -> ( I o. ( G ` k ) ) = ( G ` k ) )
24 1 2 3 smndex1ibas 
 |-  I e. ( Base ` M )
25 1 2 3 4 smndex1gid 
 |-  ( ( I e. ( Base ` M ) /\ k e. ( 0 ..^ N ) ) -> ( ( G ` k ) o. I ) = ( G ` k ) )
26 24 25 mpan 
 |-  ( k e. ( 0 ..^ N ) -> ( ( G ` k ) o. I ) = ( G ` k ) )
27 23 26 jca 
 |-  ( k e. ( 0 ..^ N ) -> ( ( I o. ( G ` k ) ) = ( G ` k ) /\ ( ( G ` k ) o. I ) = ( G ` k ) ) )
28 coeq2 
 |-  ( X = ( G ` k ) -> ( I o. X ) = ( I o. ( G ` k ) ) )
29 id 
 |-  ( X = ( G ` k ) -> X = ( G ` k ) )
30 28 29 eqeq12d 
 |-  ( X = ( G ` k ) -> ( ( I o. X ) = X <-> ( I o. ( G ` k ) ) = ( G ` k ) ) )
31 coeq1 
 |-  ( X = ( G ` k ) -> ( X o. I ) = ( ( G ` k ) o. I ) )
32 31 29 eqeq12d 
 |-  ( X = ( G ` k ) -> ( ( X o. I ) = X <-> ( ( G ` k ) o. I ) = ( G ` k ) ) )
33 30 32 anbi12d 
 |-  ( X = ( G ` k ) -> ( ( ( I o. X ) = X /\ ( X o. I ) = X ) <-> ( ( I o. ( G ` k ) ) = ( G ` k ) /\ ( ( G ` k ) o. I ) = ( G ` k ) ) ) )
34 27 33 syl5ibr 
 |-  ( X = ( G ` k ) -> ( k e. ( 0 ..^ N ) -> ( ( I o. X ) = X /\ ( X o. I ) = X ) ) )
35 22 34 syl 
 |-  ( X e. { ( G ` k ) } -> ( k e. ( 0 ..^ N ) -> ( ( I o. X ) = X /\ ( X o. I ) = X ) ) )
36 35 impcom 
 |-  ( ( k e. ( 0 ..^ N ) /\ X e. { ( G ` k ) } ) -> ( ( I o. X ) = X /\ ( X o. I ) = X ) )
37 36 rexlimiva 
 |-  ( E. k e. ( 0 ..^ N ) X e. { ( G ` k ) } -> ( ( I o. X ) = X /\ ( X o. I ) = X ) )
38 21 37 sylbi 
 |-  ( E. n e. ( 0 ..^ N ) X e. { ( G ` n ) } -> ( ( I o. X ) = X /\ ( X o. I ) = X ) )
39 17 38 sylbi 
 |-  ( X e. U_ n e. ( 0 ..^ N ) { ( G ` n ) } -> ( ( I o. X ) = X /\ ( X o. I ) = X ) )
40 16 39 jaoi 
 |-  ( ( X e. { I } \/ X e. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) -> ( ( I o. X ) = X /\ ( X o. I ) = X ) )
41 7 40 sylbi 
 |-  ( X e. ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) -> ( ( I o. X ) = X /\ ( X o. I ) = X ) )
42 41 5 eleq2s 
 |-  ( X e. B -> ( ( I o. X ) = X /\ ( X o. I ) = X ) )