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 31 33 34	mulgnn0cld	$⊢ (((((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$
36		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}$
37		1nn0	$⊢ 1 \in ℕ_{0}$
38	37	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}$
39	36 38	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}$
40	39	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}$
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	1 3 31 41 34	mulgnn0cld	$⊢ (((((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$
43	32 35 42	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)$
44		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)$
45		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$
46	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$
47	46 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$
48		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$
49		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}$
50	1 3 46 49 48	mulgnn0cld	$⊢ ((((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$
51		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$
52		eqid	$⊢ +_{M} = +_{M}$
53	1 2 52	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))$
54	45 47 48 50 51 53	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))$
55	1 52 4	mndlid	$⊢ (M \in Mnd \land n \underset{˙}{\cdot} X \in B) \to \underset{˙}{0} +_{M} (n \underset{˙}{\cdot} X) = n \underset{˙}{\cdot} X$
56	46 50 55	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$
57	37	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}$
58	1 3 52	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)$
59	46 57 49 48 58	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)$
60		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 ℂ$
61		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}$
62	61	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 ℂ$
63	60 62	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$
64	63	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$
65	64	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$
66	1 3	mulg1	$⊢ X \in B \to 1 \underset{˙}{\cdot} X = X$
67	48 66	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$
68	67	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)$
69	59 65 68	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$
70	54 56 69	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)$
71	70	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)$
72	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))$
73	72	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)$
74	30 43 44 71 73	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)$
75	11 13 15 17 29 74	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)$
76	9 75	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)$
77	8 76	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