mulgnn0dir

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

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

Proof

Step	Hyp	Ref	Expression
1		mulgnndir.b	$⊢ B = {Base}_{G}$
2		mulgnndir.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		mulgnndir.p	$⊢ \underset{˙}{+} = +_{G}$
4		mndsgrp	Could not format ( G e. Mnd -> G e. Smgrp ) : No typesetting found for \|- ( G e. Mnd -> G e. Smgrp ) with typecode \|-
5	4	adantr	Could not format ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> G e. Smgrp ) : No typesetting found for \|- ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) -> G e. Smgrp ) with typecode \|-
6	5	ad2antrr	Could not format ( ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M e. NN ) /\ N e. NN ) -> G e. Smgrp ) : No typesetting found for \|- ( ( ( ( G e. Mnd /\ ( M e. NN0 /\ N e. NN0 /\ X e. B ) ) /\ M e. NN ) /\ N e. NN ) -> G e. Smgrp ) with typecode \|-
7		simplr	$⊢ (((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M \in ℕ) \land N \in ℕ) \to M \in ℕ$
8		simpr	$⊢ (((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M \in ℕ) \land N \in ℕ) \to N \in ℕ$
9		simpr3	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to X \in B$
10	9	ad2antrr	$⊢ (((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$
11	1 2 3	mulgnndir	Could not format ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) ) : No typesetting found for \|- ( ( G e. Smgrp /\ ( M e. NN /\ N e. NN /\ X e. B ) ) -> ( ( M + N ) .x. X ) = ( ( M .x. X ) .+ ( N .x. X ) ) ) with typecode \|-
12	6 7 8 10 11	syl13anc	$⊢ (((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M \in ℕ) \land N \in ℕ) \to (M + N) \underset{˙}{\cdot} X = (M \underset{˙}{\cdot} X) \underset{˙}{+} (N \underset{˙}{\cdot} X)$
13		simpll	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land N = 0) \to G \in Mnd$
14		simpr1	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to M \in ℕ_{0}$
15	14	adantr	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land N = 0) \to M \in ℕ_{0}$
16		simplr3	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land N = 0) \to X \in B$
17	1 2 13 15 16	mulgnn0cld	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land N = 0) \to M \underset{˙}{\cdot} X \in B$
18		eqid	$⊢ 0_{G} = 0_{G}$
19	1 3 18	mndrid	$⊢ (G \in Mnd \land M \underset{˙}{\cdot} X \in B) \to (M \underset{˙}{\cdot} X) \underset{˙}{+} 0_{G} = M \underset{˙}{\cdot} X$
20	13 17 19	syl2anc	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land N = 0) \to (M \underset{˙}{\cdot} X) \underset{˙}{+} 0_{G} = M \underset{˙}{\cdot} X$
21		simpr	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land N = 0) \to N = 0$
22	21	oveq1d	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land N = 0) \to N \underset{˙}{\cdot} X = 0 \underset{˙}{\cdot} X$
23	1 18 2	mulg0	$⊢ X \in B \to 0 \underset{˙}{\cdot} X = 0_{G}$
24	16 23	syl	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land N = 0) \to 0 \underset{˙}{\cdot} X = 0_{G}$
25	22 24	eqtrd	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land N = 0) \to N \underset{˙}{\cdot} X = 0_{G}$
26	25	oveq2d	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land N = 0) \to (M \underset{˙}{\cdot} X) \underset{˙}{+} (N \underset{˙}{\cdot} X) = (M \underset{˙}{\cdot} X) \underset{˙}{+} 0_{G}$
27	21	oveq2d	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land N = 0) \to M + N = M + 0$
28	15	nn0cnd	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land N = 0) \to M \in ℂ$
29	28	addridd	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land N = 0) \to M + 0 = M$
30	27 29	eqtrd	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land N = 0) \to M + N = M$
31	30	oveq1d	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land N = 0) \to (M + N) \underset{˙}{\cdot} X = M \underset{˙}{\cdot} X$
32	20 26 31	3eqtr4rd	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land N = 0) \to (M + N) \underset{˙}{\cdot} X = (M \underset{˙}{\cdot} X) \underset{˙}{+} (N \underset{˙}{\cdot} X)$
33	32	adantlr	$⊢ (((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M \in ℕ) \land N = 0) \to (M + N) \underset{˙}{\cdot} X = (M \underset{˙}{\cdot} X) \underset{˙}{+} (N \underset{˙}{\cdot} X)$
34		simpr2	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to N \in ℕ_{0}$
35		elnn0	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℕ \lor N = 0)$
36	34 35	sylib	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to (N \in ℕ \lor N = 0)$
37	36	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)$
38	12 33 37	mpjaodan	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M \in ℕ) \to (M + N) \underset{˙}{\cdot} X = (M \underset{˙}{\cdot} X) \underset{˙}{+} (N \underset{˙}{\cdot} X)$
39		simpll	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M = 0) \to G \in Mnd$
40		simplr2	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M = 0) \to N \in ℕ_{0}$
41		simplr3	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M = 0) \to X \in B$
42	1 2 39 40 41	mulgnn0cld	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M = 0) \to N \underset{˙}{\cdot} X \in B$
43	1 3 18	mndlid	$⊢ (G \in Mnd \land N \underset{˙}{\cdot} X \in B) \to 0_{G} \underset{˙}{+} (N \underset{˙}{\cdot} X) = N \underset{˙}{\cdot} X$
44	39 42 43	syl2anc	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M = 0) \to 0_{G} \underset{˙}{+} (N \underset{˙}{\cdot} X) = N \underset{˙}{\cdot} X$
45		simpr	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M = 0) \to M = 0$
46	45	oveq1d	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M = 0) \to M \underset{˙}{\cdot} X = 0 \underset{˙}{\cdot} X$
47	41 23	syl	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M = 0) \to 0 \underset{˙}{\cdot} X = 0_{G}$
48	46 47	eqtrd	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M = 0) \to M \underset{˙}{\cdot} X = 0_{G}$
49	48	oveq1d	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M = 0) \to (M \underset{˙}{\cdot} X) \underset{˙}{+} (N \underset{˙}{\cdot} X) = 0_{G} \underset{˙}{+} (N \underset{˙}{\cdot} X)$
50	45	oveq1d	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M = 0) \to M + N = 0 + N$
51	40	nn0cnd	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M = 0) \to N \in ℂ$
52	51	addlidd	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M = 0) \to 0 + N = N$
53	50 52	eqtrd	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M = 0) \to M + N = N$
54	53	oveq1d	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M = 0) \to (M + N) \underset{˙}{\cdot} X = N \underset{˙}{\cdot} X$
55	44 49 54	3eqtr4rd	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M = 0) \to (M + N) \underset{˙}{\cdot} X = (M \underset{˙}{\cdot} X) \underset{˙}{+} (N \underset{˙}{\cdot} X)$
56		elnn0	$⊢ M \in ℕ_{0} \leftrightarrow (M \in ℕ \lor M = 0)$
57	14 56	sylib	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to (M \in ℕ \lor M = 0)$
58	38 55 57	mpjaodan	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to (M + N) \underset{˙}{\cdot} X = (M \underset{˙}{\cdot} X) \underset{˙}{+} (N \underset{˙}{\cdot} X)$

Metamath Proof Explorer

Theorem mulgnn0dir

Proof