This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ↾ 𝐵 ) )