Metamath Proof Explorer

Theorem cycsubm

Description: The set of nonnegative integer powers of an element A of a monoid forms a submonoid containing A (see cycsubmcl ), called the cyclic monoid generated by the element A . This corresponds to the statement in Lang p. 6. (Contributed by AV, 28-Dec-2023)

Ref Expression
Hypotheses cycsubm.b 
|- B = ( Base ` G )
cycsubm.t 
|- .x. = ( .g ` G )
cycsubm.f 
|- F = ( x e. NN0 |-> ( x .x. A ) )
cycsubm.c 
|- C = ran F
Assertion cycsubm 
|- ( ( G e. Mnd /\ A e. B ) -> C e. ( SubMnd ` G ) )

Proof

Step Hyp Ref Expression
1 cycsubm.b 
 |-  B = ( Base ` G )
2 cycsubm.t 
 |-  .x. = ( .g ` G )
3 cycsubm.f 
 |-  F = ( x e. NN0 |-> ( x .x. A ) )
4 cycsubm.c 
 |-  C = ran F
5 1 2 mulgnn0cl 
 |-  ( ( G e. Mnd /\ x e. NN0 /\ A e. B ) -> ( x .x. A ) e. B )
6 5 3expa 
 |-  ( ( ( G e. Mnd /\ x e. NN0 ) /\ A e. B ) -> ( x .x. A ) e. B )
7 6 an32s 
 |-  ( ( ( G e. Mnd /\ A e. B ) /\ x e. NN0 ) -> ( x .x. A ) e. B )
8 7 3 fmptd 
 |-  ( ( G e. Mnd /\ A e. B ) -> F : NN0 --> B )
9 8 frnd 
 |-  ( ( G e. Mnd /\ A e. B ) -> ran F C_ B )
10 4 9 eqsstrid 
 |-  ( ( G e. Mnd /\ A e. B ) -> C C_ B )
11 0nn0 
 |-  0 e. NN0
12 11 a1i 
 |-  ( ( G e. Mnd /\ A e. B ) -> 0 e. NN0 )
13 oveq1 
 |-  ( i = 0 -> ( i .x. A ) = ( 0 .x. A ) )
14 13 eqeq2d 
 |-  ( i = 0 -> ( ( 0g ` G ) = ( i .x. A ) <-> ( 0g ` G ) = ( 0 .x. A ) ) )
15 14 adantl 
 |-  ( ( ( G e. Mnd /\ A e. B ) /\ i = 0 ) -> ( ( 0g ` G ) = ( i .x. A ) <-> ( 0g ` G ) = ( 0 .x. A ) ) )
16 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
17 1 16 2 mulg0 
 |-  ( A e. B -> ( 0 .x. A ) = ( 0g ` G ) )
18 17 adantl 
 |-  ( ( G e. Mnd /\ A e. B ) -> ( 0 .x. A ) = ( 0g ` G ) )
19 18 eqcomd 
 |-  ( ( G e. Mnd /\ A e. B ) -> ( 0g ` G ) = ( 0 .x. A ) )
20 12 15 19 rspcedvd 
 |-  ( ( G e. Mnd /\ A e. B ) -> E. i e. NN0 ( 0g ` G ) = ( i .x. A ) )
21 1 2 3 4 cycsubmel 
 |-  ( ( 0g ` G ) e. C <-> E. i e. NN0 ( 0g ` G ) = ( i .x. A ) )
22 20 21 sylibr 
 |-  ( ( G e. Mnd /\ A e. B ) -> ( 0g ` G ) e. C )
23 simplr 
 |-  ( ( ( ( G e. Mnd /\ A e. B ) /\ i e. NN0 ) /\ j e. NN0 ) -> i e. NN0 )
24 simpr 
 |-  ( ( ( ( G e. Mnd /\ A e. B ) /\ i e. NN0 ) /\ j e. NN0 ) -> j e. NN0 )
25 23 24 nn0addcld 
 |-  ( ( ( ( G e. Mnd /\ A e. B ) /\ i e. NN0 ) /\ j e. NN0 ) -> ( i + j ) e. NN0 )
26 25 adantr 
 |-  ( ( ( ( ( G e. Mnd /\ A e. B ) /\ i e. NN0 ) /\ j e. NN0 ) /\ ( b = ( j .x. A ) /\ a = ( i .x. A ) ) ) -> ( i + j ) e. NN0 )
27 oveq1 
 |-  ( k = ( i + j ) -> ( k .x. A ) = ( ( i + j ) .x. A ) )
28 27 eqeq2d 
 |-  ( k = ( i + j ) -> ( ( a ( +g ` G ) b ) = ( k .x. A ) <-> ( a ( +g ` G ) b ) = ( ( i + j ) .x. A ) ) )
29 28 adantl 
 |-  ( ( ( ( ( ( G e. Mnd /\ A e. B ) /\ i e. NN0 ) /\ j e. NN0 ) /\ ( b = ( j .x. A ) /\ a = ( i .x. A ) ) ) /\ k = ( i + j ) ) -> ( ( a ( +g ` G ) b ) = ( k .x. A ) <-> ( a ( +g ` G ) b ) = ( ( i + j ) .x. A ) ) )
30 oveq12 
 |-  ( ( a = ( i .x. A ) /\ b = ( j .x. A ) ) -> ( a ( +g ` G ) b ) = ( ( i .x. A ) ( +g ` G ) ( j .x. A ) ) )
31 30 ancoms 
 |-  ( ( b = ( j .x. A ) /\ a = ( i .x. A ) ) -> ( a ( +g ` G ) b ) = ( ( i .x. A ) ( +g ` G ) ( j .x. A ) ) )
32 simplll 
 |-  ( ( ( ( G e. Mnd /\ A e. B ) /\ i e. NN0 ) /\ j e. NN0 ) -> G e. Mnd )
33 simpllr 
 |-  ( ( ( ( G e. Mnd /\ A e. B ) /\ i e. NN0 ) /\ j e. NN0 ) -> A e. B )
34 eqid 
 |-  ( +g ` G ) = ( +g ` G )
35 1 2 34 mulgnn0dir 
 |-  ( ( G e. Mnd /\ ( i e. NN0 /\ j e. NN0 /\ A e. B ) ) -> ( ( i + j ) .x. A ) = ( ( i .x. A ) ( +g ` G ) ( j .x. A ) ) )
36 32 23 24 33 35 syl13anc 
 |-  ( ( ( ( G e. Mnd /\ A e. B ) /\ i e. NN0 ) /\ j e. NN0 ) -> ( ( i + j ) .x. A ) = ( ( i .x. A ) ( +g ` G ) ( j .x. A ) ) )
37 36 eqcomd 
 |-  ( ( ( ( G e. Mnd /\ A e. B ) /\ i e. NN0 ) /\ j e. NN0 ) -> ( ( i .x. A ) ( +g ` G ) ( j .x. A ) ) = ( ( i + j ) .x. A ) )
38 31 37 sylan9eqr 
 |-  ( ( ( ( ( G e. Mnd /\ A e. B ) /\ i e. NN0 ) /\ j e. NN0 ) /\ ( b = ( j .x. A ) /\ a = ( i .x. A ) ) ) -> ( a ( +g ` G ) b ) = ( ( i + j ) .x. A ) )
39 26 29 38 rspcedvd 
 |-  ( ( ( ( ( G e. Mnd /\ A e. B ) /\ i e. NN0 ) /\ j e. NN0 ) /\ ( b = ( j .x. A ) /\ a = ( i .x. A ) ) ) -> E. k e. NN0 ( a ( +g ` G ) b ) = ( k .x. A ) )
40 39 exp32 
 |-  ( ( ( ( G e. Mnd /\ A e. B ) /\ i e. NN0 ) /\ j e. NN0 ) -> ( b = ( j .x. A ) -> ( a = ( i .x. A ) -> E. k e. NN0 ( a ( +g ` G ) b ) = ( k .x. A ) ) ) )
41 40 rexlimdva 
 |-  ( ( ( G e. Mnd /\ A e. B ) /\ i e. NN0 ) -> ( E. j e. NN0 b = ( j .x. A ) -> ( a = ( i .x. A ) -> E. k e. NN0 ( a ( +g ` G ) b ) = ( k .x. A ) ) ) )
42 41 com23 
 |-  ( ( ( G e. Mnd /\ A e. B ) /\ i e. NN0 ) -> ( a = ( i .x. A ) -> ( E. j e. NN0 b = ( j .x. A ) -> E. k e. NN0 ( a ( +g ` G ) b ) = ( k .x. A ) ) ) )
43 42 rexlimdva 
 |-  ( ( G e. Mnd /\ A e. B ) -> ( E. i e. NN0 a = ( i .x. A ) -> ( E. j e. NN0 b = ( j .x. A ) -> E. k e. NN0 ( a ( +g ` G ) b ) = ( k .x. A ) ) ) )
44 43 impd 
 |-  ( ( G e. Mnd /\ A e. B ) -> ( ( E. i e. NN0 a = ( i .x. A ) /\ E. j e. NN0 b = ( j .x. A ) ) -> E. k e. NN0 ( a ( +g ` G ) b ) = ( k .x. A ) ) )
45 1 2 3 4 cycsubmel 
 |-  ( a e. C <-> E. i e. NN0 a = ( i .x. A ) )
46 1 2 3 4 cycsubmel 
 |-  ( b e. C <-> E. j e. NN0 b = ( j .x. A ) )
47 45 46 anbi12i 
 |-  ( ( a e. C /\ b e. C ) <-> ( E. i e. NN0 a = ( i .x. A ) /\ E. j e. NN0 b = ( j .x. A ) ) )
48 1 2 3 4 cycsubmel 
 |-  ( ( a ( +g ` G ) b ) e. C <-> E. k e. NN0 ( a ( +g ` G ) b ) = ( k .x. A ) )
49 44 47 48 3imtr4g 
 |-  ( ( G e. Mnd /\ A e. B ) -> ( ( a e. C /\ b e. C ) -> ( a ( +g ` G ) b ) e. C ) )
50 49 ralrimivv 
 |-  ( ( G e. Mnd /\ A e. B ) -> A. a e. C A. b e. C ( a ( +g ` G ) b ) e. C )
51 1 16 34 issubm 
 |-  ( G e. Mnd -> ( C e. ( SubMnd ` G ) <-> ( C C_ B /\ ( 0g ` G ) e. C /\ A. a e. C A. b e. C ( a ( +g ` G ) b ) e. C ) ) )
52 51 adantr 
 |-  ( ( G e. Mnd /\ A e. B ) -> ( C e. ( SubMnd ` G ) <-> ( C C_ B /\ ( 0g ` G ) e. C /\ A. a e. C A. b e. C ( a ( +g ` G ) b ) e. C ) ) )
53 10 22 50 52 mpbir3and 
 |-  ( ( G e. Mnd /\ A e. B ) -> C e. ( SubMnd ` G ) )