lsmelvalm

Description: Subgroup sum membership analogue of lsmelval using vector subtraction. TODO: any way to shorten proof? (Contributed by NM, 16-Mar-2015) (Revised by Mario Carneiro, 19-Apr-2016)

	Ref	Expression
Hypotheses	lsmelvalm.m	$⊢ \underset{˙}{-} = -_{G}$
	lsmelvalm.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
	lsmelvalm.t	$⊢ φ \to T \in SubGrp (G)$
	lsmelvalm.u	$⊢ φ \to U \in SubGrp (G)$
Assertion	lsmelvalm	$⊢ φ \to (X \in (T \underset{˙}{\oplus} U) \leftrightarrow \exists y \in T \exists z \in U X = y \underset{˙}{-} z)$

Proof

Step	Hyp	Ref	Expression
1		lsmelvalm.m	$⊢ \underset{˙}{-} = -_{G}$
2		lsmelvalm.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
3		lsmelvalm.t	$⊢ φ \to T \in SubGrp (G)$
4		lsmelvalm.u	$⊢ φ \to U \in SubGrp (G)$
5		eqid	$⊢ +_{G} = +_{G}$
6	5 2	lsmelval	$⊢ (T \in SubGrp (G) \land U \in SubGrp (G)) \to (X \in (T \underset{˙}{\oplus} U) \leftrightarrow \exists y \in T \exists x \in U X = y +_{G} x)$
7	3 4 6	syl2anc	$⊢ φ \to (X \in (T \underset{˙}{\oplus} U) \leftrightarrow \exists y \in T \exists x \in U X = y +_{G} x)$
8	4	adantr	$⊢ (φ \land y \in T) \to U \in SubGrp (G)$
9		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
10	9	subginvcl	$⊢ (U \in SubGrp (G) \land x \in U) \to {inv}_{g} (G) (x) \in U$
11	8 10	sylan	$⊢ ((φ \land y \in T) \land x \in U) \to {inv}_{g} (G) (x) \in U$
12		eqid	$⊢ {Base}_{G} = {Base}_{G}$
13		subgrcl	$⊢ T \in SubGrp (G) \to G \in Grp$
14	3 13	syl	$⊢ φ \to G \in Grp$
15	14	ad2antrr	$⊢ ((φ \land y \in T) \land x \in U) \to G \in Grp$
16	12	subgss	$⊢ T \in SubGrp (G) \to T \subseteq {Base}_{G}$
17	3 16	syl	$⊢ φ \to T \subseteq {Base}_{G}$
18	17	sselda	$⊢ (φ \land y \in T) \to y \in {Base}_{G}$
19	18	adantr	$⊢ ((φ \land y \in T) \land x \in U) \to y \in {Base}_{G}$
20	12	subgss	$⊢ U \in SubGrp (G) \to U \subseteq {Base}_{G}$
21	8 20	syl	$⊢ (φ \land y \in T) \to U \subseteq {Base}_{G}$
22	21	sselda	$⊢ ((φ \land y \in T) \land x \in U) \to x \in {Base}_{G}$
23	12 5 1 9 15 19 22	grpsubinv	$⊢ ((φ \land y \in T) \land x \in U) \to y \underset{˙}{-} {inv}_{g} (G) (x) = y +_{G} x$
24	23	eqcomd	$⊢ ((φ \land y \in T) \land x \in U) \to y +_{G} x = y \underset{˙}{-} {inv}_{g} (G) (x)$
25		oveq2	$⊢ z = {inv}_{g} (G) (x) \to y \underset{˙}{-} z = y \underset{˙}{-} {inv}_{g} (G) (x)$
26	25	rspceeqv	$⊢ ({inv}_{g} (G) (x) \in U \land y +_{G} x = y \underset{˙}{-} {inv}_{g} (G) (x)) \to \exists z \in U y +_{G} x = y \underset{˙}{-} z$
27	11 24 26	syl2anc	$⊢ ((φ \land y \in T) \land x \in U) \to \exists z \in U y +_{G} x = y \underset{˙}{-} z$
28		eqeq1	$⊢ X = y +_{G} x \to (X = y \underset{˙}{-} z \leftrightarrow y +_{G} x = y \underset{˙}{-} z)$
29	28	rexbidv	$⊢ X = y +_{G} x \to (\exists z \in U X = y \underset{˙}{-} z \leftrightarrow \exists z \in U y +_{G} x = y \underset{˙}{-} z)$
30	27 29	syl5ibrcom	$⊢ ((φ \land y \in T) \land x \in U) \to (X = y +_{G} x \to \exists z \in U X = y \underset{˙}{-} z)$
31	30	rexlimdva	$⊢ (φ \land y \in T) \to (\exists x \in U X = y +_{G} x \to \exists z \in U X = y \underset{˙}{-} z)$
32	9	subginvcl	$⊢ (U \in SubGrp (G) \land z \in U) \to {inv}_{g} (G) (z) \in U$
33	8 32	sylan	$⊢ ((φ \land y \in T) \land z \in U) \to {inv}_{g} (G) (z) \in U$
34	18	adantr	$⊢ ((φ \land y \in T) \land z \in U) \to y \in {Base}_{G}$
35	21	sselda	$⊢ ((φ \land y \in T) \land z \in U) \to z \in {Base}_{G}$
36	12 5 9 1	grpsubval	$⊢ (y \in {Base}_{G} \land z \in {Base}_{G}) \to y \underset{˙}{-} z = y +_{G} {inv}_{g} (G) (z)$
37	34 35 36	syl2anc	$⊢ ((φ \land y \in T) \land z \in U) \to y \underset{˙}{-} z = y +_{G} {inv}_{g} (G) (z)$
38		oveq2	$⊢ x = {inv}_{g} (G) (z) \to y +_{G} x = y +_{G} {inv}_{g} (G) (z)$
39	38	rspceeqv	$⊢ ({inv}_{g} (G) (z) \in U \land y \underset{˙}{-} z = y +_{G} {inv}_{g} (G) (z)) \to \exists x \in U y \underset{˙}{-} z = y +_{G} x$
40	33 37 39	syl2anc	$⊢ ((φ \land y \in T) \land z \in U) \to \exists x \in U y \underset{˙}{-} z = y +_{G} x$
41		eqeq1	$⊢ X = y \underset{˙}{-} z \to (X = y +_{G} x \leftrightarrow y \underset{˙}{-} z = y +_{G} x)$
42	41	rexbidv	$⊢ X = y \underset{˙}{-} z \to (\exists x \in U X = y +_{G} x \leftrightarrow \exists x \in U y \underset{˙}{-} z = y +_{G} x)$
43	40 42	syl5ibrcom	$⊢ ((φ \land y \in T) \land z \in U) \to (X = y \underset{˙}{-} z \to \exists x \in U X = y +_{G} x)$
44	43	rexlimdva	$⊢ (φ \land y \in T) \to (\exists z \in U X = y \underset{˙}{-} z \to \exists x \in U X = y +_{G} x)$
45	31 44	impbid	$⊢ (φ \land y \in T) \to (\exists x \in U X = y +_{G} x \leftrightarrow \exists z \in U X = y \underset{˙}{-} z)$
46	45	rexbidva	$⊢ φ \to (\exists y \in T \exists x \in U X = y +_{G} x \leftrightarrow \exists y \in T \exists z \in U X = y \underset{˙}{-} z)$
47	7 46	bitrd	$⊢ φ \to (X \in (T \underset{˙}{\oplus} U) \leftrightarrow \exists y \in T \exists z \in U X = y \underset{˙}{-} z)$

Metamath Proof Explorer

Theorem lsmelvalm

Proof