mulgz

Description: A group multiple of the identity, for integer multiple. (Contributed by Mario Carneiro, 13-Dec-2014)

	Ref	Expression
Hypotheses	mulgnn0z.b	$⊢ B = {Base}_{G}$
	mulgnn0z.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	mulgnn0z.o	$⊢ \underset{˙}{0} = 0_{G}$
Assertion	mulgz	$⊢ (G \in Grp \land N \in ℤ) \to N \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		mulgnn0z.b	$⊢ B = {Base}_{G}$
2		mulgnn0z.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		mulgnn0z.o	$⊢ \underset{˙}{0} = 0_{G}$
4		grpmnd	$⊢ G \in Grp \to G \in Mnd$
5	4	adantr	$⊢ (G \in Grp \land N \in ℤ) \to G \in Mnd$
6	1 2 3	mulgnn0z	$⊢ (G \in Mnd \land N \in ℕ_{0}) \to N \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
7	5 6	sylan	$⊢ ((G \in Grp \land N \in ℤ) \land N \in ℕ_{0}) \to N \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
8		simpll	$⊢ ((G \in Grp \land N \in ℤ) \land - N \in ℕ_{0}) \to G \in Grp$
9		nn0z	$⊢ - N \in ℕ_{0} \to - N \in ℤ$
10	9	adantl	$⊢ ((G \in Grp \land N \in ℤ) \land - N \in ℕ_{0}) \to - N \in ℤ$
11	1 3	grpidcl	$⊢ G \in Grp \to \underset{˙}{0} \in B$
12	11	ad2antrr	$⊢ ((G \in Grp \land N \in ℤ) \land - N \in ℕ_{0}) \to \underset{˙}{0} \in B$
13		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
14	1 2 13	mulgneg	$⊢ (G \in Grp \land - N \in ℤ \land \underset{˙}{0} \in B) \to (- -N) \underset{˙}{\cdot} \underset{˙}{0} = {inv}_{g} (G) (-N \underset{˙}{\cdot} \underset{˙}{0})$
15	8 10 12 14	syl3anc	$⊢ ((G \in Grp \land N \in ℤ) \land - N \in ℕ_{0}) \to (- -N) \underset{˙}{\cdot} \underset{˙}{0} = {inv}_{g} (G) (-N \underset{˙}{\cdot} \underset{˙}{0})$
16		zcn	$⊢ N \in ℤ \to N \in ℂ$
17	16	ad2antlr	$⊢ ((G \in Grp \land N \in ℤ) \land - N \in ℕ_{0}) \to N \in ℂ$
18	17	negnegd	$⊢ ((G \in Grp \land N \in ℤ) \land - N \in ℕ_{0}) \to - -N = N$
19	18	oveq1d	$⊢ ((G \in Grp \land N \in ℤ) \land - N \in ℕ_{0}) \to (- -N) \underset{˙}{\cdot} \underset{˙}{0} = N \underset{˙}{\cdot} \underset{˙}{0}$
20	1 2 3	mulgnn0z	$⊢ (G \in Mnd \land - N \in ℕ_{0}) \to -N \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
21	5 20	sylan	$⊢ ((G \in Grp \land N \in ℤ) \land - N \in ℕ_{0}) \to -N \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
22	21	fveq2d	$⊢ ((G \in Grp \land N \in ℤ) \land - N \in ℕ_{0}) \to {inv}_{g} (G) (-N \underset{˙}{\cdot} \underset{˙}{0}) = {inv}_{g} (G) (\underset{˙}{0})$
23	3 13	grpinvid	$⊢ G \in Grp \to {inv}_{g} (G) (\underset{˙}{0}) = \underset{˙}{0}$
24	23	ad2antrr	$⊢ ((G \in Grp \land N \in ℤ) \land - N \in ℕ_{0}) \to {inv}_{g} (G) (\underset{˙}{0}) = \underset{˙}{0}$
25	22 24	eqtrd	$⊢ ((G \in Grp \land N \in ℤ) \land - N \in ℕ_{0}) \to {inv}_{g} (G) (-N \underset{˙}{\cdot} \underset{˙}{0}) = \underset{˙}{0}$
26	15 19 25	3eqtr3d	$⊢ ((G \in Grp \land N \in ℤ) \land - N \in ℕ_{0}) \to N \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
27		elznn0	$⊢ N \in ℤ \leftrightarrow (N \in ℝ \land (N \in ℕ_{0} \lor - N \in ℕ_{0}))$
28	27	simprbi	$⊢ N \in ℤ \to (N \in ℕ_{0} \lor - N \in ℕ_{0})$
29	28	adantl	$⊢ (G \in Grp \land N \in ℤ) \to (N \in ℕ_{0} \lor - N \in ℕ_{0})$
30	7 26 29	mpjaodan	$⊢ (G \in Grp \land N \in ℤ) \to N \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$

Metamath Proof Explorer

Theorem mulgz

Proof