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