mulgnn0ass

Description: Product of group multiples, generalized to NN0 . (Contributed by Mario Carneiro, 13-Dec-2014)

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

Proof

Step	Hyp	Ref	Expression
1		mulgass.b	$⊢ B = {Base}_{G}$
2		mulgass.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		mndsgrp	$⊢ G \in Mnd \to G \in Smgrp$
4	3	adantr	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to G \in Smgrp$
5	4	adantr	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land (M \in ℕ \land N \in ℕ)) \to G \in Smgrp$
6		simprl	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land (M \in ℕ \land N \in ℕ)) \to M \in ℕ$
7		simprr	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land (M \in ℕ \land N \in ℕ)) \to N \in ℕ$
8		simpr3	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to X \in B$
9	8	adantr	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land (M \in ℕ \land N \in ℕ)) \to X \in B$
10	1 2	mulgnnass	$⊢ (G \in Smgrp \land (M \in ℕ \land N \in ℕ \land X \in B)) \to M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$
11	5 6 7 9 10	syl13anc	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land (M \in ℕ \land N \in ℕ)) \to M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$
12	11	expr	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M \in ℕ) \to (N \in ℕ \to M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X))$
13		eqid	$⊢ 0_{G} = 0_{G}$
14	1 13 2	mulg0	$⊢ X \in B \to 0 \underset{˙}{\cdot} X = 0_{G}$
15	8 14	syl	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to 0 \underset{˙}{\cdot} X = 0_{G}$
16		simpr1	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to M \in ℕ_{0}$
17	16	nn0cnd	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to M \in ℂ$
18	17	mul01d	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to M \cdot 0 = 0$
19	18	oveq1d	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to M \cdot 0 \underset{˙}{\cdot} X = 0 \underset{˙}{\cdot} X$
20	15	oveq2d	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to M \underset{˙}{\cdot} (0 \underset{˙}{\cdot} X) = M \underset{˙}{\cdot} 0_{G}$
21	1 2 13	mulgnn0z	$⊢ (G \in Mnd \land M \in ℕ_{0}) \to M \underset{˙}{\cdot} 0_{G} = 0_{G}$
22	21	3ad2antr1	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to M \underset{˙}{\cdot} 0_{G} = 0_{G}$
23	20 22	eqtrd	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to M \underset{˙}{\cdot} (0 \underset{˙}{\cdot} X) = 0_{G}$
24	15 19 23	3eqtr4d	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to M \cdot 0 \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (0 \underset{˙}{\cdot} X)$
25	24	adantr	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M \in ℕ) \to M \cdot 0 \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (0 \underset{˙}{\cdot} X)$
26		oveq2	$⊢ N = 0 \to M \cdot N = M \cdot 0$
27	26	oveq1d	$⊢ N = 0 \to M \cdot N \underset{˙}{\cdot} X = M \cdot 0 \underset{˙}{\cdot} X$
28		oveq1	$⊢ N = 0 \to N \underset{˙}{\cdot} X = 0 \underset{˙}{\cdot} X$
29	28	oveq2d	$⊢ N = 0 \to M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X) = M \underset{˙}{\cdot} (0 \underset{˙}{\cdot} X)$
30	27 29	eqeq12d	$⊢ N = 0 \to (M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X) \leftrightarrow M \cdot 0 \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (0 \underset{˙}{\cdot} X))$
31	25 30	syl5ibrcom	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M \in ℕ) \to (N = 0 \to M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X))$
32		simpr2	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to N \in ℕ_{0}$
33		elnn0	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℕ \lor N = 0)$
34	32 33	sylib	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to (N \in ℕ \lor N = 0)$
35	34	adantr	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M \in ℕ) \to (N \in ℕ \lor N = 0)$
36	12 31 35	mpjaod	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M \in ℕ) \to M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$
37	36	ex	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to (M \in ℕ \to M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X))$
38	32	nn0cnd	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to N \in ℂ$
39	38	mul02d	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to 0 \cdot N = 0$
40	39	oveq1d	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to 0 \cdot N \underset{˙}{\cdot} X = 0 \underset{˙}{\cdot} X$
41	1 2	mulgnn0cl	$⊢ (G \in Mnd \land N \in ℕ_{0} \land X \in B) \to N \underset{˙}{\cdot} X \in B$
42	41	3adant3r1	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to N \underset{˙}{\cdot} X \in B$
43	1 13 2	mulg0	$⊢ N \underset{˙}{\cdot} X \in B \to 0 \underset{˙}{\cdot} (N \underset{˙}{\cdot} X) = 0_{G}$
44	42 43	syl	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to 0 \underset{˙}{\cdot} (N \underset{˙}{\cdot} X) = 0_{G}$
45	15 40 44	3eqtr4d	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to 0 \cdot N \underset{˙}{\cdot} X = 0 \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$
46		oveq1	$⊢ M = 0 \to M \cdot N = 0 \cdot N$
47	46	oveq1d	$⊢ M = 0 \to M \cdot N \underset{˙}{\cdot} X = 0 \cdot N \underset{˙}{\cdot} X$
48		oveq1	$⊢ M = 0 \to M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X) = 0 \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$
49	47 48	eqeq12d	$⊢ M = 0 \to (M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X) \leftrightarrow 0 \cdot N \underset{˙}{\cdot} X = 0 \underset{˙}{\cdot} (N \underset{˙}{\cdot} X))$
50	45 49	syl5ibrcom	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to (M = 0 \to M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X))$
51		elnn0	$⊢ M \in ℕ_{0} \leftrightarrow (M \in ℕ \lor M = 0)$
52	16 51	sylib	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to (M \in ℕ \lor M = 0)$
53	37 50 52	mpjaod	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to M \cdot N \underset{˙}{\cdot} X = M \underset{˙}{\cdot} (N \underset{˙}{\cdot} X)$

Metamath Proof Explorer

Theorem mulgnn0ass

Proof