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 
|- ( ph -> U = ( R /s .~ ) )
qusgrp2.v 
|- ( ph -> V = ( Base ` R ) )
qusgrp2.p 
|- ( ph -> .+ = ( +g ` R ) )
qusgrp2.r 
|- ( ph -> .~ Er V )
qusgrp2.x 
|- ( ph -> R e. X )
qusgrp2.e 
|- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .+ b ) .~ ( p .+ q ) ) )
qusgrp2.1 
|- ( ( ph /\ x e. V /\ y e. V ) -> ( x .+ y ) e. V )
qusgrp2.2 
|- ( ( ph /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( x .+ y ) .+ z ) .~ ( x .+ ( y .+ z ) ) )
qusgrp2.3 
|- ( ph -> .0. e. V )
qusgrp2.4 
|- ( ( ph /\ x e. V ) -> ( .0. .+ x ) .~ x )
qusgrp2.5 
|- ( ( ph /\ x e. V ) -> N e. V )
qusgrp2.6 
|- ( ( ph /\ x e. V ) -> ( N .+ x ) .~ .0. )
Assertion qusgrp2 
|- ( ph -> ( U e. Grp /\ [ .0. ] .~ = ( 0g ` U ) ) )

Proof

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