qus0subgadd

Description: The addition in a quotient of a group by the trivial (zero) subgroup. (Contributed by AV, 26-Feb-2025)

	Ref	Expression
Hypotheses	qus0subg.0	$⊢ \underset{˙}{0} = 0_{G}$
	qus0subg.s	$⊢ S = \{\underset{˙}{0}\}$
	qus0subg.e	$⊢ \underset{˙}{\sim} = G ~_{QG} S$
	qus0subg.u	$⊢ U = G /_{𝑠} \underset{˙}{\sim}$
	qus0subg.b	$⊢ B = {Base}_{G}$
Assertion	qus0subgadd	$⊢ G \in Grp \to \forall a \in B \forall b \in B \{a\} +_{U} \{b\} = \{a +_{G} b\}$

Proof

Step	Hyp	Ref	Expression
1		qus0subg.0	$⊢ \underset{˙}{0} = 0_{G}$
2		qus0subg.s	$⊢ S = \{\underset{˙}{0}\}$
3		qus0subg.e	$⊢ \underset{˙}{\sim} = G ~_{QG} S$
4		qus0subg.u	$⊢ U = G /_{𝑠} \underset{˙}{\sim}$
5		qus0subg.b	$⊢ B = {Base}_{G}$
6	4	a1i	$⊢ G \in Grp \to U = G /_{𝑠} \underset{˙}{\sim}$
7	5	a1i	$⊢ G \in Grp \to B = {Base}_{G}$
8	1	0subg	$⊢ G \in Grp \to \{\underset{˙}{0}\} \in SubGrp (G)$
9	2 8	eqeltrid	$⊢ G \in Grp \to S \in SubGrp (G)$
10	5 3	eqger	$⊢ S \in SubGrp (G) \to \underset{˙}{\sim} Er B$
11	9 10	syl	$⊢ G \in Grp \to \underset{˙}{\sim} Er B$
12		id	$⊢ G \in Grp \to G \in Grp$
13	1	0nsg	$⊢ G \in Grp \to \{\underset{˙}{0}\} \in NrmSGrp (G)$
14	2 13	eqeltrid	$⊢ G \in Grp \to S \in NrmSGrp (G)$
15		eqid	$⊢ +_{G} = +_{G}$
16	5 3 15	eqgcpbl	$⊢ S \in NrmSGrp (G) \to ((x \underset{˙}{\sim} p \land y \underset{˙}{\sim} q) \to (x +_{G} y) \underset{˙}{\sim} (p +_{G} q))$
17	14 16	syl	$⊢ G \in Grp \to ((x \underset{˙}{\sim} p \land y \underset{˙}{\sim} q) \to (x +_{G} y) \underset{˙}{\sim} (p +_{G} q))$
18	5 15	grpcl	$⊢ (G \in Grp \land p \in B \land q \in B) \to p +_{G} q \in B$
19	18	3expb	$⊢ (G \in Grp \land (p \in B \land q \in B)) \to p +_{G} q \in B$
20		eqid	$⊢ +_{U} = +_{U}$
21	6 7 11 12 17 19 15 20	qusaddval	$⊢ (G \in Grp \land a \in B \land b \in B) \to [a] \underset{˙}{\sim} +_{U} [b] \underset{˙}{\sim} = [(a +_{G} b)] \underset{˙}{\sim}$
22	21	3expb	$⊢ (G \in Grp \land (a \in B \land b \in B)) \to [a] \underset{˙}{\sim} +_{U} [b] \underset{˙}{\sim} = [(a +_{G} b)] \underset{˙}{\sim}$
23	1 2 5 3	eqg0subgecsn	$⊢ (G \in Grp \land a \in B) \to [a] \underset{˙}{\sim} = \{a\}$
24	23	adantrr	$⊢ (G \in Grp \land (a \in B \land b \in B)) \to [a] \underset{˙}{\sim} = \{a\}$
25	1 2 5 3	eqg0subgecsn	$⊢ (G \in Grp \land b \in B) \to [b] \underset{˙}{\sim} = \{b\}$
26	25	adantrl	$⊢ (G \in Grp \land (a \in B \land b \in B)) \to [b] \underset{˙}{\sim} = \{b\}$
27	24 26	oveq12d	$⊢ (G \in Grp \land (a \in B \land b \in B)) \to [a] \underset{˙}{\sim} +_{U} [b] \underset{˙}{\sim} = \{a\} +_{U} \{b\}$
28	5 15	grpcl	$⊢ (G \in Grp \land a \in B \land b \in B) \to a +_{G} b \in B$
29	28	3expb	$⊢ (G \in Grp \land (a \in B \land b \in B)) \to a +_{G} b \in B$
30	1 2 5 3	eqg0subgecsn	$⊢ (G \in Grp \land a +_{G} b \in B) \to [(a +_{G} b)] \underset{˙}{\sim} = \{a +_{G} b\}$
31	29 30	syldan	$⊢ (G \in Grp \land (a \in B \land b \in B)) \to [(a +_{G} b)] \underset{˙}{\sim} = \{a +_{G} b\}$
32	22 27 31	3eqtr3d	$⊢ (G \in Grp \land (a \in B \land b \in B)) \to \{a\} +_{U} \{b\} = \{a +_{G} b\}$
33	32	ralrimivva	$⊢ G \in Grp \to \forall a \in B \forall b \in B \{a\} +_{U} \{b\} = \{a +_{G} b\}$

Metamath Proof Explorer

Theorem qus0subgadd

Proof