grplsmid

Description: The direct sum of an element X of a subgroup A is the subgroup itself. (Contributed by Thierry Arnoux, 27-Jul-2024)

		Ref	Expression
	Hypothesis	grplsmid.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
	Assertion	grplsmid	$⊢ (A \in SubGrp (G) \land X \in A) \to \{X\} \underset{˙}{\oplus} A = A$

Proof

Step	Hyp	Ref	Expression
1		grplsmid.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
2		subgrcl	$⊢ A \in SubGrp (G) \to G \in Grp$
3	2	adantr	$⊢ (A \in SubGrp (G) \land X \in A) \to G \in Grp$
4		eqid	$⊢ {Base}_{G} = {Base}_{G}$
5	4	subgss	$⊢ A \in SubGrp (G) \to A \subseteq {Base}_{G}$
6	5	sselda	$⊢ (A \in SubGrp (G) \land X \in A) \to X \in {Base}_{G}$
7	6	snssd	$⊢ (A \in SubGrp (G) \land X \in A) \to \{X\} \subseteq {Base}_{G}$
8	5	adantr	$⊢ (A \in SubGrp (G) \land X \in A) \to A \subseteq {Base}_{G}$
9		eqid	$⊢ +_{G} = +_{G}$
10	4 9 1	lsmelvalx	$⊢ (G \in Grp \land \{X\} \subseteq {Base}_{G} \land A \subseteq {Base}_{G}) \to (x \in (\{X\} \underset{˙}{\oplus} A) \leftrightarrow \exists o \in \{X\} \exists a \in A x = o +_{G} a)$
11	3 7 8 10	syl3anc	$⊢ (A \in SubGrp (G) \land X \in A) \to (x \in (\{X\} \underset{˙}{\oplus} A) \leftrightarrow \exists o \in \{X\} \exists a \in A x = o +_{G} a)$
12		oveq1	$⊢ o = X \to o +_{G} a = X +_{G} a$
13	12	eqeq2d	$⊢ o = X \to (x = o +_{G} a \leftrightarrow x = X +_{G} a)$
14	13	rexbidv	$⊢ o = X \to (\exists a \in A x = o +_{G} a \leftrightarrow \exists a \in A x = X +_{G} a)$
15	14	rexsng	$⊢ X \in A \to (\exists o \in \{X\} \exists a \in A x = o +_{G} a \leftrightarrow \exists a \in A x = X +_{G} a)$
16	15	adantl	$⊢ (A \in SubGrp (G) \land X \in A) \to (\exists o \in \{X\} \exists a \in A x = o +_{G} a \leftrightarrow \exists a \in A x = X +_{G} a)$
17		simpr	$⊢ (((A \in SubGrp (G) \land X \in A) \land a \in A) \land x = X +_{G} a) \to x = X +_{G} a$
18	9	subgcl	$⊢ (A \in SubGrp (G) \land X \in A \land a \in A) \to X +_{G} a \in A$
19	18	ad4ant123	$⊢ (((A \in SubGrp (G) \land X \in A) \land a \in A) \land x = X +_{G} a) \to X +_{G} a \in A$
20	17 19	eqeltrd	$⊢ (((A \in SubGrp (G) \land X \in A) \land a \in A) \land x = X +_{G} a) \to x \in A$
21	20	r19.29an	$⊢ ((A \in SubGrp (G) \land X \in A) \land \exists a \in A x = X +_{G} a) \to x \in A$
22		simpll	$⊢ ((A \in SubGrp (G) \land X \in A) \land x \in A) \to A \in SubGrp (G)$
23		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
24	23	subginvcl	$⊢ (A \in SubGrp (G) \land X \in A) \to {inv}_{g} (G) (X) \in A$
25	24	adantr	$⊢ ((A \in SubGrp (G) \land X \in A) \land x \in A) \to {inv}_{g} (G) (X) \in A$
26		simpr	$⊢ ((A \in SubGrp (G) \land X \in A) \land x \in A) \to x \in A$
27	9	subgcl	$⊢ (A \in SubGrp (G) \land {inv}_{g} (G) (X) \in A \land x \in A) \to {inv}_{g} (G) (X) +_{G} x \in A$
28	22 25 26 27	syl3anc	$⊢ ((A \in SubGrp (G) \land X \in A) \land x \in A) \to {inv}_{g} (G) (X) +_{G} x \in A$
29		oveq2	$⊢ a = {inv}_{g} (G) (X) +_{G} x \to X +_{G} a = X +_{G} ({inv}_{g} (G) (X) +_{G} x)$
30	29	eqeq2d	$⊢ a = {inv}_{g} (G) (X) +_{G} x \to (x = X +_{G} a \leftrightarrow x = X +_{G} ({inv}_{g} (G) (X) +_{G} x))$
31	30	adantl	$⊢ (((A \in SubGrp (G) \land X \in A) \land x \in A) \land a = {inv}_{g} (G) (X) +_{G} x) \to (x = X +_{G} a \leftrightarrow x = X +_{G} ({inv}_{g} (G) (X) +_{G} x))$
32	3	adantr	$⊢ ((A \in SubGrp (G) \land X \in A) \land x \in A) \to G \in Grp$
33	6	adantr	$⊢ ((A \in SubGrp (G) \land X \in A) \land x \in A) \to X \in {Base}_{G}$
34	8	sselda	$⊢ ((A \in SubGrp (G) \land X \in A) \land x \in A) \to x \in {Base}_{G}$
35	4 9 23	grpasscan1	$⊢ (G \in Grp \land X \in {Base}_{G} \land x \in {Base}_{G}) \to X +_{G} ({inv}_{g} (G) (X) +_{G} x) = x$
36	32 33 34 35	syl3anc	$⊢ ((A \in SubGrp (G) \land X \in A) \land x \in A) \to X +_{G} ({inv}_{g} (G) (X) +_{G} x) = x$
37	36	eqcomd	$⊢ ((A \in SubGrp (G) \land X \in A) \land x \in A) \to x = X +_{G} ({inv}_{g} (G) (X) +_{G} x)$
38	28 31 37	rspcedvd	$⊢ ((A \in SubGrp (G) \land X \in A) \land x \in A) \to \exists a \in A x = X +_{G} a$
39	21 38	impbida	$⊢ (A \in SubGrp (G) \land X \in A) \to (\exists a \in A x = X +_{G} a \leftrightarrow x \in A)$
40	11 16 39	3bitrd	$⊢ (A \in SubGrp (G) \land X \in A) \to (x \in (\{X\} \underset{˙}{\oplus} A) \leftrightarrow x \in A)$
41	40	eqrdv	$⊢ (A \in SubGrp (G) \land X \in A) \to \{X\} \underset{˙}{\oplus} A = A$

Metamath Proof Explorer

Theorem grplsmid

Proof