Metamath Proof Explorer

Theorem qusadd

Description: Value of the group operation in a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015)

Ref Expression
Hypotheses qusgrp.h 
|- H = ( G /s ( G ~QG S ) )
qusadd.v 
|- V = ( Base ` G )
qusadd.p 
|- .+ = ( +g ` G )
qusadd.a 
|- .+b = ( +g ` H )
Assertion qusadd 
|- ( ( S e. ( NrmSGrp ` G ) /\ X e. V /\ Y e. V ) -> ( [ X ] ( G ~QG S ) .+b [ Y ] ( G ~QG S ) ) = [ ( X .+ Y ) ] ( G ~QG S ) )

Proof

Step Hyp Ref Expression
1 qusgrp.h 
 |-  H = ( G /s ( G ~QG S ) )
2 qusadd.v 
 |-  V = ( Base ` G )
3 qusadd.p 
 |-  .+ = ( +g ` G )
4 qusadd.a 
 |-  .+b = ( +g ` H )
5 1 a1i 
 |-  ( S e. ( NrmSGrp ` G ) -> H = ( G /s ( G ~QG S ) ) )
6 2 a1i 
 |-  ( S e. ( NrmSGrp ` G ) -> V = ( Base ` G ) )
7 nsgsubg 
 |-  ( S e. ( NrmSGrp ` G ) -> S e. ( SubGrp ` G ) )
8 eqid 
 |-  ( G ~QG S ) = ( G ~QG S )
9 2 8 eqger 
 |-  ( S e. ( SubGrp ` G ) -> ( G ~QG S ) Er V )
10 7 9 syl 
 |-  ( S e. ( NrmSGrp ` G ) -> ( G ~QG S ) Er V )
11 subgrcl 
 |-  ( S e. ( SubGrp ` G ) -> G e. Grp )
12 7 11 syl 
 |-  ( S e. ( NrmSGrp ` G ) -> G e. Grp )
13 2 8 3 eqgcpbl 
 |-  ( S e. ( NrmSGrp ` G ) -> ( ( a ( G ~QG S ) p /\ b ( G ~QG S ) q ) -> ( a .+ b ) ( G ~QG S ) ( p .+ q ) ) )
14 2 3 grpcl 
 |-  ( ( G e. Grp /\ p e. V /\ q e. V ) -> ( p .+ q ) e. V )
15 14 3expb 
 |-  ( ( G e. Grp /\ ( p e. V /\ q e. V ) ) -> ( p .+ q ) e. V )
16 12 15 sylan 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ ( p e. V /\ q e. V ) ) -> ( p .+ q ) e. V )
17 5 6 10 12 13 16 3 4 qusaddval 
 |-  ( ( S e. ( NrmSGrp ` G ) /\ X e. V /\ Y e. V ) -> ( [ X ] ( G ~QG S ) .+b [ Y ] ( G ~QG S ) ) = [ ( X .+ Y ) ] ( G ~QG S ) )