mhmmulg

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

	Ref	Expression
Hypotheses	mhmmulg.b	$⊢ B = {Base}_{G}$
	mhmmulg.s	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	mhmmulg.t	$⊢ \underset{˙}{\times} = \cdot_{H}$
Assertion	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)$

Proof

Step	Hyp	Ref	Expression
1		mhmmulg.b	$⊢ B = {Base}_{G}$
2		mhmmulg.s	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		mhmmulg.t	$⊢ \underset{˙}{\times} = \cdot_{H}$
4		fvoveq1	$⊢ n = 0 \to F (n \underset{˙}{\cdot} X) = F (0 \underset{˙}{\cdot} X)$
5		oveq1	$⊢ n = 0 \to n \underset{˙}{\times} F (X) = 0 \underset{˙}{\times} F (X)$
6	4 5	eqeq12d	$⊢ n = 0 \to (F (n \underset{˙}{\cdot} X) = n \underset{˙}{\times} F (X) \leftrightarrow F (0 \underset{˙}{\cdot} X) = 0 \underset{˙}{\times} F (X))$
7	6	imbi2d	$⊢ n = 0 \to (((F \in (G MndHom H) \land X \in B) \to F (n \underset{˙}{\cdot} X) = n \underset{˙}{\times} F (X)) \leftrightarrow ((F \in (G MndHom H) \land X \in B) \to F (0 \underset{˙}{\cdot} X) = 0 \underset{˙}{\times} F (X)))$
8		fvoveq1	$⊢ n = m \to F (n \underset{˙}{\cdot} X) = F (m \underset{˙}{\cdot} X)$
9		oveq1	$⊢ n = m \to n \underset{˙}{\times} F (X) = m \underset{˙}{\times} F (X)$
10	8 9	eqeq12d	$⊢ n = m \to (F (n \underset{˙}{\cdot} X) = n \underset{˙}{\times} F (X) \leftrightarrow F (m \underset{˙}{\cdot} X) = m \underset{˙}{\times} F (X))$
11	10	imbi2d	$⊢ n = m \to (((F \in (G MndHom H) \land X \in B) \to F (n \underset{˙}{\cdot} X) = n \underset{˙}{\times} F (X)) \leftrightarrow ((F \in (G MndHom H) \land X \in B) \to F (m \underset{˙}{\cdot} X) = m \underset{˙}{\times} F (X)))$
12		fvoveq1	$⊢ n = m + 1 \to F (n \underset{˙}{\cdot} X) = F ((m + 1) \underset{˙}{\cdot} X)$
13		oveq1	$⊢ n = m + 1 \to n \underset{˙}{\times} F (X) = (m + 1) \underset{˙}{\times} F (X)$
14	12 13	eqeq12d	$⊢ n = m + 1 \to (F (n \underset{˙}{\cdot} X) = n \underset{˙}{\times} F (X) \leftrightarrow F ((m + 1) \underset{˙}{\cdot} X) = (m + 1) \underset{˙}{\times} F (X))$
15	14	imbi2d	$⊢ n = m + 1 \to (((F \in (G MndHom H) \land X \in B) \to F (n \underset{˙}{\cdot} X) = n \underset{˙}{\times} F (X)) \leftrightarrow ((F \in (G MndHom H) \land X \in B) \to F ((m + 1) \underset{˙}{\cdot} X) = (m + 1) \underset{˙}{\times} F (X)))$
16		fvoveq1	$⊢ n = N \to F (n \underset{˙}{\cdot} X) = F (N \underset{˙}{\cdot} X)$
17		oveq1	$⊢ n = N \to n \underset{˙}{\times} F (X) = N \underset{˙}{\times} F (X)$
18	16 17	eqeq12d	$⊢ n = N \to (F (n \underset{˙}{\cdot} X) = n \underset{˙}{\times} F (X) \leftrightarrow F (N \underset{˙}{\cdot} X) = N \underset{˙}{\times} F (X))$
19	18	imbi2d	$⊢ n = N \to (((F \in (G MndHom H) \land X \in B) \to F (n \underset{˙}{\cdot} X) = n \underset{˙}{\times} F (X)) \leftrightarrow ((F \in (G MndHom H) \land X \in B) \to F (N \underset{˙}{\cdot} X) = N \underset{˙}{\times} F (X)))$
20		eqid	$⊢ 0_{G} = 0_{G}$
21		eqid	$⊢ 0_{H} = 0_{H}$
22	20 21	mhm0	$⊢ F \in (G MndHom H) \to F (0_{G}) = 0_{H}$
23	22	adantr	$⊢ (F \in (G MndHom H) \land X \in B) \to F (0_{G}) = 0_{H}$
24	1 20 2	mulg0	$⊢ X \in B \to 0 \underset{˙}{\cdot} X = 0_{G}$
25	24	adantl	$⊢ (F \in (G MndHom H) \land X \in B) \to 0 \underset{˙}{\cdot} X = 0_{G}$
26	25	fveq2d	$⊢ (F \in (G MndHom H) \land X \in B) \to F (0 \underset{˙}{\cdot} X) = F (0_{G})$
27		eqid	$⊢ {Base}_{H} = {Base}_{H}$
28	1 27	mhmf	$⊢ F \in (G MndHom H) \to F : B ⟶ {Base}_{H}$
29	28	ffvelrnda	$⊢ (F \in (G MndHom H) \land X \in B) \to F (X) \in {Base}_{H}$
30	27 21 3	mulg0	$⊢ F (X) \in {Base}_{H} \to 0 \underset{˙}{\times} F (X) = 0_{H}$
31	29 30	syl	$⊢ (F \in (G MndHom H) \land X \in B) \to 0 \underset{˙}{\times} F (X) = 0_{H}$
32	23 26 31	3eqtr4d	$⊢ (F \in (G MndHom H) \land X \in B) \to F (0 \underset{˙}{\cdot} X) = 0 \underset{˙}{\times} F (X)$
33		oveq1	$⊢ F (m \underset{˙}{\cdot} X) = m \underset{˙}{\times} F (X) \to F (m \underset{˙}{\cdot} X) +_{H} F (X) = (m \underset{˙}{\times} F (X)) +_{H} F (X)$
34		mhmrcl1	$⊢ F \in (G MndHom H) \to G \in Mnd$
35	34	ad2antrr	$⊢ ((F \in (G MndHom H) \land X \in B) \land m \in ℕ_{0}) \to G \in Mnd$
36		simpr	$⊢ ((F \in (G MndHom H) \land X \in B) \land m \in ℕ_{0}) \to m \in ℕ_{0}$
37		simplr	$⊢ ((F \in (G MndHom H) \land X \in B) \land m \in ℕ_{0}) \to X \in B$
38		eqid	$⊢ +_{G} = +_{G}$
39	1 2 38	mulgnn0p1	$⊢ (G \in Mnd \land m \in ℕ_{0} \land X \in B) \to (m + 1) \underset{˙}{\cdot} X = (m \underset{˙}{\cdot} X) +_{G} X$
40	35 36 37 39	syl3anc	$⊢ ((F \in (G MndHom H) \land X \in B) \land m \in ℕ_{0}) \to (m + 1) \underset{˙}{\cdot} X = (m \underset{˙}{\cdot} X) +_{G} X$
41	40	fveq2d	$⊢ ((F \in (G MndHom H) \land X \in B) \land m \in ℕ_{0}) \to F ((m + 1) \underset{˙}{\cdot} X) = F ((m \underset{˙}{\cdot} X) +_{G} X)$
42		simpll	$⊢ ((F \in (G MndHom H) \land X \in B) \land m \in ℕ_{0}) \to F \in (G MndHom H)$
43	34	ad2antrr	$⊢ ((F \in (G MndHom H) \land m \in ℕ_{0}) \land X \in B) \to G \in Mnd$
44		simplr	$⊢ ((F \in (G MndHom H) \land m \in ℕ_{0}) \land X \in B) \to m \in ℕ_{0}$
45		simpr	$⊢ ((F \in (G MndHom H) \land m \in ℕ_{0}) \land X \in B) \to X \in B$
46	1 2	mulgnn0cl	$⊢ (G \in Mnd \land m \in ℕ_{0} \land X \in B) \to m \underset{˙}{\cdot} X \in B$
47	43 44 45 46	syl3anc	$⊢ ((F \in (G MndHom H) \land m \in ℕ_{0}) \land X \in B) \to m \underset{˙}{\cdot} X \in B$
48	47	an32s	$⊢ ((F \in (G MndHom H) \land X \in B) \land m \in ℕ_{0}) \to m \underset{˙}{\cdot} X \in B$
49		eqid	$⊢ +_{H} = +_{H}$
50	1 38 49	mhmlin	$⊢ (F \in (G MndHom H) \land m \underset{˙}{\cdot} X \in B \land X \in B) \to F ((m \underset{˙}{\cdot} X) +_{G} X) = F (m \underset{˙}{\cdot} X) +_{H} F (X)$
51	42 48 37 50	syl3anc	$⊢ ((F \in (G MndHom H) \land X \in B) \land m \in ℕ_{0}) \to F ((m \underset{˙}{\cdot} X) +_{G} X) = F (m \underset{˙}{\cdot} X) +_{H} F (X)$
52	41 51	eqtrd	$⊢ ((F \in (G MndHom H) \land X \in B) \land m \in ℕ_{0}) \to F ((m + 1) \underset{˙}{\cdot} X) = F (m \underset{˙}{\cdot} X) +_{H} F (X)$
53		mhmrcl2	$⊢ F \in (G MndHom H) \to H \in Mnd$
54	53	ad2antrr	$⊢ ((F \in (G MndHom H) \land X \in B) \land m \in ℕ_{0}) \to H \in Mnd$
55	29	adantr	$⊢ ((F \in (G MndHom H) \land X \in B) \land m \in ℕ_{0}) \to F (X) \in {Base}_{H}$
56	27 3 49	mulgnn0p1	$⊢ (H \in Mnd \land m \in ℕ_{0} \land F (X) \in {Base}_{H}) \to (m + 1) \underset{˙}{\times} F (X) = (m \underset{˙}{\times} F (X)) +_{H} F (X)$
57	54 36 55 56	syl3anc	$⊢ ((F \in (G MndHom H) \land X \in B) \land m \in ℕ_{0}) \to (m + 1) \underset{˙}{\times} F (X) = (m \underset{˙}{\times} F (X)) +_{H} F (X)$
58	52 57	eqeq12d	$⊢ ((F \in (G MndHom H) \land X \in B) \land m \in ℕ_{0}) \to (F ((m + 1) \underset{˙}{\cdot} X) = (m + 1) \underset{˙}{\times} F (X) \leftrightarrow F (m \underset{˙}{\cdot} X) +_{H} F (X) = (m \underset{˙}{\times} F (X)) +_{H} F (X))$
59	33 58	syl5ibr	$⊢ ((F \in (G MndHom H) \land X \in B) \land m \in ℕ_{0}) \to (F (m \underset{˙}{\cdot} X) = m \underset{˙}{\times} F (X) \to F ((m + 1) \underset{˙}{\cdot} X) = (m + 1) \underset{˙}{\times} F (X))$
60	59	expcom	$⊢ m \in ℕ_{0} \to ((F \in (G MndHom H) \land X \in B) \to (F (m \underset{˙}{\cdot} X) = m \underset{˙}{\times} F (X) \to F ((m + 1) \underset{˙}{\cdot} X) = (m + 1) \underset{˙}{\times} F (X)))$
61	60	a2d	$⊢ m \in ℕ_{0} \to (((F \in (G MndHom H) \land X \in B) \to F (m \underset{˙}{\cdot} X) = m \underset{˙}{\times} F (X)) \to ((F \in (G MndHom H) \land X \in B) \to F ((m + 1) \underset{˙}{\cdot} X) = (m + 1) \underset{˙}{\times} F (X)))$
62	7 11 15 19 32 61	nn0ind	$⊢ N \in ℕ_{0} \to ((F \in (G MndHom H) \land X \in B) \to F (N \underset{˙}{\cdot} X) = N \underset{˙}{\times} F (X))$
63	62	3impib	$⊢ (N \in ℕ_{0} \land F \in (G MndHom H) \land X \in B) \to F (N \underset{˙}{\cdot} X) = N \underset{˙}{\times} F (X)$
64	63	3com12	$⊢ (F \in (G MndHom H) \land N \in ℕ_{0} \land X \in B) \to F (N \underset{˙}{\cdot} X) = N \underset{˙}{\times} F (X)$

Metamath Proof Explorer

Theorem mhmmulg

Proof