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	⊢ 0 = ( 0_g ‘ 𝐺 )
	qus0subg.s	⊢ 𝑆 = { 0 }
	qus0subg.e	⊢ ∼ = ( 𝐺 ~_QG 𝑆 )
	qus0subg.u	⊢ 𝑈 = ( 𝐺 /_s ∼ )
	qus0subg.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
Assertion	qus0subgadd	⊢ ( 𝐺 ∈ Grp → ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( { 𝑎 } ( +_g ‘ 𝑈 ) { 𝑏 } ) = { ( 𝑎 ( +_g ‘ 𝐺 ) 𝑏 ) } )

Proof

Step	Hyp	Ref	Expression
1		qus0subg.0	⊢ 0 = ( 0_g ‘ 𝐺 )
2		qus0subg.s	⊢ 𝑆 = { 0 }
3		qus0subg.e	⊢ ∼ = ( 𝐺 ~_QG 𝑆 )
4		qus0subg.u	⊢ 𝑈 = ( 𝐺 /_s ∼ )
5		qus0subg.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
6	4	a1i	⊢ ( 𝐺 ∈ Grp → 𝑈 = ( 𝐺 /_s ∼ ) )
7	5	a1i	⊢ ( 𝐺 ∈ Grp → 𝐵 = ( Base ‘ 𝐺 ) )
8	1	0subg	⊢ ( 𝐺 ∈ Grp → { 0 } ∈ ( SubGrp ‘ 𝐺 ) )
9	2 8	eqeltrid	⊢ ( 𝐺 ∈ Grp → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
10	5 3	eqger	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ∼ Er 𝐵 )
11	9 10	syl	⊢ ( 𝐺 ∈ Grp → ∼ Er 𝐵 )
12		id	⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Grp )
13	1	0nsg	⊢ ( 𝐺 ∈ Grp → { 0 } ∈ ( NrmSGrp ‘ 𝐺 ) )
14	2 13	eqeltrid	⊢ ( 𝐺 ∈ Grp → 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) )
15		eqid	⊢ ( +_g ‘ 𝐺 ) = ( +_g ‘ 𝐺 )
16	5 3 15	eqgcpbl	⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → ( ( 𝑥 ∼ 𝑝 ∧ 𝑦 ∼ 𝑞 ) → ( 𝑥 ( +_g ‘ 𝐺 ) 𝑦 ) ∼ ( 𝑝 ( +_g ‘ 𝐺 ) 𝑞 ) ) )
17	14 16	syl	⊢ ( 𝐺 ∈ Grp → ( ( 𝑥 ∼ 𝑝 ∧ 𝑦 ∼ 𝑞 ) → ( 𝑥 ( +_g ‘ 𝐺 ) 𝑦 ) ∼ ( 𝑝 ( +_g ‘ 𝐺 ) 𝑞 ) ) )
18	5 15	grpcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) → ( 𝑝 ( +_g ‘ 𝐺 ) 𝑞 ) ∈ 𝐵 )
19	18	3expb	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) → ( 𝑝 ( +_g ‘ 𝐺 ) 𝑞 ) ∈ 𝐵 )
20		eqid	⊢ ( +_g ‘ 𝑈 ) = ( +_g ‘ 𝑈 )
21	6 7 11 12 17 19 15 20	qusaddval	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( [ 𝑎 ] ∼ ( +_g ‘ 𝑈 ) [ 𝑏 ] ∼ ) = [ ( 𝑎 ( +_g ‘ 𝐺 ) 𝑏 ) ] ∼ )
22	21	3expb	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( [ 𝑎 ] ∼ ( +_g ‘ 𝑈 ) [ 𝑏 ] ∼ ) = [ ( 𝑎 ( +_g ‘ 𝐺 ) 𝑏 ) ] ∼ )
23	1 2 5 3	eqg0subgecsn	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑎 ∈ 𝐵 ) → [ 𝑎 ] ∼ = { 𝑎 } )
24	23	adantrr	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → [ 𝑎 ] ∼ = { 𝑎 } )
25	1 2 5 3	eqg0subgecsn	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑏 ∈ 𝐵 ) → [ 𝑏 ] ∼ = { 𝑏 } )
26	25	adantrl	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → [ 𝑏 ] ∼ = { 𝑏 } )
27	24 26	oveq12d	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( [ 𝑎 ] ∼ ( +_g ‘ 𝑈 ) [ 𝑏 ] ∼ ) = ( { 𝑎 } ( +_g ‘ 𝑈 ) { 𝑏 } ) )
28	5 15	grpcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ( +_g ‘ 𝐺 ) 𝑏 ) ∈ 𝐵 )
29	28	3expb	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( +_g ‘ 𝐺 ) 𝑏 ) ∈ 𝐵 )
30	1 2 5 3	eqg0subgecsn	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑎 ( +_g ‘ 𝐺 ) 𝑏 ) ∈ 𝐵 ) → [ ( 𝑎 ( +_g ‘ 𝐺 ) 𝑏 ) ] ∼ = { ( 𝑎 ( +_g ‘ 𝐺 ) 𝑏 ) } )
31	29 30	syldan	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → [ ( 𝑎 ( +_g ‘ 𝐺 ) 𝑏 ) ] ∼ = { ( 𝑎 ( +_g ‘ 𝐺 ) 𝑏 ) } )
32	22 27 31	3eqtr3d	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( { 𝑎 } ( +_g ‘ 𝑈 ) { 𝑏 } ) = { ( 𝑎 ( +_g ‘ 𝐺 ) 𝑏 ) } )
33	32	ralrimivva	⊢ ( 𝐺 ∈ Grp → ∀ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( { 𝑎 } ( +_g ‘ 𝑈 ) { 𝑏 } ) = { ( 𝑎 ( +_g ‘ 𝐺 ) 𝑏 ) } )

Metamath Proof Explorer

Theorem qus0subgadd

Proof