omndmul2

Description: In an ordered monoid, the ordering is compatible with group power. This version does not require the monoid to be commutative. (Contributed by Thierry Arnoux, 23-Mar-2018)

	Ref	Expression
Hypotheses	omndmul.0	$⊢ B = {Base}_{M}$
	omndmul.1	$⊢ \underset{˙}{\leq} = \leq_{M}$
	omndmul2.2	$⊢ \underset{˙}{\cdot} = \cdot_{M}$
	omndmul2.3	$⊢ \underset{˙}{0} = 0_{M}$
Assertion	omndmul2	$⊢ (M \in oMnd \land (X \in B \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \to \underset{˙}{0} \underset{˙}{\leq} (N \underset{˙}{\cdot} X)$

Proof

Step	Hyp	Ref	Expression
1		omndmul.0	$⊢ B = {Base}_{M}$
2		omndmul.1	$⊢ \underset{˙}{\leq} = \leq_{M}$
3		omndmul2.2	$⊢ \underset{˙}{\cdot} = \cdot_{M}$
4		omndmul2.3	$⊢ \underset{˙}{0} = 0_{M}$
5		df-3an	$⊢ (M \in oMnd \land (X \in B \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \leftrightarrow ((M \in oMnd \land (X \in B \land N \in ℕ_{0})) \land \underset{˙}{0} \underset{˙}{\leq} X)$
6		anass	$⊢ ((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \leftrightarrow (M \in oMnd \land (X \in B \land N \in ℕ_{0}))$
7	6	anbi1i	$⊢ (((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \leftrightarrow ((M \in oMnd \land (X \in B \land N \in ℕ_{0})) \land \underset{˙}{0} \underset{˙}{\leq} X)$
8	5 7	bitr4i	$⊢ (M \in oMnd \land (X \in B \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \leftrightarrow (((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X)$
9		simplr	$⊢ (((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \to N \in ℕ_{0}$
10		oveq1	$⊢ m = 0 \to m \underset{˙}{\cdot} X = 0 \underset{˙}{\cdot} X$
11	10	breq2d	$⊢ m = 0 \to (\underset{˙}{0} \underset{˙}{\leq} (m \underset{˙}{\cdot} X) \leftrightarrow \underset{˙}{0} \underset{˙}{\leq} (0 \underset{˙}{\cdot} X))$
12		oveq1	$⊢ m = n \to m \underset{˙}{\cdot} X = n \underset{˙}{\cdot} X$
13	12	breq2d	$⊢ m = n \to (\underset{˙}{0} \underset{˙}{\leq} (m \underset{˙}{\cdot} X) \leftrightarrow \underset{˙}{0} \underset{˙}{\leq} (n \underset{˙}{\cdot} X))$
14		oveq1	$⊢ m = n + 1 \to m \underset{˙}{\cdot} X = (n + 1) \underset{˙}{\cdot} X$
15	14	breq2d	$⊢ m = n + 1 \to (\underset{˙}{0} \underset{˙}{\leq} (m \underset{˙}{\cdot} X) \leftrightarrow \underset{˙}{0} \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} X))$
16		oveq1	$⊢ m = N \to m \underset{˙}{\cdot} X = N \underset{˙}{\cdot} X$
17	16	breq2d	$⊢ m = N \to (\underset{˙}{0} \underset{˙}{\leq} (m \underset{˙}{\cdot} X) \leftrightarrow \underset{˙}{0} \underset{˙}{\leq} (N \underset{˙}{\cdot} X))$
18		omndtos	$⊢ M \in oMnd \to M \in Toset$
19		tospos	$⊢ M \in Toset \to M \in Poset$
20	18 19	syl	$⊢ M \in oMnd \to M \in Poset$
21		omndmnd	$⊢ M \in oMnd \to M \in Mnd$
22	1 4	mndidcl	$⊢ M \in Mnd \to \underset{˙}{0} \in B$
23	21 22	syl	$⊢ M \in oMnd \to \underset{˙}{0} \in B$
24	1 2	posref	$⊢ (M \in Poset \land \underset{˙}{0} \in B) \to \underset{˙}{0} \underset{˙}{\leq} \underset{˙}{0}$
25	20 23 24	syl2anc	$⊢ M \in oMnd \to \underset{˙}{0} \underset{˙}{\leq} \underset{˙}{0}$
26	25	ad3antrrr	$⊢ (((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \to \underset{˙}{0} \underset{˙}{\leq} \underset{˙}{0}$
27	1 4 3	mulg0	$⊢ X \in B \to 0 \underset{˙}{\cdot} X = \underset{˙}{0}$
28	27	ad3antlr	$⊢ (((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \to 0 \underset{˙}{\cdot} X = \underset{˙}{0}$
29	26 28	breqtrrd	$⊢ (((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \to \underset{˙}{0} \underset{˙}{\leq} (0 \underset{˙}{\cdot} X)$
30	20	ad5antr	$⊢ (((((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \land n \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} (n \underset{˙}{\cdot} X)) \to M \in Poset$
31	21	ad5antr	$⊢ (((((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \land n \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} (n \underset{˙}{\cdot} X)) \to M \in Mnd$
32	31 22	syl	$⊢ (((((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \land n \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} (n \underset{˙}{\cdot} X)) \to \underset{˙}{0} \in B$
33		simplr	$⊢ (((((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \land n \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} (n \underset{˙}{\cdot} X)) \to n \in ℕ_{0}$
34		simp-5r	$⊢ (((((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \land n \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} (n \underset{˙}{\cdot} X)) \to X \in B$
35	1 3	mulgnn0cl	$⊢ (M \in Mnd \land n \in ℕ_{0} \land X \in B) \to n \underset{˙}{\cdot} X \in B$
36	31 33 34 35	syl3anc	$⊢ (((((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \land n \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} (n \underset{˙}{\cdot} X)) \to n \underset{˙}{\cdot} X \in B$
37		simpr32	$⊢ (M \in oMnd \land (X \in B \land N \in ℕ_{0} \land (\underset{˙}{0} \underset{˙}{\leq} X \land n \in ℕ_{0} \land \underset{˙}{0} \underset{˙}{\leq} (n \underset{˙}{\cdot} X)))) \to n \in ℕ_{0}$
38		1nn0	$⊢ 1 \in ℕ_{0}$
39	38	a1i	$⊢ (M \in oMnd \land (X \in B \land N \in ℕ_{0} \land (\underset{˙}{0} \underset{˙}{\leq} X \land n \in ℕ_{0} \land \underset{˙}{0} \underset{˙}{\leq} (n \underset{˙}{\cdot} X)))) \to 1 \in ℕ_{0}$
40	37 39	nn0addcld	$⊢ (M \in oMnd \land (X \in B \land N \in ℕ_{0} \land (\underset{˙}{0} \underset{˙}{\leq} X \land n \in ℕ_{0} \land \underset{˙}{0} \underset{˙}{\leq} (n \underset{˙}{\cdot} X)))) \to n + 1 \in ℕ_{0}$
41	40	3anassrs	$⊢ (((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land (\underset{˙}{0} \underset{˙}{\leq} X \land n \in ℕ_{0} \land \underset{˙}{0} \underset{˙}{\leq} (n \underset{˙}{\cdot} X))) \to n + 1 \in ℕ_{0}$
42	41	3anassrs	$⊢ (((((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \land n \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} (n \underset{˙}{\cdot} X)) \to n + 1 \in ℕ_{0}$
43	1 3	mulgnn0cl	$⊢ (M \in Mnd \land n + 1 \in ℕ_{0} \land X \in B) \to (n + 1) \underset{˙}{\cdot} X \in B$
44	31 42 34 43	syl3anc	$⊢ (((((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \land n \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} (n \underset{˙}{\cdot} X)) \to (n + 1) \underset{˙}{\cdot} X \in B$
45	32 36 44	3jca	$⊢ (((((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \land n \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} (n \underset{˙}{\cdot} X)) \to (\underset{˙}{0} \in B \land n \underset{˙}{\cdot} X \in B \land (n + 1) \underset{˙}{\cdot} X \in B)$
46		simpr	$⊢ (((((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \land n \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} (n \underset{˙}{\cdot} X)) \to \underset{˙}{0} \underset{˙}{\leq} (n \underset{˙}{\cdot} X)$
47		simp-4l	$⊢ ((((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \land n \in ℕ_{0}) \to M \in oMnd$
48	21	ad4antr	$⊢ ((((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \land n \in ℕ_{0}) \to M \in Mnd$
49	48 22	syl	$⊢ ((((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \land n \in ℕ_{0}) \to \underset{˙}{0} \in B$
50		simp-4r	$⊢ ((((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \land n \in ℕ_{0}) \to X \in B$
51		simpr	$⊢ ((((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \land n \in ℕ_{0}) \to n \in ℕ_{0}$
52	48 51 50 35	syl3anc	$⊢ ((((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \land n \in ℕ_{0}) \to n \underset{˙}{\cdot} X \in B$
53		simplr	$⊢ ((((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \land n \in ℕ_{0}) \to \underset{˙}{0} \underset{˙}{\leq} X$
54		eqid	$⊢ +_{M} = +_{M}$
55	1 2 54	omndadd	$⊢ (M \in oMnd \land (\underset{˙}{0} \in B \land X \in B \land n \underset{˙}{\cdot} X \in B) \land \underset{˙}{0} \underset{˙}{\leq} X) \to (\underset{˙}{0} +_{M} (n \underset{˙}{\cdot} X)) \underset{˙}{\leq} (X +_{M} (n \underset{˙}{\cdot} X))$
56	47 49 50 52 53 55	syl131anc	$⊢ ((((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \land n \in ℕ_{0}) \to (\underset{˙}{0} +_{M} (n \underset{˙}{\cdot} X)) \underset{˙}{\leq} (X +_{M} (n \underset{˙}{\cdot} X))$
57	1 54 4	mndlid	$⊢ (M \in Mnd \land n \underset{˙}{\cdot} X \in B) \to \underset{˙}{0} +_{M} (n \underset{˙}{\cdot} X) = n \underset{˙}{\cdot} X$
58	48 52 57	syl2anc	$⊢ ((((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \land n \in ℕ_{0}) \to \underset{˙}{0} +_{M} (n \underset{˙}{\cdot} X) = n \underset{˙}{\cdot} X$
59	38	a1i	$⊢ ((((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \land n \in ℕ_{0}) \to 1 \in ℕ_{0}$
60	1 3 54	mulgnn0dir	$⊢ (M \in Mnd \land (1 \in ℕ_{0} \land n \in ℕ_{0} \land X \in B)) \to (1 + n) \underset{˙}{\cdot} X = (1 \underset{˙}{\cdot} X) +_{M} (n \underset{˙}{\cdot} X)$
61	48 59 51 50 60	syl13anc	$⊢ ((((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \land n \in ℕ_{0}) \to (1 + n) \underset{˙}{\cdot} X = (1 \underset{˙}{\cdot} X) +_{M} (n \underset{˙}{\cdot} X)$
62		1cnd	$⊢ ((M \in oMnd \land X \in B) \land (N \in ℕ_{0} \land \underset{˙}{0} \underset{˙}{\leq} X \land n \in ℕ_{0})) \to 1 \in ℂ$
63		simpr3	$⊢ ((M \in oMnd \land X \in B) \land (N \in ℕ_{0} \land \underset{˙}{0} \underset{˙}{\leq} X \land n \in ℕ_{0})) \to n \in ℕ_{0}$
64	63	nn0cnd	$⊢ ((M \in oMnd \land X \in B) \land (N \in ℕ_{0} \land \underset{˙}{0} \underset{˙}{\leq} X \land n \in ℕ_{0})) \to n \in ℂ$
65	62 64	addcomd	$⊢ ((M \in oMnd \land X \in B) \land (N \in ℕ_{0} \land \underset{˙}{0} \underset{˙}{\leq} X \land n \in ℕ_{0})) \to 1 + n = n + 1$
66	65	3anassrs	$⊢ ((((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \land n \in ℕ_{0}) \to 1 + n = n + 1$
67	66	oveq1d	$⊢ ((((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \land n \in ℕ_{0}) \to (1 + n) \underset{˙}{\cdot} X = (n + 1) \underset{˙}{\cdot} X$
68	1 3	mulg1	$⊢ X \in B \to 1 \underset{˙}{\cdot} X = X$
69	50 68	syl	$⊢ ((((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \land n \in ℕ_{0}) \to 1 \underset{˙}{\cdot} X = X$
70	69	oveq1d	$⊢ ((((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \land n \in ℕ_{0}) \to (1 \underset{˙}{\cdot} X) +_{M} (n \underset{˙}{\cdot} X) = X +_{M} (n \underset{˙}{\cdot} X)$
71	61 67 70	3eqtr3rd	$⊢ ((((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \land n \in ℕ_{0}) \to X +_{M} (n \underset{˙}{\cdot} X) = (n + 1) \underset{˙}{\cdot} X$
72	56 58 71	3brtr3d	$⊢ ((((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \land n \in ℕ_{0}) \to (n \underset{˙}{\cdot} X) \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} X)$
73	72	adantr	$⊢ (((((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \land n \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} (n \underset{˙}{\cdot} X)) \to (n \underset{˙}{\cdot} X) \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} X)$
74	1 2	postr	$⊢ (M \in Poset \land (\underset{˙}{0} \in B \land n \underset{˙}{\cdot} X \in B \land (n + 1) \underset{˙}{\cdot} X \in B)) \to ((\underset{˙}{0} \underset{˙}{\leq} (n \underset{˙}{\cdot} X) \land (n \underset{˙}{\cdot} X) \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} X)) \to \underset{˙}{0} \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} X))$
75	74	imp	$⊢ ((M \in Poset \land (\underset{˙}{0} \in B \land n \underset{˙}{\cdot} X \in B \land (n + 1) \underset{˙}{\cdot} X \in B)) \land (\underset{˙}{0} \underset{˙}{\leq} (n \underset{˙}{\cdot} X) \land (n \underset{˙}{\cdot} X) \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} X))) \to \underset{˙}{0} \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} X)$
76	30 45 46 73 75	syl22anc	$⊢ (((((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \land n \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} (n \underset{˙}{\cdot} X)) \to \underset{˙}{0} \underset{˙}{\leq} ((n + 1) \underset{˙}{\cdot} X)$
77	11 13 15 17 29 76	nn0indd	$⊢ ((((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \land N \in ℕ_{0}) \to \underset{˙}{0} \underset{˙}{\leq} (N \underset{˙}{\cdot} X)$
78	9 77	mpdan	$⊢ (((M \in oMnd \land X \in B) \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \to \underset{˙}{0} \underset{˙}{\leq} (N \underset{˙}{\cdot} X)$
79	8 78	sylbi	$⊢ (M \in oMnd \land (X \in B \land N \in ℕ_{0}) \land \underset{˙}{0} \underset{˙}{\leq} X) \to \underset{˙}{0} \underset{˙}{\leq} (N \underset{˙}{\cdot} X)$

Metamath Proof Explorer

Theorem omndmul2

Proof