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	mulgnn0cl	$⊢ (G \in Mnd \land M \in ℕ_{0} \land X \in B) \to M \underset{˙}{\cdot} X \in B$
18	13 15 16 17	syl3anc	$⊢ ((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$
19		eqid	$⊢ 0_{G} = 0_{G}$
20	1 3 19	mndrid	$⊢ (G \in Mnd \land M \underset{˙}{\cdot} X \in B) \to (M \underset{˙}{\cdot} X) \underset{˙}{+} 0_{G} = M \underset{˙}{\cdot} X$
21	13 18 20	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$
22		simpr	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land N = 0) \to N = 0$
23	22	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$
24	1 19 2	mulg0	$⊢ X \in B \to 0 \underset{˙}{\cdot} X = 0_{G}$
25	16 24	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}$
26	23 25	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}$
27	26	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}$
28	22	oveq2d	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land N = 0) \to M + N = M + 0$
29	15	nn0cnd	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land N = 0) \to M \in ℂ$
30	29	addid1d	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land N = 0) \to M + 0 = M$
31	28 30	eqtrd	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land N = 0) \to M + N = M$
32	31	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$
33	21 27 32	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)$
34	33	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)$
35		simpr2	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to N \in ℕ_{0}$
36		elnn0	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℕ \lor N = 0)$
37	35 36	sylib	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to (N \in ℕ \lor N = 0)$
38	37	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)$
39	12 34 38	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)$
40		simpll	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M = 0) \to G \in Mnd$
41		simplr2	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M = 0) \to N \in ℕ_{0}$
42		simplr3	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M = 0) \to X \in B$
43	1 2	mulgnn0cl	$⊢ (G \in Mnd \land N \in ℕ_{0} \land X \in B) \to N \underset{˙}{\cdot} X \in B$
44	40 41 42 43	syl3anc	$⊢ ((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$
45	1 3 19	mndlid	$⊢ (G \in Mnd \land N \underset{˙}{\cdot} X \in B) \to 0_{G} \underset{˙}{+} (N \underset{˙}{\cdot} X) = N \underset{˙}{\cdot} X$
46	40 44 45	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$
47		simpr	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M = 0) \to M = 0$
48	47	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$
49	42 24	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}$
50	48 49	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}$
51	50	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)$
52	47	oveq1d	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M = 0) \to M + N = 0 + N$
53	41	nn0cnd	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M = 0) \to N \in ℂ$
54	53	addid2d	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M = 0) \to 0 + N = N$
55	52 54	eqtrd	$⊢ ((G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \land M = 0) \to M + N = N$
56	55	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$
57	46 51 56	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)$
58		elnn0	$⊢ M \in ℕ_{0} \leftrightarrow (M \in ℕ \lor M = 0)$
59	14 58	sylib	$⊢ (G \in Mnd \land (M \in ℕ_{0} \land N \in ℕ_{0} \land X \in B)) \to (M \in ℕ \lor M = 0)$
60	39 57 59	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