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 φ U = R / 𝑠 ˙
qusgrp2.v φ V = Base R
qusgrp2.p φ + ˙ = + R
qusgrp2.r φ ˙ Er V
qusgrp2.x φ R X
qusgrp2.e φ a ˙ p b ˙ q a + ˙ b ˙ p + ˙ q
qusgrp2.1 φ x V y V x + ˙ y V
qusgrp2.2 φ x V y V z V x + ˙ y + ˙ z ˙ x + ˙ y + ˙ z
qusgrp2.3 φ 0 ˙ V
qusgrp2.4 φ x V 0 ˙ + ˙ x ˙ x
qusgrp2.5 φ x V N V
qusgrp2.6 φ x V N + ˙ x ˙ 0 ˙
Assertion qusgrp2 φ U Grp 0 ˙ ˙ = 0 U

Proof

Step Hyp Ref Expression
1 qusgrp2.u φ U = R / 𝑠 ˙
2 qusgrp2.v φ V = Base R
3 qusgrp2.p φ + ˙ = + R
4 qusgrp2.r φ ˙ Er V
5 qusgrp2.x φ R X
6 qusgrp2.e φ a ˙ p b ˙ q a + ˙ b ˙ p + ˙ q
7 qusgrp2.1 φ x V y V x + ˙ y V
8 qusgrp2.2 φ x V y V z V x + ˙ y + ˙ z ˙ x + ˙ y + ˙ z
9 qusgrp2.3 φ 0 ˙ V
10 qusgrp2.4 φ x V 0 ˙ + ˙ x ˙ x
11 qusgrp2.5 φ x V N V
12 qusgrp2.6 φ x V N + ˙ x ˙ 0 ˙
13 eqid u V u ˙ = u V u ˙
14 fvex Base R V
15 2 14 syl6eqel φ V V
16 erex ˙ Er V V V ˙ V
17 4 15 16 sylc φ ˙ V
18 1 2 13 17 5 qusval φ U = u V u ˙ 𝑠 R
19 1 2 13 17 5 quslem φ u V u ˙ : V onto V / ˙
20 7 3expb φ x V y V x + ˙ y V
21 4 15 13 20 6 ercpbl φ a V b V p V q V u V u ˙ a = u V u ˙ p u V u ˙ b = u V u ˙ q u V u ˙ a + ˙ b = u V u ˙ p + ˙ q
22 4 adantr φ x V y V z V ˙ Er V
23 22 8 erthi φ x V y V z V x + ˙ y + ˙ z ˙ = x + ˙ y + ˙ z ˙
24 15 adantr φ x V y V z V V V
25 22 24 13 divsfval φ x V y V z V u V u ˙ x + ˙ y + ˙ z = x + ˙ y + ˙ z ˙
26 22 24 13 divsfval φ x V y V z V u V u ˙ x + ˙ y + ˙ z = x + ˙ y + ˙ z ˙
27 23 25 26 3eqtr4d φ x V y V z V u V u ˙ x + ˙ y + ˙ z = u V u ˙ x + ˙ y + ˙ z
28 4 adantr φ x V ˙ Er V
29 28 10 erthi φ x V 0 ˙ + ˙ x ˙ = x ˙
30 15 adantr φ x V V V
31 28 30 13 divsfval φ x V u V u ˙ 0 ˙ + ˙ x = 0 ˙ + ˙ x ˙
32 28 30 13 divsfval φ x V u V u ˙ x = x ˙
33 29 31 32 3eqtr4d φ x V u V u ˙ 0 ˙ + ˙ x = u V u ˙ x
34 28 12 ersym φ x V 0 ˙ ˙ N + ˙ x
35 28 34 erthi φ x V 0 ˙ ˙ = N + ˙ x ˙
36 28 30 13 divsfval φ x V u V u ˙ 0 ˙ = 0 ˙ ˙
37 28 30 13 divsfval φ x V u V u ˙ N + ˙ x = N + ˙ x ˙
38 35 36 37 3eqtr4rd φ x V u V u ˙ N + ˙ x = u V u ˙ 0 ˙
39 18 2 3 19 21 5 7 27 9 33 11 38 imasgrp2 φ U Grp u V u ˙ 0 ˙ = 0 U
40 4 15 13 divsfval φ u V u ˙ 0 ˙ = 0 ˙ ˙
41 40 eqcomd φ 0 ˙ ˙ = u V u ˙ 0 ˙
42 41 eqeq1d φ 0 ˙ ˙ = 0 U u V u ˙ 0 ˙ = 0 U
43 42 anbi2d φ U Grp 0 ˙ ˙ = 0 U U Grp u V u ˙ 0 ˙ = 0 U
44 39 43 mpbird φ U Grp 0 ˙ ˙ = 0 U