ghmmulg

Description: A group homomorphism preserves group multiples. (Contributed by Mario Carneiro, 14-Jun-2015)

	Ref	Expression
Hypotheses	ghmmulg.b	$⊢ B = {Base}_{G}$
	ghmmulg.s	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	ghmmulg.t	$⊢ \underset{˙}{\times} = \cdot_{H}$
Assertion	ghmmulg	$⊢ (F \in (G GrpHom H) \land N \in ℤ \land X \in B) \to F (N \underset{˙}{\cdot} X) = N \underset{˙}{\times} F (X)$

Proof

Step	Hyp	Ref	Expression
1		ghmmulg.b	$⊢ B = {Base}_{G}$
2		ghmmulg.s	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		ghmmulg.t	$⊢ \underset{˙}{\times} = \cdot_{H}$
4		ghmmhm	$⊢ F \in (G GrpHom H) \to F \in (G MndHom H)$
5	1 2 3	mhmmulg	$⊢ (F \in (G MndHom H) \land N \in ℕ_{0} \land X \in B) \to F (N \underset{˙}{\cdot} X) = N \underset{˙}{\times} F (X)$
6	4 5	syl3an1	$⊢ (F \in (G GrpHom H) \land N \in ℕ_{0} \land X \in B) \to F (N \underset{˙}{\cdot} X) = N \underset{˙}{\times} F (X)$
7	6	3expa	$⊢ ((F \in (G GrpHom H) \land N \in ℕ_{0}) \land X \in B) \to F (N \underset{˙}{\cdot} X) = N \underset{˙}{\times} F (X)$
8	7	an32s	$⊢ ((F \in (G GrpHom H) \land X \in B) \land N \in ℕ_{0}) \to F (N \underset{˙}{\cdot} X) = N \underset{˙}{\times} F (X)$
9	8	3adantl2	$⊢ ((F \in (G GrpHom H) \land N \in ℤ \land X \in B) \land N \in ℕ_{0}) \to F (N \underset{˙}{\cdot} X) = N \underset{˙}{\times} F (X)$
10		simpl1	$⊢ ((F \in (G GrpHom H) \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to F \in (G GrpHom H)$
11	10 4	syl	$⊢ ((F \in (G GrpHom H) \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to F \in (G MndHom H)$
12		nnnn0	$⊢ - N \in ℕ \to - N \in ℕ_{0}$
13	12	ad2antll	$⊢ ((F \in (G GrpHom H) \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to - N \in ℕ_{0}$
14		simpl3	$⊢ ((F \in (G GrpHom H) \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to X \in B$
15	1 2 3	mhmmulg	$⊢ (F \in (G MndHom H) \land - N \in ℕ_{0} \land X \in B) \to F (-N \underset{˙}{\cdot} X) = -N \underset{˙}{\times} F (X)$
16	11 13 14 15	syl3anc	$⊢ ((F \in (G GrpHom H) \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to F (-N \underset{˙}{\cdot} X) = -N \underset{˙}{\times} F (X)$
17	16	fveq2d	$⊢ ((F \in (G GrpHom H) \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to {inv}_{g} (H) (F (-N \underset{˙}{\cdot} X)) = {inv}_{g} (H) (-N \underset{˙}{\times} F (X))$
18		ghmgrp1	$⊢ F \in (G GrpHom H) \to G \in Grp$
19	10 18	syl	$⊢ ((F \in (G GrpHom H) \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to G \in Grp$
20		nnz	$⊢ - N \in ℕ \to - N \in ℤ$
21	20	ad2antll	$⊢ ((F \in (G GrpHom H) \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to - N \in ℤ$
22	1 2	mulgcl	$⊢ (G \in Grp \land - N \in ℤ \land X \in B) \to -N \underset{˙}{\cdot} X \in B$
23	19 21 14 22	syl3anc	$⊢ ((F \in (G GrpHom H) \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to -N \underset{˙}{\cdot} X \in B$
24		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
25		eqid	$⊢ {inv}_{g} (H) = {inv}_{g} (H)$
26	1 24 25	ghminv	$⊢ (F \in (G GrpHom H) \land -N \underset{˙}{\cdot} X \in B) \to F ({inv}_{g} (G) (-N \underset{˙}{\cdot} X)) = {inv}_{g} (H) (F (-N \underset{˙}{\cdot} X))$
27	10 23 26	syl2anc	$⊢ ((F \in (G GrpHom H) \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to F ({inv}_{g} (G) (-N \underset{˙}{\cdot} X)) = {inv}_{g} (H) (F (-N \underset{˙}{\cdot} X))$
28		ghmgrp2	$⊢ F \in (G GrpHom H) \to H \in Grp$
29	10 28	syl	$⊢ ((F \in (G GrpHom H) \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to H \in Grp$
30		eqid	$⊢ {Base}_{H} = {Base}_{H}$
31	1 30	ghmf	$⊢ F \in (G GrpHom H) \to F : B ⟶ {Base}_{H}$
32	10 31	syl	$⊢ ((F \in (G GrpHom H) \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to F : B ⟶ {Base}_{H}$
33	32 14	ffvelcdmd	$⊢ ((F \in (G GrpHom H) \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to F (X) \in {Base}_{H}$
34	30 3 25	mulgneg	$⊢ (H \in Grp \land - N \in ℤ \land F (X) \in {Base}_{H}) \to (- -N) \underset{˙}{\times} F (X) = {inv}_{g} (H) (-N \underset{˙}{\times} F (X))$
35	29 21 33 34	syl3anc	$⊢ ((F \in (G GrpHom H) \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to (- -N) \underset{˙}{\times} F (X) = {inv}_{g} (H) (-N \underset{˙}{\times} F (X))$
36	17 27 35	3eqtr4d	$⊢ ((F \in (G GrpHom H) \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to F ({inv}_{g} (G) (-N \underset{˙}{\cdot} X)) = (- -N) \underset{˙}{\times} F (X)$
37	1 2 24	mulgneg	$⊢ (G \in Grp \land - N \in ℤ \land X \in B) \to (- -N) \underset{˙}{\cdot} X = {inv}_{g} (G) (-N \underset{˙}{\cdot} X)$
38	19 21 14 37	syl3anc	$⊢ ((F \in (G GrpHom H) \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to (- -N) \underset{˙}{\cdot} X = {inv}_{g} (G) (-N \underset{˙}{\cdot} X)$
39		simprl	$⊢ ((F \in (G GrpHom H) \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to N \in ℝ$
40	39	recnd	$⊢ ((F \in (G GrpHom H) \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to N \in ℂ$
41	40	negnegd	$⊢ ((F \in (G GrpHom H) \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to - -N = N$
42	41	oveq1d	$⊢ ((F \in (G GrpHom H) \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to (- -N) \underset{˙}{\cdot} X = N \underset{˙}{\cdot} X$
43	38 42	eqtr3d	$⊢ ((F \in (G GrpHom H) \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to {inv}_{g} (G) (-N \underset{˙}{\cdot} X) = N \underset{˙}{\cdot} X$
44	43	fveq2d	$⊢ ((F \in (G GrpHom H) \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to F ({inv}_{g} (G) (-N \underset{˙}{\cdot} X)) = F (N \underset{˙}{\cdot} X)$
45	36 44	eqtr3d	$⊢ ((F \in (G GrpHom H) \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to (- -N) \underset{˙}{\times} F (X) = F (N \underset{˙}{\cdot} X)$
46	41	oveq1d	$⊢ ((F \in (G GrpHom H) \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to (- -N) \underset{˙}{\times} F (X) = N \underset{˙}{\times} F (X)$
47	45 46	eqtr3d	$⊢ ((F \in (G GrpHom H) \land N \in ℤ \land X \in B) \land (N \in ℝ \land - N \in ℕ)) \to F (N \underset{˙}{\cdot} X) = N \underset{˙}{\times} F (X)$
48		simp2	$⊢ (F \in (G GrpHom H) \land N \in ℤ \land X \in B) \to N \in ℤ$
49		elznn0nn	$⊢ N \in ℤ \leftrightarrow (N \in ℕ_{0} \lor (N \in ℝ \land - N \in ℕ))$
50	48 49	sylib	$⊢ (F \in (G GrpHom H) \land N \in ℤ \land X \in B) \to (N \in ℕ_{0} \lor (N \in ℝ \land - N \in ℕ))$
51	9 47 50	mpjaodan	$⊢ (F \in (G GrpHom H) \land N \in ℤ \land X \in B) \to F (N \underset{˙}{\cdot} X) = N \underset{˙}{\times} F (X)$

Metamath Proof Explorer

Theorem ghmmulg

Proof