mulgnn0p1

Description: Group multiple (exponentiation) operation at a successor, extended to NN0 . (Contributed by Mario Carneiro, 11-Dec-2014)

	Ref	Expression
Hypotheses	mulgnn0p1.b	$⊢ B = {Base}_{G}$
	mulgnn0p1.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	mulgnn0p1.p	$⊢ \underset{˙}{+} = +_{G}$
Assertion	mulgnn0p1	$⊢ (G \in Mnd \land N \in ℕ_{0} \land X \in B) \to (N + 1) \underset{˙}{\cdot} X = (N \underset{˙}{\cdot} X) \underset{˙}{+} X$

Proof

Step	Hyp	Ref	Expression
1		mulgnn0p1.b	$⊢ B = {Base}_{G}$
2		mulgnn0p1.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		mulgnn0p1.p	$⊢ \underset{˙}{+} = +_{G}$
4		simpr	$⊢ ((G \in Mnd \land N \in ℕ_{0} \land X \in B) \land N \in ℕ) \to N \in ℕ$
5		simpl3	$⊢ ((G \in Mnd \land N \in ℕ_{0} \land X \in B) \land N \in ℕ) \to X \in B$
6	1 2 3	mulgnnp1	$⊢ (N \in ℕ \land X \in B) \to (N + 1) \underset{˙}{\cdot} X = (N \underset{˙}{\cdot} X) \underset{˙}{+} X$
7	4 5 6	syl2anc	$⊢ ((G \in Mnd \land N \in ℕ_{0} \land X \in B) \land N \in ℕ) \to (N + 1) \underset{˙}{\cdot} X = (N \underset{˙}{\cdot} X) \underset{˙}{+} X$
8		eqid	$⊢ 0_{G} = 0_{G}$
9	1 3 8	mndlid	$⊢ (G \in Mnd \land X \in B) \to 0_{G} \underset{˙}{+} X = X$
10	1 8 2	mulg0	$⊢ X \in B \to 0 \underset{˙}{\cdot} X = 0_{G}$
11	10	adantl	$⊢ (G \in Mnd \land X \in B) \to 0 \underset{˙}{\cdot} X = 0_{G}$
12	11	oveq1d	$⊢ (G \in Mnd \land X \in B) \to (0 \underset{˙}{\cdot} X) \underset{˙}{+} X = 0_{G} \underset{˙}{+} X$
13	1 2	mulg1	$⊢ X \in B \to 1 \underset{˙}{\cdot} X = X$
14	13	adantl	$⊢ (G \in Mnd \land X \in B) \to 1 \underset{˙}{\cdot} X = X$
15	9 12 14	3eqtr4rd	$⊢ (G \in Mnd \land X \in B) \to 1 \underset{˙}{\cdot} X = (0 \underset{˙}{\cdot} X) \underset{˙}{+} X$
16	15	3adant2	$⊢ (G \in Mnd \land N \in ℕ_{0} \land X \in B) \to 1 \underset{˙}{\cdot} X = (0 \underset{˙}{\cdot} X) \underset{˙}{+} X$
17		oveq1	$⊢ N = 0 \to N + 1 = 0 + 1$
18		1e0p1	$⊢ 1 = 0 + 1$
19	17 18	eqtr4di	$⊢ N = 0 \to N + 1 = 1$
20	19	oveq1d	$⊢ N = 0 \to (N + 1) \underset{˙}{\cdot} X = 1 \underset{˙}{\cdot} X$
21		oveq1	$⊢ N = 0 \to N \underset{˙}{\cdot} X = 0 \underset{˙}{\cdot} X$
22	21	oveq1d	$⊢ N = 0 \to (N \underset{˙}{\cdot} X) \underset{˙}{+} X = (0 \underset{˙}{\cdot} X) \underset{˙}{+} X$
23	20 22	eqeq12d	$⊢ N = 0 \to ((N + 1) \underset{˙}{\cdot} X = (N \underset{˙}{\cdot} X) \underset{˙}{+} X \leftrightarrow 1 \underset{˙}{\cdot} X = (0 \underset{˙}{\cdot} X) \underset{˙}{+} X)$
24	16 23	syl5ibrcom	$⊢ (G \in Mnd \land N \in ℕ_{0} \land X \in B) \to (N = 0 \to (N + 1) \underset{˙}{\cdot} X = (N \underset{˙}{\cdot} X) \underset{˙}{+} X)$
25	24	imp	$⊢ ((G \in Mnd \land N \in ℕ_{0} \land X \in B) \land N = 0) \to (N + 1) \underset{˙}{\cdot} X = (N \underset{˙}{\cdot} X) \underset{˙}{+} X$
26		simp2	$⊢ (G \in Mnd \land N \in ℕ_{0} \land X \in B) \to N \in ℕ_{0}$
27		elnn0	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℕ \lor N = 0)$
28	26 27	sylib	$⊢ (G \in Mnd \land N \in ℕ_{0} \land X \in B) \to (N \in ℕ \lor N = 0)$
29	7 25 28	mpjaodan	$⊢ (G \in Mnd \land N \in ℕ_{0} \land X \in B) \to (N + 1) \underset{˙}{\cdot} X = (N \underset{˙}{\cdot} X) \underset{˙}{+} X$

Metamath Proof Explorer

Theorem mulgnn0p1

Proof