Metamath Proof Explorer


Theorem qustrivr

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

Ref Expression
Hypotheses qustrivr.1 B=BaseG
qustrivr.2 Q=G/𝑠G~QGH
Assertion qustrivr GGrpHSubGrpGBaseQ=HH=B

Proof

Step Hyp Ref Expression
1 qustrivr.1 B=BaseG
2 qustrivr.2 Q=G/𝑠G~QGH
3 2 a1i GGrpHSubGrpGQ=G/𝑠G~QGH
4 1 a1i GGrpHSubGrpGB=BaseG
5 ovexd GGrpHSubGrpGG~QGHV
6 simpl GGrpHSubGrpGGGrp
7 3 4 5 6 qusbas GGrpHSubGrpGB/G~QGH=BaseQ
8 7 3adant3 GGrpHSubGrpGBaseQ=HB/G~QGH=BaseQ
9 simp3 GGrpHSubGrpGBaseQ=HBaseQ=H
10 8 9 eqtrd GGrpHSubGrpGBaseQ=HB/G~QGH=H
11 10 unieqd GGrpHSubGrpGBaseQ=HB/G~QGH=H
12 eqid G~QGH=G~QGH
13 1 12 eqger HSubGrpGG~QGHErB
14 13 adantl GGrpHSubGrpGG~QGHErB
15 14 5 uniqs2 GGrpHSubGrpGB/G~QGH=B
16 15 3adant3 GGrpHSubGrpGBaseQ=HB/G~QGH=B
17 unisng HSubGrpGH=H
18 17 3ad2ant2 GGrpHSubGrpGBaseQ=HH=H
19 11 16 18 3eqtr3rd GGrpHSubGrpGBaseQ=HH=B