Metamath Proof Explorer

Theorem qus0

Description: Value of the group identity operation in a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015)

Ref Expression
Hypotheses qusgrp.h ⊢ 𝐻 = ( 𝐺 /s ( 𝐺 ~QG 𝑆 ) )
qus0.p ⊢ 0 = ( 0g ‘ 𝐺 )
Assertion qus0 ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → [ 0 ] ( 𝐺 ~QG 𝑆 ) = ( 0g ‘ 𝐻 ) )

Proof

Step Hyp Ref Expression
1 qusgrp.h ⊢ 𝐻 = ( 𝐺 /s ( 𝐺 ~QG 𝑆 ) )
2 qus0.p ⊢ 0 = ( 0g ‘ 𝐺 )
3 nsgsubg ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
4 subgrcl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
5 3 4 syl ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
6 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
7 6 2 grpidcl ⊢ ( 𝐺 ∈ Grp → 0 ∈ ( Base ‘ 𝐺 ) )
8 5 7 syl ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → 0 ∈ ( Base ‘ 𝐺 ) )
9 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
10 eqid ⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐻 )
11 1 6 9 10 qusadd ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 0 ∈ ( Base ‘ 𝐺 ) ∧ 0 ∈ ( Base ‘ 𝐺 ) ) → ( [ 0 ] ( 𝐺 ~QG 𝑆 ) ( +g ‘ 𝐻 ) [ 0 ] ( 𝐺 ~QG 𝑆 ) ) = [ ( 0 ( +g ‘ 𝐺 ) 0 ) ] ( 𝐺 ~QG 𝑆 ) )
12 8 8 11 mpd3an23 ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → ( [ 0 ] ( 𝐺 ~QG 𝑆 ) ( +g ‘ 𝐻 ) [ 0 ] ( 𝐺 ~QG 𝑆 ) ) = [ ( 0 ( +g ‘ 𝐺 ) 0 ) ] ( 𝐺 ~QG 𝑆 ) )
13 6 9 2 grplid ⊢ ( ( 𝐺 ∈ Grp ∧ 0 ∈ ( Base ‘ 𝐺 ) ) → ( 0 ( +g ‘ 𝐺 ) 0 ) = 0 )
14 5 8 13 syl2anc ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → ( 0 ( +g ‘ 𝐺 ) 0 ) = 0 )
15 14 eceq1d ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → [ ( 0 ( +g ‘ 𝐺 ) 0 ) ] ( 𝐺 ~QG 𝑆 ) = [ 0 ] ( 𝐺 ~QG 𝑆 ) )
16 12 15 eqtrd ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → ( [ 0 ] ( 𝐺 ~QG 𝑆 ) ( +g ‘ 𝐻 ) [ 0 ] ( 𝐺 ~QG 𝑆 ) ) = [ 0 ] ( 𝐺 ~QG 𝑆 ) )
17 1 qusgrp ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝐻 ∈ Grp )
18 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
19 1 6 18 quseccl ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 0 ∈ ( Base ‘ 𝐺 ) ) → [ 0 ] ( 𝐺 ~QG 𝑆 ) ∈ ( Base ‘ 𝐻 ) )
20 8 19 mpdan ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → [ 0 ] ( 𝐺 ~QG 𝑆 ) ∈ ( Base ‘ 𝐻 ) )
21 eqid ⊢ ( 0g ‘ 𝐻 ) = ( 0g ‘ 𝐻 )
22 18 10 21 grpid ⊢ ( ( 𝐻 ∈ Grp ∧ [ 0 ] ( 𝐺 ~QG 𝑆 ) ∈ ( Base ‘ 𝐻 ) ) → ( ( [ 0 ] ( 𝐺 ~QG 𝑆 ) ( +g ‘ 𝐻 ) [ 0 ] ( 𝐺 ~QG 𝑆 ) ) = [ 0 ] ( 𝐺 ~QG 𝑆 ) ↔ ( 0g ‘ 𝐻 ) = [ 0 ] ( 𝐺 ~QG 𝑆 ) ) )
23 17 20 22 syl2anc ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → ( ( [ 0 ] ( 𝐺 ~QG 𝑆 ) ( +g ‘ 𝐻 ) [ 0 ] ( 𝐺 ~QG 𝑆 ) ) = [ 0 ] ( 𝐺 ~QG 𝑆 ) ↔ ( 0g ‘ 𝐻 ) = [ 0 ] ( 𝐺 ~QG 𝑆 ) ) )
24 16 23 mpbid ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → ( 0g ‘ 𝐻 ) = [ 0 ] ( 𝐺 ~QG 𝑆 ) )
25 24 eqcomd ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → [ 0 ] ( 𝐺 ~QG 𝑆 ) = ( 0g ‘ 𝐻 ) )