Theorem 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	⊢ 0 = ( 0g ‘ 𝐺 )
	eqg0subg.s	⊢ 𝑆 = { 0 }
	eqg0subg.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	eqg0subg.r	⊢ 𝑅 = ( 𝐺 ~QG 𝑆 )
Assertion	eqg0subg	⊢ ( 𝐺 ∈ Grp → 𝑅 = ( I ↾ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		eqg0subg.0	⊢ 0 = ( 0g ‘ 𝐺 )
2		eqg0subg.s	⊢ 𝑆 = { 0 }
3		eqg0subg.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
4		eqg0subg.r	⊢ 𝑅 = ( 𝐺 ~QG 𝑆 )
5	1	0subg	⊢ ( 𝐺 ∈ Grp → { 0 } ∈ ( SubGrp ‘ 𝐺 ) )
6	3	subgss	⊢ ( { 0 } ∈ ( SubGrp ‘ 𝐺 ) → { 0 } ⊆ 𝐵 )
7	5 6	syl	⊢ ( 𝐺 ∈ Grp → { 0 } ⊆ 𝐵 )
8	2 7	eqsstrid	⊢ ( 𝐺 ∈ Grp → 𝑆 ⊆ 𝐵 )
9		eqid	⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
10		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
11	3 9 10 4	eqgfval	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) → 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ) } )
12	8 11	mpdan	⊢ ( 𝐺 ∈ Grp → 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ) } )
13		opabresid	⊢ ( I ↾ 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 = 𝑥 ) }
14		simpl	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 = 𝑥 ) → 𝑥 ∈ 𝐵 )
15		eleq1w	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵 ) )
16	15	equcoms	⊢ ( 𝑦 = 𝑥 → ( 𝑥 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵 ) )
17	16	biimpac	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 = 𝑥 ) → 𝑦 ∈ 𝐵 )
18		simpr	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 = 𝑥 ) → 𝑦 = 𝑥 )
19	14 17 18	jca31	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 = 𝑥 ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 = 𝑥 ) )
20		simpl	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
21	20	anim1i	⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 = 𝑥 ) → ( 𝑥 ∈ 𝐵 ∧ 𝑦 = 𝑥 ) )
22	21	a1i	⊢ ( 𝐺 ∈ Grp → ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 = 𝑥 ) → ( 𝑥 ∈ 𝐵 ∧ 𝑦 = 𝑥 ) ) )
23	19 22	impbid2	⊢ ( 𝐺 ∈ Grp → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 = 𝑥 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 = 𝑥 ) ) )
24		simpl	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐺 ∈ Grp )
25		simpr	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
26	25	adantl	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
27	20	adantl	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
28	3 9 24 26 27	grpinv11	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) = ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ↔ 𝑦 = 𝑥 ) )
29	3 9	grpinvcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐵 )
30	29	adantrr	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐵 )
31	3 10 1 9	grpinvid2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ 𝐵 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐵 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) = ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) 𝑦 ) = 0 ) )
32	24 26 30 31	syl3anc	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) = ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) 𝑦 ) = 0 ) )
33	28 32	bitr3d	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑦 = 𝑥 ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) 𝑦 ) = 0 ) )
34	33	pm5.32da	⊢ ( 𝐺 ∈ Grp → ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑦 = 𝑥 ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) 𝑦 ) = 0 ) ) )
35		vex	⊢ 𝑥 ∈ V
36		vex	⊢ 𝑦 ∈ V
37	35 36	prss	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ↔ { 𝑥 , 𝑦 } ⊆ 𝐵 )
38	37	a1i	⊢ ( 𝐺 ∈ Grp → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ↔ { 𝑥 , 𝑦 } ⊆ 𝐵 ) )
39	2	eleq2i	⊢ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) 𝑦 ) ∈ { 0 } )
40		ovex	⊢ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) 𝑦 ) ∈ V
41	40	elsn	⊢ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) 𝑦 ) ∈ { 0 } ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) 𝑦 ) = 0 )
42	39 41	bitr2i	⊢ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) 𝑦 ) = 0 ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 )
43	42	a1i	⊢ ( 𝐺 ∈ Grp → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) 𝑦 ) = 0 ↔ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ) )
44	38 43	anbi12d	⊢ ( 𝐺 ∈ Grp → ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) 𝑦 ) = 0 ) ↔ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ) ) )
45	23 34 44	3bitrd	⊢ ( 𝐺 ∈ Grp → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 = 𝑥 ) ↔ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ) ) )
46	45	opabbidv	⊢ ( 𝐺 ∈ Grp → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐵 ∧ 𝑦 = 𝑥 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ) } )
47	13 46	eqtr2id	⊢ ( 𝐺 ∈ Grp → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝐵 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ) } = ( I ↾ 𝐵 ) )
48	12 47	eqtrd	⊢ ( 𝐺 ∈ Grp → 𝑅 = ( I ↾ 𝐵 ) )