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	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	cycsubmcom.f	$⊢ F = (x \in ℕ_{0} ⟼ x \underset{˙}{\cdot} A)$
	cycsubmcom.c	$⊢ C = ran F$
	cycsubmcom.p	$⊢ \underset{˙}{+} = +_{G}$
Assertion	cycsubmcom	$⊢ ((G \in Mnd \land A \in B) \land (X \in C \land Y \in C)) \to X \underset{˙}{+} Y = Y \underset{˙}{+} X$

Proof

Step	Hyp	Ref	Expression
1		cycsubmcom.b	$⊢ B = {Base}_{G}$
2		cycsubmcom.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		cycsubmcom.f	$⊢ F = (x \in ℕ_{0} ⟼ x \underset{˙}{\cdot} A)$
4		cycsubmcom.c	$⊢ C = ran F$
5		cycsubmcom.p	$⊢ \underset{˙}{+} = +_{G}$
6	1 2 3 4	cycsubmel	$⊢ c \in C \leftrightarrow \exists i \in ℕ_{0} c = i \underset{˙}{\cdot} A$
7	6	biimpi	$⊢ c \in C \to \exists i \in ℕ_{0} c = i \underset{˙}{\cdot} A$
8	7	adantl	$⊢ (((G \in Mnd \land A \in B) \land (X \in C \land Y \in C)) \land c \in C) \to \exists i \in ℕ_{0} c = i \underset{˙}{\cdot} A$
9	8	ralrimiva	$⊢ ((G \in Mnd \land A \in B) \land (X \in C \land Y \in C)) \to \forall c \in C \exists i \in ℕ_{0} c = i \underset{˙}{\cdot} A$
10		simplll	$⊢ (((G \in Mnd \land A \in B) \land (X \in C \land Y \in C)) \land (m \in ℕ_{0} \land n \in ℕ_{0})) \to G \in Mnd$
11		simprl	$⊢ (((G \in Mnd \land A \in B) \land (X \in C \land Y \in C)) \land (m \in ℕ_{0} \land n \in ℕ_{0})) \to m \in ℕ_{0}$
12		simprr	$⊢ (((G \in Mnd \land A \in B) \land (X \in C \land Y \in C)) \land (m \in ℕ_{0} \land n \in ℕ_{0})) \to n \in ℕ_{0}$
13		simpllr	$⊢ (((G \in Mnd \land A \in B) \land (X \in C \land Y \in C)) \land (m \in ℕ_{0} \land n \in ℕ_{0})) \to A \in B$
14	1 2 5	mulgnn0dir	$⊢ (G \in Mnd \land (m \in ℕ_{0} \land n \in ℕ_{0} \land A \in B)) \to (m + n) \underset{˙}{\cdot} A = (m \underset{˙}{\cdot} A) \underset{˙}{+} (n \underset{˙}{\cdot} A)$
15	10 11 12 13 14	syl13anc	$⊢ (((G \in Mnd \land A \in B) \land (X \in C \land Y \in C)) \land (m \in ℕ_{0} \land n \in ℕ_{0})) \to (m + n) \underset{˙}{\cdot} A = (m \underset{˙}{\cdot} A) \underset{˙}{+} (n \underset{˙}{\cdot} A)$
16	15	ralrimivva	$⊢ ((G \in Mnd \land A \in B) \land (X \in C \land Y \in C)) \to \forall m \in ℕ_{0} \forall n \in ℕ_{0} (m + n) \underset{˙}{\cdot} A = (m \underset{˙}{\cdot} A) \underset{˙}{+} (n \underset{˙}{\cdot} A)$
17		simprl	$⊢ ((G \in Mnd \land A \in B) \land (X \in C \land Y \in C)) \to X \in C$
18		simprr	$⊢ ((G \in Mnd \land A \in B) \land (X \in C \land Y \in C)) \to Y \in C$
19		nn0sscn	$⊢ ℕ_{0} \subseteq ℂ$
20	19	a1i	$⊢ ((G \in Mnd \land A \in B) \land (X \in C \land Y \in C)) \to ℕ_{0} \subseteq ℂ$
21	9 16 17 18 20	cyccom	$⊢ ((G \in Mnd \land A \in B) \land (X \in C \land Y \in C)) \to X \underset{˙}{+} Y = Y \underset{˙}{+} X$

Metamath Proof Explorer

Theorem cycsubmcom

Proof