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 ) )