# Metamath Proof Explorer

## Theorem qusgrp2

Description: Prove that a quotient structure is a group. (Contributed by Mario Carneiro, 14-Jun-2015) (Revised by Mario Carneiro, 12-Aug-2015)

Ref Expression
Hypotheses qusgrp2.u
qusgrp2.v ${⊢}{\phi }\to {V}={\mathrm{Base}}_{{R}}$
qusgrp2.p
qusgrp2.r
qusgrp2.x ${⊢}{\phi }\to {R}\in {X}$
qusgrp2.e
qusgrp2.1
qusgrp2.2
qusgrp2.3
qusgrp2.4
qusgrp2.5 ${⊢}\left({\phi }\wedge {x}\in {V}\right)\to {N}\in {V}$
qusgrp2.6
Assertion qusgrp2

### Proof

Step Hyp Ref Expression
1 qusgrp2.u
2 qusgrp2.v ${⊢}{\phi }\to {V}={\mathrm{Base}}_{{R}}$
3 qusgrp2.p
4 qusgrp2.r
5 qusgrp2.x ${⊢}{\phi }\to {R}\in {X}$
6 qusgrp2.e
7 qusgrp2.1
8 qusgrp2.2
9 qusgrp2.3
10 qusgrp2.4
11 qusgrp2.5 ${⊢}\left({\phi }\wedge {x}\in {V}\right)\to {N}\in {V}$
12 qusgrp2.6
13 eqid
14 fvex ${⊢}{\mathrm{Base}}_{{R}}\in \mathrm{V}$
15 2 14 syl6eqel ${⊢}{\phi }\to {V}\in \mathrm{V}$
16 erex
17 4 15 16 sylc
18 1 2 13 17 5 qusval
19 1 2 13 17 5 quslem
20 7 3expb
21 4 15 13 20 6 ercpbl
23 22 8 erthi
24 15 adantr ${⊢}\left({\phi }\wedge \left({x}\in {V}\wedge {y}\in {V}\wedge {z}\in {V}\right)\right)\to {V}\in \mathrm{V}$
25 22 24 13 divsfval
26 22 24 13 divsfval
27 23 25 26 3eqtr4d
29 28 10 erthi
30 15 adantr ${⊢}\left({\phi }\wedge {x}\in {V}\right)\to {V}\in \mathrm{V}$
31 28 30 13 divsfval
32 28 30 13 divsfval
33 29 31 32 3eqtr4d
34 28 12 ersym
35 28 34 erthi
36 28 30 13 divsfval
37 28 30 13 divsfval
38 35 36 37 3eqtr4rd
39 18 2 3 19 21 5 7 27 9 33 11 38 imasgrp2
40 4 15 13 divsfval
41 40 eqcomd
42 41 eqeq1d
43 42 anbi2d
44 39 43 mpbird