Metamath Proof Explorer


Theorem qustrivr

Description: Converse of qustriv . (Contributed by Thierry Arnoux, 15-Jan-2024)

Ref Expression
Hypotheses qustrivr.1 𝐵 = ( Base ‘ 𝐺 )
qustrivr.2 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝐻 ) )
Assertion qustrivr ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( Base ‘ 𝑄 ) = { 𝐻 } ) → 𝐻 = 𝐵 )

Proof

Step Hyp Ref Expression
1 qustrivr.1 𝐵 = ( Base ‘ 𝐺 )
2 qustrivr.2 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝐻 ) )
3 2 a1i ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝐻 ) ) )
4 1 a1i ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝐵 = ( Base ‘ 𝐺 ) )
5 ovexd ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐺 ~QG 𝐻 ) ∈ V )
6 simpl ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝐺 ∈ Grp )
7 3 4 5 6 qusbas ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐵 / ( 𝐺 ~QG 𝐻 ) ) = ( Base ‘ 𝑄 ) )
8 7 3adant3 ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( Base ‘ 𝑄 ) = { 𝐻 } ) → ( 𝐵 / ( 𝐺 ~QG 𝐻 ) ) = ( Base ‘ 𝑄 ) )
9 simp3 ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( Base ‘ 𝑄 ) = { 𝐻 } ) → ( Base ‘ 𝑄 ) = { 𝐻 } )
10 8 9 eqtrd ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( Base ‘ 𝑄 ) = { 𝐻 } ) → ( 𝐵 / ( 𝐺 ~QG 𝐻 ) ) = { 𝐻 } )
11 10 unieqd ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( Base ‘ 𝑄 ) = { 𝐻 } ) → ( 𝐵 / ( 𝐺 ~QG 𝐻 ) ) = { 𝐻 } )
12 eqid ( 𝐺 ~QG 𝐻 ) = ( 𝐺 ~QG 𝐻 )
13 1 12 eqger ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺 ~QG 𝐻 ) Er 𝐵 )
14 13 adantl ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐺 ~QG 𝐻 ) Er 𝐵 )
15 14 5 uniqs2 ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐵 / ( 𝐺 ~QG 𝐻 ) ) = 𝐵 )
16 15 3adant3 ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( Base ‘ 𝑄 ) = { 𝐻 } ) → ( 𝐵 / ( 𝐺 ~QG 𝐻 ) ) = 𝐵 )
17 unisng ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → { 𝐻 } = 𝐻 )
18 17 3ad2ant2 ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( Base ‘ 𝑄 ) = { 𝐻 } ) → { 𝐻 } = 𝐻 )
19 11 16 18 3eqtr3rd ( ( 𝐺 ∈ Grp ∧ 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( Base ‘ 𝑄 ) = { 𝐻 } ) → 𝐻 = 𝐵 )