Metamath Proof Explorer

Theorem ressnm

Description: The norm in a restricted structure. (Contributed by Thierry Arnoux, 8-Oct-2017)

Ref Expression
Hypotheses ressnm.1 
|- H = ( G |`s A )
ressnm.2 
|- B = ( Base ` G )
ressnm.3 
|- .0. = ( 0g ` G )
ressnm.4 
|- N = ( norm ` G )
Assertion ressnm 
|- ( ( G e. Mnd /\ .0. e. A /\ A C_ B ) -> ( N |` A ) = ( norm ` H ) )

Proof

Step Hyp Ref Expression
1 ressnm.1 
 |-  H = ( G |`s A )
2 ressnm.2 
 |-  B = ( Base ` G )
3 ressnm.3 
 |-  .0. = ( 0g ` G )
4 ressnm.4 
 |-  N = ( norm ` G )
5 1 2 ressbas2 
 |-  ( A C_ B -> A = ( Base ` H ) )
6 5 3ad2ant3 
 |-  ( ( G e. Mnd /\ .0. e. A /\ A C_ B ) -> A = ( Base ` H ) )
7 2 fvexi 
 |-  B e. _V
8 7 ssex 
 |-  ( A C_ B -> A e. _V )
9 eqid 
 |-  ( dist ` G ) = ( dist ` G )
10 1 9 ressds 
 |-  ( A e. _V -> ( dist ` G ) = ( dist ` H ) )
11 8 10 syl 
 |-  ( A C_ B -> ( dist ` G ) = ( dist ` H ) )
12 11 3ad2ant3 
 |-  ( ( G e. Mnd /\ .0. e. A /\ A C_ B ) -> ( dist ` G ) = ( dist ` H ) )
13 eqidd 
 |-  ( ( G e. Mnd /\ .0. e. A /\ A C_ B ) -> x = x )
14 1 2 3 ress0g 
 |-  ( ( G e. Mnd /\ .0. e. A /\ A C_ B ) -> .0. = ( 0g ` H ) )
15 12 13 14 oveq123d 
 |-  ( ( G e. Mnd /\ .0. e. A /\ A C_ B ) -> ( x ( dist ` G ) .0. ) = ( x ( dist ` H ) ( 0g ` H ) ) )
16 6 15 mpteq12dv 
 |-  ( ( G e. Mnd /\ .0. e. A /\ A C_ B ) -> ( x e. A |-> ( x ( dist ` G ) .0. ) ) = ( x e. ( Base ` H ) |-> ( x ( dist ` H ) ( 0g ` H ) ) ) )
17 4 2 3 9 nmfval 
 |-  N = ( x e. B |-> ( x ( dist ` G ) .0. ) )
18 17 reseq1i 
 |-  ( N |` A ) = ( ( x e. B |-> ( x ( dist ` G ) .0. ) ) |` A )
19 resmpt 
 |-  ( A C_ B -> ( ( x e. B |-> ( x ( dist ` G ) .0. ) ) |` A ) = ( x e. A |-> ( x ( dist ` G ) .0. ) ) )
20 18 19 syl5eq 
 |-  ( A C_ B -> ( N |` A ) = ( x e. A |-> ( x ( dist ` G ) .0. ) ) )
21 20 3ad2ant3 
 |-  ( ( G e. Mnd /\ .0. e. A /\ A C_ B ) -> ( N |` A ) = ( x e. A |-> ( x ( dist ` G ) .0. ) ) )
22 eqid 
 |-  ( norm ` H ) = ( norm ` H )
23 eqid 
 |-  ( Base ` H ) = ( Base ` H )
24 eqid 
 |-  ( 0g ` H ) = ( 0g ` H )
25 eqid 
 |-  ( dist ` H ) = ( dist ` H )
26 22 23 24 25 nmfval 
 |-  ( norm ` H ) = ( x e. ( Base ` H ) |-> ( x ( dist ` H ) ( 0g ` H ) ) )
27 26 a1i 
 |-  ( ( G e. Mnd /\ .0. e. A /\ A C_ B ) -> ( norm ` H ) = ( x e. ( Base ` H ) |-> ( x ( dist ` H ) ( 0g ` H ) ) ) )
28 16 21 27 3eqtr4d 
 |-  ( ( G e. Mnd /\ .0. e. A /\ A C_ B ) -> ( N |` A ) = ( norm ` H ) )