Metamath Proof Explorer


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 / 𝑠 G ~ QG H
Assertion qustrivr G Grp H SubGrp G Base Q = H H = B

Proof

Step Hyp Ref Expression
1 qustrivr.1 B = Base G
2 qustrivr.2 Q = G / 𝑠 G ~ QG H
3 2 a1i G Grp H SubGrp G Q = G / 𝑠 G ~ QG H
4 1 a1i G Grp H SubGrp G B = Base G
5 ovexd G Grp H SubGrp G G ~ QG H V
6 simpl G Grp H SubGrp G G Grp
7 3 4 5 6 qusbas G Grp H SubGrp G B / G ~ QG H = Base Q
8 7 3adant3 G Grp H SubGrp G Base Q = H B / G ~ QG H = Base Q
9 simp3 G Grp H SubGrp G Base Q = H Base Q = H
10 8 9 eqtrd G Grp H SubGrp G Base Q = H B / G ~ QG H = H
11 10 unieqd G Grp H SubGrp G Base Q = H B / G ~ QG H = H
12 eqid G ~ QG H = G ~ QG H
13 1 12 eqger H SubGrp G G ~ QG H Er B
14 13 adantl G Grp H SubGrp G G ~ QG H Er B
15 14 5 uniqs2 G Grp H SubGrp G B / G ~ QG H = B
16 15 3adant3 G Grp H SubGrp G Base Q = H B / G ~ QG H = B
17 unisng H SubGrp G H = H
18 17 3ad2ant2 G Grp H SubGrp G Base Q = H H = H
19 11 16 18 3eqtr3rd G Grp H SubGrp G Base Q = H H = B