Metamath Proof Explorer

Theorem subgnm

Description: The norm in a subgroup. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses subgngp.h 
|- H = ( G |`s A )
subgnm.n 
|- N = ( norm ` G )
subgnm.m 
|- M = ( norm ` H )
Assertion subgnm 
|- ( A e. ( SubGrp ` G ) -> M = ( N |` A ) )

Proof

Step Hyp Ref Expression
1 subgngp.h 
 |-  H = ( G |`s A )
2 subgnm.n 
 |-  N = ( norm ` G )
3 subgnm.m 
 |-  M = ( norm ` H )
4 eqid 
 |-  ( Base ` G ) = ( Base ` G )
5 4 subgss 
 |-  ( A e. ( SubGrp ` G ) -> A C_ ( Base ` G ) )
6 5 resmptd 
 |-  ( A e. ( SubGrp ` G ) -> ( ( x e. ( Base ` G ) |-> ( x ( dist ` G ) ( 0g ` G ) ) ) |` A ) = ( x e. A |-> ( x ( dist ` G ) ( 0g ` G ) ) ) )
7 1 subgbas 
 |-  ( A e. ( SubGrp ` G ) -> A = ( Base ` H ) )
8 eqid 
 |-  ( dist ` G ) = ( dist ` G )
9 1 8 ressds 
 |-  ( A e. ( SubGrp ` G ) -> ( dist ` G ) = ( dist ` H ) )
10 eqidd 
 |-  ( A e. ( SubGrp ` G ) -> x = x )
11 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
12 1 11 subg0 
 |-  ( A e. ( SubGrp ` G ) -> ( 0g ` G ) = ( 0g ` H ) )
13 9 10 12 oveq123d 
 |-  ( A e. ( SubGrp ` G ) -> ( x ( dist ` G ) ( 0g ` G ) ) = ( x ( dist ` H ) ( 0g ` H ) ) )
14 7 13 mpteq12dv 
 |-  ( A e. ( SubGrp ` G ) -> ( x e. A |-> ( x ( dist ` G ) ( 0g ` G ) ) ) = ( x e. ( Base ` H ) |-> ( x ( dist ` H ) ( 0g ` H ) ) ) )
15 6 14 eqtr2d 
 |-  ( A e. ( SubGrp ` G ) -> ( x e. ( Base ` H ) |-> ( x ( dist ` H ) ( 0g ` H ) ) ) = ( ( x e. ( Base ` G ) |-> ( x ( dist ` G ) ( 0g ` G ) ) ) |` A ) )
16 eqid 
 |-  ( Base ` H ) = ( Base ` H )
17 eqid 
 |-  ( 0g ` H ) = ( 0g ` H )
18 eqid 
 |-  ( dist ` H ) = ( dist ` H )
19 3 16 17 18 nmfval 
 |-  M = ( x e. ( Base ` H ) |-> ( x ( dist ` H ) ( 0g ` H ) ) )
20 2 4 11 8 nmfval 
 |-  N = ( x e. ( Base ` G ) |-> ( x ( dist ` G ) ( 0g ` G ) ) )
21 20 reseq1i 
 |-  ( N |` A ) = ( ( x e. ( Base ` G ) |-> ( x ( dist ` G ) ( 0g ` G ) ) ) |` A )
22 15 19 21 3eqtr4g 
 |-  ( A e. ( SubGrp ` G ) -> M = ( N |` A ) )