cycsubmcom

Description: The operation of a monoid is commutative over the set of nonnegative integer powers of an element A of the monoid. (Contributed by AV, 20-Jan-2024)

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

Proof

Step	Hyp	Ref	Expression
1		cycsubmcom.b	\|- B = ( Base ` G )
2		cycsubmcom.t	\|- .x. = ( .g ` G )
3		cycsubmcom.f	\|- F = ( x e. NN0 \|-> ( x .x. A ) )
4		cycsubmcom.c	\|- C = ran F
5		cycsubmcom.p	\|- .+ = ( +g ` G )
6	1 2 3 4	cycsubmel	\|- ( c e. C <-> E. i e. NN0 c = ( i .x. A ) )
7	6	biimpi	\|- ( c e. C -> E. i e. NN0 c = ( i .x. A ) )
8	7	adantl	\|- ( ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) /\ c e. C ) -> E. i e. NN0 c = ( i .x. A ) )
9	8	ralrimiva	\|- ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) -> A. c e. C E. i e. NN0 c = ( i .x. A ) )
10		simplll	\|- ( ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) /\ ( m e. NN0 /\ n e. NN0 ) ) -> G e. Mnd )
11		simprl	\|- ( ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) /\ ( m e. NN0 /\ n e. NN0 ) ) -> m e. NN0 )
12		simprr	\|- ( ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) /\ ( m e. NN0 /\ n e. NN0 ) ) -> n e. NN0 )
13		simpllr	\|- ( ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) /\ ( m e. NN0 /\ n e. NN0 ) ) -> A e. B )
14	1 2 5	mulgnn0dir	\|- ( ( G e. Mnd /\ ( m e. NN0 /\ n e. NN0 /\ A e. B ) ) -> ( ( m + n ) .x. A ) = ( ( m .x. A ) .+ ( n .x. A ) ) )
15	10 11 12 13 14	syl13anc	\|- ( ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) /\ ( m e. NN0 /\ n e. NN0 ) ) -> ( ( m + n ) .x. A ) = ( ( m .x. A ) .+ ( n .x. A ) ) )
16	15	ralrimivva	\|- ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) -> A. m e. NN0 A. n e. NN0 ( ( m + n ) .x. A ) = ( ( m .x. A ) .+ ( n .x. A ) ) )
17		simprl	\|- ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) -> X e. C )
18		simprr	\|- ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) -> Y e. C )
19		nn0sscn	\|- NN0 C_ CC
20	19	a1i	\|- ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) -> NN0 C_ CC )
21	9 16 17 18 20	cyccom	\|- ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) -> ( X .+ Y ) = ( Y .+ X ) )

Metamath Proof Explorer

Theorem cycsubmcom

Proof