subglsm

Description: The subgroup sum evaluated within a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016)

	Ref	Expression
Hypotheses	subglsm.h	$⊢ H = G ↾_{𝑠} S$
	subglsm.s	$⊢ \underset{˙}{\oplus} = LSSum (G)$
	subglsm.a	$⊢ A = LSSum (H)$
Assertion	subglsm	$⊢ (S \in SubGrp (G) \land T \subseteq S \land U \subseteq S) \to T \underset{˙}{\oplus} U = T A U$

Proof

Step	Hyp	Ref	Expression
1		subglsm.h	$⊢ H = G ↾_{𝑠} S$
2		subglsm.s	$⊢ \underset{˙}{\oplus} = LSSum (G)$
3		subglsm.a	$⊢ A = LSSum (H)$
4		simp11	$⊢ ((S \in SubGrp (G) \land T \subseteq S \land U \subseteq S) \land x \in T \land y \in U) \to S \in SubGrp (G)$
5		eqid	$⊢ +_{G} = +_{G}$
6	1 5	ressplusg	$⊢ S \in SubGrp (G) \to +_{G} = +_{H}$
7	4 6	syl	$⊢ ((S \in SubGrp (G) \land T \subseteq S \land U \subseteq S) \land x \in T \land y \in U) \to +_{G} = +_{H}$
8	7	oveqd	$⊢ ((S \in SubGrp (G) \land T \subseteq S \land U \subseteq S) \land x \in T \land y \in U) \to x +_{G} y = x +_{H} y$
9	8	mpoeq3dva	$⊢ (S \in SubGrp (G) \land T \subseteq S \land U \subseteq S) \to (x \in T, y \in U ⟼ x +_{G} y) = (x \in T, y \in U ⟼ x +_{H} y)$
10	9	rneqd	$⊢ (S \in SubGrp (G) \land T \subseteq S \land U \subseteq S) \to ran (x \in T, y \in U ⟼ x +_{G} y) = ran (x \in T, y \in U ⟼ x +_{H} y)$
11		subgrcl	$⊢ S \in SubGrp (G) \to G \in Grp$
12	11	3ad2ant1	$⊢ (S \in SubGrp (G) \land T \subseteq S \land U \subseteq S) \to G \in Grp$
13		simp2	$⊢ (S \in SubGrp (G) \land T \subseteq S \land U \subseteq S) \to T \subseteq S$
14		eqid	$⊢ {Base}_{G} = {Base}_{G}$
15	14	subgss	$⊢ S \in SubGrp (G) \to S \subseteq {Base}_{G}$
16	15	3ad2ant1	$⊢ (S \in SubGrp (G) \land T \subseteq S \land U \subseteq S) \to S \subseteq {Base}_{G}$
17	13 16	sstrd	$⊢ (S \in SubGrp (G) \land T \subseteq S \land U \subseteq S) \to T \subseteq {Base}_{G}$
18		simp3	$⊢ (S \in SubGrp (G) \land T \subseteq S \land U \subseteq S) \to U \subseteq S$
19	18 16	sstrd	$⊢ (S \in SubGrp (G) \land T \subseteq S \land U \subseteq S) \to U \subseteq {Base}_{G}$
20	14 5 2	lsmvalx	$⊢ (G \in Grp \land T \subseteq {Base}_{G} \land U \subseteq {Base}_{G}) \to T \underset{˙}{\oplus} U = ran (x \in T, y \in U ⟼ x +_{G} y)$
21	12 17 19 20	syl3anc	$⊢ (S \in SubGrp (G) \land T \subseteq S \land U \subseteq S) \to T \underset{˙}{\oplus} U = ran (x \in T, y \in U ⟼ x +_{G} y)$
22	1	subggrp	$⊢ S \in SubGrp (G) \to H \in Grp$
23	22	3ad2ant1	$⊢ (S \in SubGrp (G) \land T \subseteq S \land U \subseteq S) \to H \in Grp$
24	1	subgbas	$⊢ S \in SubGrp (G) \to S = {Base}_{H}$
25	24	3ad2ant1	$⊢ (S \in SubGrp (G) \land T \subseteq S \land U \subseteq S) \to S = {Base}_{H}$
26	13 25	sseqtrd	$⊢ (S \in SubGrp (G) \land T \subseteq S \land U \subseteq S) \to T \subseteq {Base}_{H}$
27	18 25	sseqtrd	$⊢ (S \in SubGrp (G) \land T \subseteq S \land U \subseteq S) \to U \subseteq {Base}_{H}$
28		eqid	$⊢ {Base}_{H} = {Base}_{H}$
29		eqid	$⊢ +_{H} = +_{H}$
30	28 29 3	lsmvalx	$⊢ (H \in Grp \land T \subseteq {Base}_{H} \land U \subseteq {Base}_{H}) \to T A U = ran (x \in T, y \in U ⟼ x +_{H} y)$
31	23 26 27 30	syl3anc	$⊢ (S \in SubGrp (G) \land T \subseteq S \land U \subseteq S) \to T A U = ran (x \in T, y \in U ⟼ x +_{H} y)$
32	10 21 31	3eqtr4d	$⊢ (S \in SubGrp (G) \land T \subseteq S \land U \subseteq S) \to T \underset{˙}{\oplus} U = T A U$

Metamath Proof Explorer

Theorem subglsm

Proof