eqg0subg

Description: The coset equivalence relation for the trivial (zero) subgroup of a group is the identity relation restricted to the base set of the group. (Contributed by AV, 25-Feb-2025)

	Ref	Expression
Hypotheses	eqg0subg.0	$⊢ \underset{˙}{0} = 0_{G}$
	eqg0subg.s	$⊢ S = \{\underset{˙}{0}\}$
	eqg0subg.b	$⊢ B = {Base}_{G}$
	eqg0subg.r	$⊢ R = G ~_{QG} S$
Assertion	eqg0subg	$⊢ G \in Grp \to R = {I ↾}_{B}$

Proof

Step	Hyp	Ref	Expression
1		eqg0subg.0	$⊢ \underset{˙}{0} = 0_{G}$
2		eqg0subg.s	$⊢ S = \{\underset{˙}{0}\}$
3		eqg0subg.b	$⊢ B = {Base}_{G}$
4		eqg0subg.r	$⊢ R = G ~_{QG} S$
5	1	0subg	$⊢ G \in Grp \to \{\underset{˙}{0}\} \in SubGrp (G)$
6	3	subgss	$⊢ \{\underset{˙}{0}\} \in SubGrp (G) \to \{\underset{˙}{0}\} \subseteq B$
7	5 6	syl	$⊢ G \in Grp \to \{\underset{˙}{0}\} \subseteq B$
8	2 7	eqsstrid	$⊢ G \in Grp \to S \subseteq B$
9		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
10		eqid	$⊢ +_{G} = +_{G}$
11	3 9 10 4	eqgfval	$⊢ (G \in Grp \land S \subseteq B) \to R = \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land {inv}_{g} (G) (x) +_{G} y \in S)\}$
12	8 11	mpdan	$⊢ G \in Grp \to R = \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land {inv}_{g} (G) (x) +_{G} y \in S)\}$
13		opabresid	$⊢ {I ↾}_{B} = \{⟨x, y⟩ \| (x \in B \land y = x)\}$
14		simpl	$⊢ (x \in B \land y = x) \to x \in B$
15		eleq1w	$⊢ x = y \to (x \in B \leftrightarrow y \in B)$
16	15	equcoms	$⊢ y = x \to (x \in B \leftrightarrow y \in B)$
17	16	biimpac	$⊢ (x \in B \land y = x) \to y \in B$
18		simpr	$⊢ (x \in B \land y = x) \to y = x$
19	14 17 18	jca31	$⊢ (x \in B \land y = x) \to ((x \in B \land y \in B) \land y = x)$
20		simpl	$⊢ (x \in B \land y \in B) \to x \in B$
21	20	anim1i	$⊢ ((x \in B \land y \in B) \land y = x) \to (x \in B \land y = x)$
22	21	a1i	$⊢ G \in Grp \to (((x \in B \land y \in B) \land y = x) \to (x \in B \land y = x))$
23	19 22	impbid2	$⊢ G \in Grp \to ((x \in B \land y = x) \leftrightarrow ((x \in B \land y \in B) \land y = x))$
24		simpl	$⊢ (G \in Grp \land (x \in B \land y \in B)) \to G \in Grp$
25		simpr	$⊢ (x \in B \land y \in B) \to y \in B$
26	25	adantl	$⊢ (G \in Grp \land (x \in B \land y \in B)) \to y \in B$
27	20	adantl	$⊢ (G \in Grp \land (x \in B \land y \in B)) \to x \in B$
28	3 9 24 26 27	grpinv11	$⊢ (G \in Grp \land (x \in B \land y \in B)) \to ({inv}_{g} (G) (y) = {inv}_{g} (G) (x) \leftrightarrow y = x)$
29	3 9	grpinvcl	$⊢ (G \in Grp \land x \in B) \to {inv}_{g} (G) (x) \in B$
30	29	adantrr	$⊢ (G \in Grp \land (x \in B \land y \in B)) \to {inv}_{g} (G) (x) \in B$
31	3 10 1 9	grpinvid2	$⊢ (G \in Grp \land y \in B \land {inv}_{g} (G) (x) \in B) \to ({inv}_{g} (G) (y) = {inv}_{g} (G) (x) \leftrightarrow {inv}_{g} (G) (x) +_{G} y = \underset{˙}{0})$
32	24 26 30 31	syl3anc	$⊢ (G \in Grp \land (x \in B \land y \in B)) \to ({inv}_{g} (G) (y) = {inv}_{g} (G) (x) \leftrightarrow {inv}_{g} (G) (x) +_{G} y = \underset{˙}{0})$
33	28 32	bitr3d	$⊢ (G \in Grp \land (x \in B \land y \in B)) \to (y = x \leftrightarrow {inv}_{g} (G) (x) +_{G} y = \underset{˙}{0})$
34	33	pm5.32da	$⊢ G \in Grp \to (((x \in B \land y \in B) \land y = x) \leftrightarrow ((x \in B \land y \in B) \land {inv}_{g} (G) (x) +_{G} y = \underset{˙}{0}))$
35		vex	$⊢ x \in V$
36		vex	$⊢ y \in V$
37	35 36	prss	$⊢ (x \in B \land y \in B) \leftrightarrow \{x, y\} \subseteq B$
38	37	a1i	$⊢ G \in Grp \to ((x \in B \land y \in B) \leftrightarrow \{x, y\} \subseteq B)$
39	2	eleq2i	$⊢ {inv}_{g} (G) (x) +_{G} y \in S \leftrightarrow {inv}_{g} (G) (x) +_{G} y \in \{\underset{˙}{0}\}$
40		ovex	$⊢ {inv}_{g} (G) (x) +_{G} y \in V$
41	40	elsn	$⊢ {inv}_{g} (G) (x) +_{G} y \in \{\underset{˙}{0}\} \leftrightarrow {inv}_{g} (G) (x) +_{G} y = \underset{˙}{0}$
42	39 41	bitr2i	$⊢ {inv}_{g} (G) (x) +_{G} y = \underset{˙}{0} \leftrightarrow {inv}_{g} (G) (x) +_{G} y \in S$
43	42	a1i	$⊢ G \in Grp \to ({inv}_{g} (G) (x) +_{G} y = \underset{˙}{0} \leftrightarrow {inv}_{g} (G) (x) +_{G} y \in S)$
44	38 43	anbi12d	$⊢ G \in Grp \to (((x \in B \land y \in B) \land {inv}_{g} (G) (x) +_{G} y = \underset{˙}{0}) \leftrightarrow (\{x, y\} \subseteq B \land {inv}_{g} (G) (x) +_{G} y \in S))$
45	23 34 44	3bitrd	$⊢ G \in Grp \to ((x \in B \land y = x) \leftrightarrow (\{x, y\} \subseteq B \land {inv}_{g} (G) (x) +_{G} y \in S))$
46	45	opabbidv	$⊢ G \in Grp \to \{⟨x, y⟩ \| (x \in B \land y = x)\} = \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land {inv}_{g} (G) (x) +_{G} y \in S)\}$
47	13 46	eqtr2id	$⊢ G \in Grp \to \{⟨x, y⟩ \| (\{x, y\} \subseteq B \land {inv}_{g} (G) (x) +_{G} y \in S)\} = {I ↾}_{B}$
48	12 47	eqtrd	$⊢ G \in Grp \to R = {I ↾}_{B}$

Metamath Proof Explorer

Theorem eqg0subg

Proof