Theorem qustrivr

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

	Ref	Expression
Hypotheses	qustrivr.1	|- B = ( Base ` G )
	qustrivr.2	|- Q = ( G /s ( G ~QG H ) )
Assertion	qustrivr	|- ( ( G e. Grp /\ H e. ( SubGrp ` G ) /\ ( Base ` Q ) = { H } ) -> H = B )

Proof

Step	Hyp	Ref	Expression
1		qustrivr.1	|- B = ( Base ` G )
2		qustrivr.2	|- Q = ( G /s ( G ~QG H ) )
3	2	a1i	|- ( ( G e. Grp /\ H e. ( SubGrp ` G ) ) -> Q = ( G /s ( G ~QG H ) ) )
4	1	a1i	|- ( ( G e. Grp /\ H e. ( SubGrp ` G ) ) -> B = ( Base ` G ) )
5		ovexd	|- ( ( G e. Grp /\ H e. ( SubGrp ` G ) ) -> ( G ~QG H ) e. _V )
6		simpl	|- ( ( G e. Grp /\ H e. ( SubGrp ` G ) ) -> G e. Grp )
7	3 4 5 6	qusbas	|- ( ( G e. Grp /\ H e. ( SubGrp ` G ) ) -> ( B /. ( G ~QG H ) ) = ( Base ` Q ) )
8	7	3adant3	|- ( ( G e. Grp /\ H e. ( SubGrp ` G ) /\ ( Base ` Q ) = { H } ) -> ( B /. ( G ~QG H ) ) = ( Base ` Q ) )
9		simp3	|- ( ( G e. Grp /\ H e. ( SubGrp ` G ) /\ ( Base ` Q ) = { H } ) -> ( Base ` Q ) = { H } )
10	8 9	eqtrd	|- ( ( G e. Grp /\ H e. ( SubGrp ` G ) /\ ( Base ` Q ) = { H } ) -> ( B /. ( G ~QG H ) ) = { H } )
11	10	unieqd	|- ( ( G e. Grp /\ H e. ( SubGrp ` G ) /\ ( Base ` Q ) = { H } ) -> U. ( B /. ( G ~QG H ) ) = U. { H } )
12		eqid	|- ( G ~QG H ) = ( G ~QG H )
13	1 12	eqger	|- ( H e. ( SubGrp ` G ) -> ( G ~QG H ) Er B )
14	13	adantl	|- ( ( G e. Grp /\ H e. ( SubGrp ` G ) ) -> ( G ~QG H ) Er B )
15	14 5	uniqs2	|- ( ( G e. Grp /\ H e. ( SubGrp ` G ) ) -> U. ( B /. ( G ~QG H ) ) = B )
16	15	3adant3	|- ( ( G e. Grp /\ H e. ( SubGrp ` G ) /\ ( Base ` Q ) = { H } ) -> U. ( B /. ( G ~QG H ) ) = B )
17		unisng	|- ( H e. ( SubGrp ` G ) -> U. { H } = H )
18	17	3ad2ant2	|- ( ( G e. Grp /\ H e. ( SubGrp ` G ) /\ ( Base ` Q ) = { H } ) -> U. { H } = H )
19	11 16 18	3eqtr3rd	|- ( ( G e. Grp /\ H e. ( SubGrp ` G ) /\ ( Base ` Q ) = { H } ) -> H = B )