Theorem mndodcongi

Description: If two multipliers are congruent relative to the base point's order, the corresponding multiples are the same. For monoids, the reverse implication is false for elements with infinite order. For example, the powers of 2 mod 1 0 are 1,2,4,8,6,2,4,8,6,... so that the identity 1 never repeats, which is infinite order by our definition, yet other numbers like 6 appear many times in the sequence. (Contributed by Mario Carneiro, 23-Sep-2015)

	Ref	Expression
Hypotheses	odcl.1	|- X = ( Base ` G )
	odcl.2	|- O = ( od ` G )
	odid.3	|- .x. = ( .g ` G )
	odid.4	|- .0. = ( 0g ` G )
Assertion	mndodcongi	|- ( ( G e. Mnd /\ A e. X /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( O ` A ) || ( M - N ) -> ( M .x. A ) = ( N .x. A ) ) )

Proof

Step	Hyp	Ref	Expression
1		odcl.1	|- X = ( Base ` G )
2		odcl.2	|- O = ( od ` G )
3		odid.3	|- .x. = ( .g ` G )
4		odid.4	|- .0. = ( 0g ` G )
5	1 2 3 4	mndodcong	|- ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( O ` A ) || ( M - N ) <-> ( M .x. A ) = ( N .x. A ) ) )
6	5	biimpd	|- ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( O ` A ) || ( M - N ) -> ( M .x. A ) = ( N .x. A ) ) )
7	6	3expia	|- ( ( ( G e. Mnd /\ A e. X ) /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( O ` A ) e. NN -> ( ( O ` A ) || ( M - N ) -> ( M .x. A ) = ( N .x. A ) ) ) )
8	7	3impa	|- ( ( G e. Mnd /\ A e. X /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( O ` A ) e. NN -> ( ( O ` A ) || ( M - N ) -> ( M .x. A ) = ( N .x. A ) ) ) )
9		nn0z	|- ( M e. NN0 -> M e. ZZ )
10		nn0z	|- ( N e. NN0 -> N e. ZZ )
11		zsubcl	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M - N ) e. ZZ )
12	9 10 11	syl2an	|- ( ( M e. NN0 /\ N e. NN0 ) -> ( M - N ) e. ZZ )
13	12	3ad2ant3	|- ( ( G e. Mnd /\ A e. X /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( M - N ) e. ZZ )
14		0dvds	|- ( ( M - N ) e. ZZ -> ( 0 || ( M - N ) <-> ( M - N ) = 0 ) )
15	13 14	syl	|- ( ( G e. Mnd /\ A e. X /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( 0 || ( M - N ) <-> ( M - N ) = 0 ) )
16		nn0cn	|- ( M e. NN0 -> M e. CC )
17		nn0cn	|- ( N e. NN0 -> N e. CC )
18		subeq0	|- ( ( M e. CC /\ N e. CC ) -> ( ( M - N ) = 0 <-> M = N ) )
19	16 17 18	syl2an	|- ( ( M e. NN0 /\ N e. NN0 ) -> ( ( M - N ) = 0 <-> M = N ) )
20	19	3ad2ant3	|- ( ( G e. Mnd /\ A e. X /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( M - N ) = 0 <-> M = N ) )
21		oveq1	|- ( M = N -> ( M .x. A ) = ( N .x. A ) )
22	20 21	syl6bi	|- ( ( G e. Mnd /\ A e. X /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( M - N ) = 0 -> ( M .x. A ) = ( N .x. A ) ) )
23	15 22	sylbid	|- ( ( G e. Mnd /\ A e. X /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( 0 || ( M - N ) -> ( M .x. A ) = ( N .x. A ) ) )
24		breq1	|- ( ( O ` A ) = 0 -> ( ( O ` A ) || ( M - N ) <-> 0 || ( M - N ) ) )
25	24	imbi1d	|- ( ( O ` A ) = 0 -> ( ( ( O ` A ) || ( M - N ) -> ( M .x. A ) = ( N .x. A ) ) <-> ( 0 || ( M - N ) -> ( M .x. A ) = ( N .x. A ) ) ) )
26	23 25	syl5ibrcom	|- ( ( G e. Mnd /\ A e. X /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( O ` A ) = 0 -> ( ( O ` A ) || ( M - N ) -> ( M .x. A ) = ( N .x. A ) ) ) )
27	1 2	odcl	|- ( A e. X -> ( O ` A ) e. NN0 )
28	27	3ad2ant2	|- ( ( G e. Mnd /\ A e. X /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( O ` A ) e. NN0 )
29		elnn0	|- ( ( O ` A ) e. NN0 <-> ( ( O ` A ) e. NN \/ ( O ` A ) = 0 ) )
30	28 29	sylib	|- ( ( G e. Mnd /\ A e. X /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( O ` A ) e. NN \/ ( O ` A ) = 0 ) )
31	8 26 30	mpjaod	|- ( ( G e. Mnd /\ A e. X /\ ( M e. NN0 /\ N e. NN0 ) ) -> ( ( O ` A ) || ( M - N ) -> ( M .x. A ) = ( N .x. A ) ) )