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

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 ‘ 𝑄 ) = { 𝐻 } ) → 𝐻 = 𝐵 )