Metamath Proof Explorer

Theorem qusinv

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

Ref Expression
Hypotheses qusgrp.h ⊢ 𝐻 = ( 𝐺 /s ( 𝐺 ~QG 𝑆 ) )
qusinv.v ⊢ 𝑉 = ( Base ‘ 𝐺 )
qusinv.i ⊢ 𝐼 = ( invg ‘ 𝐺 )
qusinv.n ⊢ 𝑁 = ( invg ‘ 𝐻 )
Assertion qusinv ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) ) = [ ( 𝐼 ‘ 𝑋 ) ] ( 𝐺 ~QG 𝑆 ) )

Proof

Step Hyp Ref Expression
1 qusgrp.h ⊢ 𝐻 = ( 𝐺 /s ( 𝐺 ~QG 𝑆 ) )
2 qusinv.v ⊢ 𝑉 = ( Base ‘ 𝐺 )
3 qusinv.i ⊢ 𝐼 = ( invg ‘ 𝐺 )
4 qusinv.n ⊢ 𝑁 = ( invg ‘ 𝐻 )
5 nsgsubg ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) )
6 subgrcl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
7 5 6 syl ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
8 2 3 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝑉 ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝑉 )
9 7 8 sylan ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝑉 )
10 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
11 eqid ⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐻 )
12 1 2 10 11 qusadd ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝑉 ) → ( [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) ( +g ‘ 𝐻 ) [ ( 𝐼 ‘ 𝑋 ) ] ( 𝐺 ~QG 𝑆 ) ) = [ ( 𝑋 ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑋 ) ) ] ( 𝐺 ~QG 𝑆 ) )
13 9 12 mpd3an3 ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ) → ( [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) ( +g ‘ 𝐻 ) [ ( 𝐼 ‘ 𝑋 ) ] ( 𝐺 ~QG 𝑆 ) ) = [ ( 𝑋 ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑋 ) ) ] ( 𝐺 ~QG 𝑆 ) )
14 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
15 2 10 14 3 grprinv ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑋 ) ) = ( 0g ‘ 𝐺 ) )
16 7 15 sylan ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑋 ) ) = ( 0g ‘ 𝐺 ) )
17 16 eceq1d ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ) → [ ( 𝑋 ( +g ‘ 𝐺 ) ( 𝐼 ‘ 𝑋 ) ) ] ( 𝐺 ~QG 𝑆 ) = [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑆 ) )
18 1 14 qus0 ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑆 ) = ( 0g ‘ 𝐻 ) )
19 18 adantr ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ) → [ ( 0g ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑆 ) = ( 0g ‘ 𝐻 ) )
20 13 17 19 3eqtrd ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ) → ( [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) ( +g ‘ 𝐻 ) [ ( 𝐼 ‘ 𝑋 ) ] ( 𝐺 ~QG 𝑆 ) ) = ( 0g ‘ 𝐻 ) )
21 1 qusgrp ⊢ ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝐻 ∈ Grp )
22 21 adantr ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ) → 𝐻 ∈ Grp )
23 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
24 1 2 23 quseccl ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ) → [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) ∈ ( Base ‘ 𝐻 ) )
25 1 2 23 quseccl ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ ( 𝐼 ‘ 𝑋 ) ∈ 𝑉 ) → [ ( 𝐼 ‘ 𝑋 ) ] ( 𝐺 ~QG 𝑆 ) ∈ ( Base ‘ 𝐻 ) )
26 9 25 syldan ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ) → [ ( 𝐼 ‘ 𝑋 ) ] ( 𝐺 ~QG 𝑆 ) ∈ ( Base ‘ 𝐻 ) )
27 eqid ⊢ ( 0g ‘ 𝐻 ) = ( 0g ‘ 𝐻 )
28 23 11 27 4 grpinvid1 ⊢ ( ( 𝐻 ∈ Grp ∧ [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) ∈ ( Base ‘ 𝐻 ) ∧ [ ( 𝐼 ‘ 𝑋 ) ] ( 𝐺 ~QG 𝑆 ) ∈ ( Base ‘ 𝐻 ) ) → ( ( 𝑁 ‘ [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) ) = [ ( 𝐼 ‘ 𝑋 ) ] ( 𝐺 ~QG 𝑆 ) ↔ ( [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) ( +g ‘ 𝐻 ) [ ( 𝐼 ‘ 𝑋 ) ] ( 𝐺 ~QG 𝑆 ) ) = ( 0g ‘ 𝐻 ) ) )
29 22 24 26 28 syl3anc ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑁 ‘ [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) ) = [ ( 𝐼 ‘ 𝑋 ) ] ( 𝐺 ~QG 𝑆 ) ↔ ( [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) ( +g ‘ 𝐻 ) [ ( 𝐼 ‘ 𝑋 ) ] ( 𝐺 ~QG 𝑆 ) ) = ( 0g ‘ 𝐻 ) ) )
30 20 29 mpbird ⊢ ( ( 𝑆 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ [ 𝑋 ] ( 𝐺 ~QG 𝑆 ) ) = [ ( 𝐼 ‘ 𝑋 ) ] ( 𝐺 ~QG 𝑆 ) )