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