subgmulg

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

	Ref	Expression
Hypotheses	subgmulgcl.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	subgmulg.h	$⊢ H = G ↾_{𝑠} S$
	subgmulg.t	$⊢ \underset{˙}{∙} = \cdot_{H}$
Assertion	subgmulg	$⊢ (S \in SubGrp (G) \land N \in ℤ \land X \in S) \to N \underset{˙}{\cdot} X = N \underset{˙}{∙} X$

Proof

Step	Hyp	Ref	Expression
1		subgmulgcl.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
2		subgmulg.h	$⊢ H = G ↾_{𝑠} S$
3		subgmulg.t	$⊢ \underset{˙}{∙} = \cdot_{H}$
4		eqid	$⊢ 0_{G} = 0_{G}$
5	2 4	subg0	$⊢ S \in SubGrp (G) \to 0_{G} = 0_{H}$
6	5	3ad2ant1	$⊢ (S \in SubGrp (G) \land N \in ℤ \land X \in S) \to 0_{G} = 0_{H}$
7	6	ifeq1d	$⊢ (S \in SubGrp (G) \land N \in ℤ \land X \in S) \to if (N = 0, 0_{G}, if (0 < N, seq 1 (+_{G}, (ℕ \times \{X\})) (N), {inv}_{g} (G) (seq 1 (+_{G}, (ℕ \times \{X\})) (- N)))) = if (N = 0, 0_{H}, if (0 < N, seq 1 (+_{G}, (ℕ \times \{X\})) (N), {inv}_{g} (G) (seq 1 (+_{G}, (ℕ \times \{X\})) (- N))))$
8		eqid	$⊢ +_{G} = +_{G}$
9	2 8	ressplusg	$⊢ S \in SubGrp (G) \to +_{G} = +_{H}$
10	9	3ad2ant1	$⊢ (S \in SubGrp (G) \land N \in ℤ \land X \in S) \to +_{G} = +_{H}$
11	10	seqeq2d	$⊢ (S \in SubGrp (G) \land N \in ℤ \land X \in S) \to seq 1 (+_{G}, (ℕ \times \{X\})) = seq 1 (+_{H}, (ℕ \times \{X\}))$
12	11	adantr	$⊢ ((S \in SubGrp (G) \land N \in ℤ \land X \in S) \land \neg N = 0) \to seq 1 (+_{G}, (ℕ \times \{X\})) = seq 1 (+_{H}, (ℕ \times \{X\}))$
13	12	fveq1d	$⊢ ((S \in SubGrp (G) \land N \in ℤ \land X \in S) \land \neg N = 0) \to seq 1 (+_{G}, (ℕ \times \{X\})) (N) = seq 1 (+_{H}, (ℕ \times \{X\})) (N)$
14	13	ifeq1d	$⊢ ((S \in SubGrp (G) \land N \in ℤ \land X \in S) \land \neg N = 0) \to if (0 < N, seq 1 (+_{G}, (ℕ \times \{X\})) (N), {inv}_{g} (G) (seq 1 (+_{G}, (ℕ \times \{X\})) (- N))) = if (0 < N, seq 1 (+_{H}, (ℕ \times \{X\})) (N), {inv}_{g} (G) (seq 1 (+_{G}, (ℕ \times \{X\})) (- N)))$
15		simp2	$⊢ (S \in SubGrp (G) \land N \in ℤ \land X \in S) \to N \in ℤ$
16	15	zred	$⊢ (S \in SubGrp (G) \land N \in ℤ \land X \in S) \to N \in ℝ$
17		0re	$⊢ 0 \in ℝ$
18		axlttri	$⊢ (N \in ℝ \land 0 \in ℝ) \to (N < 0 \leftrightarrow \neg (N = 0 \lor 0 < N))$
19	16 17 18	sylancl	$⊢ (S \in SubGrp (G) \land N \in ℤ \land X \in S) \to (N < 0 \leftrightarrow \neg (N = 0 \lor 0 < N))$
20		ioran	$⊢ \neg (N = 0 \lor 0 < N) \leftrightarrow (\neg N = 0 \land \neg 0 < N)$
21	19 20	bitrdi	$⊢ (S \in SubGrp (G) \land N \in ℤ \land X \in S) \to (N < 0 \leftrightarrow (\neg N = 0 \land \neg 0 < N))$
22	21	biimpar	$⊢ ((S \in SubGrp (G) \land N \in ℤ \land X \in S) \land (\neg N = 0 \land \neg 0 < N)) \to N < 0$
23		simpl1	$⊢ ((S \in SubGrp (G) \land N \in ℤ \land X \in S) \land N < 0) \to S \in SubGrp (G)$
24	15	adantr	$⊢ ((S \in SubGrp (G) \land N \in ℤ \land X \in S) \land N < 0) \to N \in ℤ$
25	24	znegcld	$⊢ ((S \in SubGrp (G) \land N \in ℤ \land X \in S) \land N < 0) \to - N \in ℤ$
26	16	lt0neg1d	$⊢ (S \in SubGrp (G) \land N \in ℤ \land X \in S) \to (N < 0 \leftrightarrow 0 < - N)$
27	26	biimpa	$⊢ ((S \in SubGrp (G) \land N \in ℤ \land X \in S) \land N < 0) \to 0 < - N$
28		elnnz	$⊢ - N \in ℕ \leftrightarrow (- N \in ℤ \land 0 < - N)$
29	25 27 28	sylanbrc	$⊢ ((S \in SubGrp (G) \land N \in ℤ \land X \in S) \land N < 0) \to - N \in ℕ$
30		eqid	$⊢ {Base}_{G} = {Base}_{G}$
31	30	subgss	$⊢ S \in SubGrp (G) \to S \subseteq {Base}_{G}$
32	31	3ad2ant1	$⊢ (S \in SubGrp (G) \land N \in ℤ \land X \in S) \to S \subseteq {Base}_{G}$
33		simp3	$⊢ (S \in SubGrp (G) \land N \in ℤ \land X \in S) \to X \in S$
34	32 33	sseldd	$⊢ (S \in SubGrp (G) \land N \in ℤ \land X \in S) \to X \in {Base}_{G}$
35	34	adantr	$⊢ ((S \in SubGrp (G) \land N \in ℤ \land X \in S) \land N < 0) \to X \in {Base}_{G}$
36		eqid	$⊢ seq 1 (+_{G}, (ℕ \times \{X\})) = seq 1 (+_{G}, (ℕ \times \{X\}))$
37	30 8 1 36	mulgnn	$⊢ (- N \in ℕ \land X \in {Base}_{G}) \to -N \underset{˙}{\cdot} X = seq 1 (+_{G}, (ℕ \times \{X\})) (- N)$
38	29 35 37	syl2anc	$⊢ ((S \in SubGrp (G) \land N \in ℤ \land X \in S) \land N < 0) \to -N \underset{˙}{\cdot} X = seq 1 (+_{G}, (ℕ \times \{X\})) (- N)$
39	33	adantr	$⊢ ((S \in SubGrp (G) \land N \in ℤ \land X \in S) \land N < 0) \to X \in S$
40	1	subgmulgcl	$⊢ (S \in SubGrp (G) \land - N \in ℤ \land X \in S) \to -N \underset{˙}{\cdot} X \in S$
41	23 25 39 40	syl3anc	$⊢ ((S \in SubGrp (G) \land N \in ℤ \land X \in S) \land N < 0) \to -N \underset{˙}{\cdot} X \in S$
42	38 41	eqeltrrd	$⊢ ((S \in SubGrp (G) \land N \in ℤ \land X \in S) \land N < 0) \to seq 1 (+_{G}, (ℕ \times \{X\})) (- N) \in S$
43		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
44		eqid	$⊢ {inv}_{g} (H) = {inv}_{g} (H)$
45	2 43 44	subginv	$⊢ (S \in SubGrp (G) \land seq 1 (+_{G}, (ℕ \times \{X\})) (- N) \in S) \to {inv}_{g} (G) (seq 1 (+_{G}, (ℕ \times \{X\})) (- N)) = {inv}_{g} (H) (seq 1 (+_{G}, (ℕ \times \{X\})) (- N))$
46	23 42 45	syl2anc	$⊢ ((S \in SubGrp (G) \land N \in ℤ \land X \in S) \land N < 0) \to {inv}_{g} (G) (seq 1 (+_{G}, (ℕ \times \{X\})) (- N)) = {inv}_{g} (H) (seq 1 (+_{G}, (ℕ \times \{X\})) (- N))$
47	22 46	syldan	$⊢ ((S \in SubGrp (G) \land N \in ℤ \land X \in S) \land (\neg N = 0 \land \neg 0 < N)) \to {inv}_{g} (G) (seq 1 (+_{G}, (ℕ \times \{X\})) (- N)) = {inv}_{g} (H) (seq 1 (+_{G}, (ℕ \times \{X\})) (- N))$
48	11	adantr	$⊢ ((S \in SubGrp (G) \land N \in ℤ \land X \in S) \land (\neg N = 0 \land \neg 0 < N)) \to seq 1 (+_{G}, (ℕ \times \{X\})) = seq 1 (+_{H}, (ℕ \times \{X\}))$
49	48	fveq1d	$⊢ ((S \in SubGrp (G) \land N \in ℤ \land X \in S) \land (\neg N = 0 \land \neg 0 < N)) \to seq 1 (+_{G}, (ℕ \times \{X\})) (- N) = seq 1 (+_{H}, (ℕ \times \{X\})) (- N)$
50	49	fveq2d	$⊢ ((S \in SubGrp (G) \land N \in ℤ \land X \in S) \land (\neg N = 0 \land \neg 0 < N)) \to {inv}_{g} (H) (seq 1 (+_{G}, (ℕ \times \{X\})) (- N)) = {inv}_{g} (H) (seq 1 (+_{H}, (ℕ \times \{X\})) (- N))$
51	47 50	eqtrd	$⊢ ((S \in SubGrp (G) \land N \in ℤ \land X \in S) \land (\neg N = 0 \land \neg 0 < N)) \to {inv}_{g} (G) (seq 1 (+_{G}, (ℕ \times \{X\})) (- N)) = {inv}_{g} (H) (seq 1 (+_{H}, (ℕ \times \{X\})) (- N))$
52	51	anassrs	$⊢ (((S \in SubGrp (G) \land N \in ℤ \land X \in S) \land \neg N = 0) \land \neg 0 < N) \to {inv}_{g} (G) (seq 1 (+_{G}, (ℕ \times \{X\})) (- N)) = {inv}_{g} (H) (seq 1 (+_{H}, (ℕ \times \{X\})) (- N))$
53	52	ifeq2da	$⊢ ((S \in SubGrp (G) \land N \in ℤ \land X \in S) \land \neg N = 0) \to if (0 < N, seq 1 (+_{H}, (ℕ \times \{X\})) (N), {inv}_{g} (G) (seq 1 (+_{G}, (ℕ \times \{X\})) (- N))) = if (0 < N, seq 1 (+_{H}, (ℕ \times \{X\})) (N), {inv}_{g} (H) (seq 1 (+_{H}, (ℕ \times \{X\})) (- N)))$
54	14 53	eqtrd	$⊢ ((S \in SubGrp (G) \land N \in ℤ \land X \in S) \land \neg N = 0) \to if (0 < N, seq 1 (+_{G}, (ℕ \times \{X\})) (N), {inv}_{g} (G) (seq 1 (+_{G}, (ℕ \times \{X\})) (- N))) = if (0 < N, seq 1 (+_{H}, (ℕ \times \{X\})) (N), {inv}_{g} (H) (seq 1 (+_{H}, (ℕ \times \{X\})) (- N)))$
55	54	ifeq2da	$⊢ (S \in SubGrp (G) \land N \in ℤ \land X \in S) \to if (N = 0, 0_{H}, if (0 < N, seq 1 (+_{G}, (ℕ \times \{X\})) (N), {inv}_{g} (G) (seq 1 (+_{G}, (ℕ \times \{X\})) (- N)))) = if (N = 0, 0_{H}, if (0 < N, seq 1 (+_{H}, (ℕ \times \{X\})) (N), {inv}_{g} (H) (seq 1 (+_{H}, (ℕ \times \{X\})) (- N))))$
56	7 55	eqtrd	$⊢ (S \in SubGrp (G) \land N \in ℤ \land X \in S) \to if (N = 0, 0_{G}, if (0 < N, seq 1 (+_{G}, (ℕ \times \{X\})) (N), {inv}_{g} (G) (seq 1 (+_{G}, (ℕ \times \{X\})) (- N)))) = if (N = 0, 0_{H}, if (0 < N, seq 1 (+_{H}, (ℕ \times \{X\})) (N), {inv}_{g} (H) (seq 1 (+_{H}, (ℕ \times \{X\})) (- N))))$
57	30 8 4 43 1 36	mulgval	$⊢ (N \in ℤ \land X \in {Base}_{G}) \to N \underset{˙}{\cdot} X = if (N = 0, 0_{G}, if (0 < N, seq 1 (+_{G}, (ℕ \times \{X\})) (N), {inv}_{g} (G) (seq 1 (+_{G}, (ℕ \times \{X\})) (- N))))$
58	15 34 57	syl2anc	$⊢ (S \in SubGrp (G) \land N \in ℤ \land X \in S) \to N \underset{˙}{\cdot} X = if (N = 0, 0_{G}, if (0 < N, seq 1 (+_{G}, (ℕ \times \{X\})) (N), {inv}_{g} (G) (seq 1 (+_{G}, (ℕ \times \{X\})) (- N))))$
59	2	subgbas	$⊢ S \in SubGrp (G) \to S = {Base}_{H}$
60	59	3ad2ant1	$⊢ (S \in SubGrp (G) \land N \in ℤ \land X \in S) \to S = {Base}_{H}$
61	33 60	eleqtrd	$⊢ (S \in SubGrp (G) \land N \in ℤ \land X \in S) \to X \in {Base}_{H}$
62		eqid	$⊢ {Base}_{H} = {Base}_{H}$
63		eqid	$⊢ +_{H} = +_{H}$
64		eqid	$⊢ 0_{H} = 0_{H}$
65		eqid	$⊢ seq 1 (+_{H}, (ℕ \times \{X\})) = seq 1 (+_{H}, (ℕ \times \{X\}))$
66	62 63 64 44 3 65	mulgval	$⊢ (N \in ℤ \land X \in {Base}_{H}) \to N \underset{˙}{∙} X = if (N = 0, 0_{H}, if (0 < N, seq 1 (+_{H}, (ℕ \times \{X\})) (N), {inv}_{g} (H) (seq 1 (+_{H}, (ℕ \times \{X\})) (- N))))$
67	15 61 66	syl2anc	$⊢ (S \in SubGrp (G) \land N \in ℤ \land X \in S) \to N \underset{˙}{∙} X = if (N = 0, 0_{H}, if (0 < N, seq 1 (+_{H}, (ℕ \times \{X\})) (N), {inv}_{g} (H) (seq 1 (+_{H}, (ℕ \times \{X\})) (- N))))$
68	56 58 67	3eqtr4d	$⊢ (S \in SubGrp (G) \land N \in ℤ \land X \in S) \to N \underset{˙}{\cdot} X = N \underset{˙}{∙} X$

Metamath Proof Explorer

Theorem subgmulg

Proof