submmulg

Description: A group multiple is the same if evaluated in a submonoid. (Contributed by Mario Carneiro, 15-Jun-2015)

	Ref	Expression
Hypotheses	submmulgcl.t	$⊢ \underset{˙}{∙} = \cdot_{G}$
	submmulg.h	$⊢ H = G ↾_{𝑠} S$
	submmulg.t	$⊢ \underset{˙}{\cdot} = \cdot_{H}$
Assertion	submmulg	$⊢ (S \in SubMnd (G) \land N \in ℕ_{0} \land X \in S) \to N \underset{˙}{∙} X = N \underset{˙}{\cdot} X$

Proof

Step	Hyp	Ref	Expression
1		submmulgcl.t	$⊢ \underset{˙}{∙} = \cdot_{G}$
2		submmulg.h	$⊢ H = G ↾_{𝑠} S$
3		submmulg.t	$⊢ \underset{˙}{\cdot} = \cdot_{H}$
4		simpl1	$⊢ ((S \in SubMnd (G) \land N \in ℕ_{0} \land X \in S) \land N \in ℕ) \to S \in SubMnd (G)$
5		eqid	$⊢ +_{G} = +_{G}$
6	2 5	ressplusg	$⊢ S \in SubMnd (G) \to +_{G} = +_{H}$
7	4 6	syl	$⊢ ((S \in SubMnd (G) \land N \in ℕ_{0} \land X \in S) \land N \in ℕ) \to +_{G} = +_{H}$
8	7	seqeq2d	$⊢ ((S \in SubMnd (G) \land N \in ℕ_{0} \land X \in S) \land N \in ℕ) \to seq 1 (+_{G}, (ℕ \times \{X\})) = seq 1 (+_{H}, (ℕ \times \{X\}))$
9	8	fveq1d	$⊢ ((S \in SubMnd (G) \land N \in ℕ_{0} \land X \in S) \land N \in ℕ) \to seq 1 (+_{G}, (ℕ \times \{X\})) (N) = seq 1 (+_{H}, (ℕ \times \{X\})) (N)$
10		simpr	$⊢ ((S \in SubMnd (G) \land N \in ℕ_{0} \land X \in S) \land N \in ℕ) \to N \in ℕ$
11		eqid	$⊢ {Base}_{G} = {Base}_{G}$
12	11	submss	$⊢ S \in SubMnd (G) \to S \subseteq {Base}_{G}$
13	12	3ad2ant1	$⊢ (S \in SubMnd (G) \land N \in ℕ_{0} \land X \in S) \to S \subseteq {Base}_{G}$
14		simp3	$⊢ (S \in SubMnd (G) \land N \in ℕ_{0} \land X \in S) \to X \in S$
15	13 14	sseldd	$⊢ (S \in SubMnd (G) \land N \in ℕ_{0} \land X \in S) \to X \in {Base}_{G}$
16	15	adantr	$⊢ ((S \in SubMnd (G) \land N \in ℕ_{0} \land X \in S) \land N \in ℕ) \to X \in {Base}_{G}$
17		eqid	$⊢ seq 1 (+_{G}, (ℕ \times \{X\})) = seq 1 (+_{G}, (ℕ \times \{X\}))$
18	11 5 1 17	mulgnn	$⊢ (N \in ℕ \land X \in {Base}_{G}) \to N \underset{˙}{∙} X = seq 1 (+_{G}, (ℕ \times \{X\})) (N)$
19	10 16 18	syl2anc	$⊢ ((S \in SubMnd (G) \land N \in ℕ_{0} \land X \in S) \land N \in ℕ) \to N \underset{˙}{∙} X = seq 1 (+_{G}, (ℕ \times \{X\})) (N)$
20	2	submbas	$⊢ S \in SubMnd (G) \to S = {Base}_{H}$
21	20	3ad2ant1	$⊢ (S \in SubMnd (G) \land N \in ℕ_{0} \land X \in S) \to S = {Base}_{H}$
22	14 21	eleqtrd	$⊢ (S \in SubMnd (G) \land N \in ℕ_{0} \land X \in S) \to X \in {Base}_{H}$
23	22	adantr	$⊢ ((S \in SubMnd (G) \land N \in ℕ_{0} \land X \in S) \land N \in ℕ) \to X \in {Base}_{H}$
24		eqid	$⊢ {Base}_{H} = {Base}_{H}$
25		eqid	$⊢ +_{H} = +_{H}$
26		eqid	$⊢ seq 1 (+_{H}, (ℕ \times \{X\})) = seq 1 (+_{H}, (ℕ \times \{X\}))$
27	24 25 3 26	mulgnn	$⊢ (N \in ℕ \land X \in {Base}_{H}) \to N \underset{˙}{\cdot} X = seq 1 (+_{H}, (ℕ \times \{X\})) (N)$
28	10 23 27	syl2anc	$⊢ ((S \in SubMnd (G) \land N \in ℕ_{0} \land X \in S) \land N \in ℕ) \to N \underset{˙}{\cdot} X = seq 1 (+_{H}, (ℕ \times \{X\})) (N)$
29	9 19 28	3eqtr4d	$⊢ ((S \in SubMnd (G) \land N \in ℕ_{0} \land X \in S) \land N \in ℕ) \to N \underset{˙}{∙} X = N \underset{˙}{\cdot} X$
30		simpl1	$⊢ ((S \in SubMnd (G) \land N \in ℕ_{0} \land X \in S) \land N = 0) \to S \in SubMnd (G)$
31		eqid	$⊢ 0_{G} = 0_{G}$
32	2 31	subm0	$⊢ S \in SubMnd (G) \to 0_{G} = 0_{H}$
33	30 32	syl	$⊢ ((S \in SubMnd (G) \land N \in ℕ_{0} \land X \in S) \land N = 0) \to 0_{G} = 0_{H}$
34	15	adantr	$⊢ ((S \in SubMnd (G) \land N \in ℕ_{0} \land X \in S) \land N = 0) \to X \in {Base}_{G}$
35	11 31 1	mulg0	$⊢ X \in {Base}_{G} \to 0 \underset{˙}{∙} X = 0_{G}$
36	34 35	syl	$⊢ ((S \in SubMnd (G) \land N \in ℕ_{0} \land X \in S) \land N = 0) \to 0 \underset{˙}{∙} X = 0_{G}$
37	22	adantr	$⊢ ((S \in SubMnd (G) \land N \in ℕ_{0} \land X \in S) \land N = 0) \to X \in {Base}_{H}$
38		eqid	$⊢ 0_{H} = 0_{H}$
39	24 38 3	mulg0	$⊢ X \in {Base}_{H} \to 0 \underset{˙}{\cdot} X = 0_{H}$
40	37 39	syl	$⊢ ((S \in SubMnd (G) \land N \in ℕ_{0} \land X \in S) \land N = 0) \to 0 \underset{˙}{\cdot} X = 0_{H}$
41	33 36 40	3eqtr4d	$⊢ ((S \in SubMnd (G) \land N \in ℕ_{0} \land X \in S) \land N = 0) \to 0 \underset{˙}{∙} X = 0 \underset{˙}{\cdot} X$
42		simpr	$⊢ ((S \in SubMnd (G) \land N \in ℕ_{0} \land X \in S) \land N = 0) \to N = 0$
43	42	oveq1d	$⊢ ((S \in SubMnd (G) \land N \in ℕ_{0} \land X \in S) \land N = 0) \to N \underset{˙}{∙} X = 0 \underset{˙}{∙} X$
44	42	oveq1d	$⊢ ((S \in SubMnd (G) \land N \in ℕ_{0} \land X \in S) \land N = 0) \to N \underset{˙}{\cdot} X = 0 \underset{˙}{\cdot} X$
45	41 43 44	3eqtr4d	$⊢ ((S \in SubMnd (G) \land N \in ℕ_{0} \land X \in S) \land N = 0) \to N \underset{˙}{∙} X = N \underset{˙}{\cdot} X$
46		simp2	$⊢ (S \in SubMnd (G) \land N \in ℕ_{0} \land X \in S) \to N \in ℕ_{0}$
47		elnn0	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℕ \lor N = 0)$
48	46 47	sylib	$⊢ (S \in SubMnd (G) \land N \in ℕ_{0} \land X \in S) \to (N \in ℕ \lor N = 0)$
49	29 45 48	mpjaodan	$⊢ (S \in SubMnd (G) \land N \in ℕ_{0} \land X \in S) \to N \underset{˙}{∙} X = N \underset{˙}{\cdot} X$

Metamath Proof Explorer

Theorem submmulg

Proof