Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ressnm Structured version   Unicode version

Theorem ressnm 26284
 Description: The norm in a restricted structure. (Contributed by Thierry Arnoux, 8-Oct-2017.)
Hypotheses
Ref Expression
ressnm.1 s
ressnm.2
ressnm.3
ressnm.4
Assertion
Ref Expression
ressnm

Proof of Theorem ressnm
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ressnm.1 . . . . 5 s
2 ressnm.2 . . . . 5
31, 2ressbas2 14352 . . . 4
5 fvex 5812 . . . . . . . 8
62, 5eqeltri 2538 . . . . . . 7
76ssex 4547 . . . . . 6
8 eqid 2454 . . . . . . 7
91, 8ressds 14475 . . . . . 6
107, 9syl 16 . . . . 5
11103ad2ant3 1011 . . . 4
12 eqidd 2455 . . . 4
13 ressnm.3 . . . . 5
141, 2, 13ress0g 15573 . . . 4
1511, 12, 14oveq123d 6224 . . 3
164, 15mpteq12dv 4481 . 2
17 ressnm.4 . . . . . 6
1817, 2, 13, 8nmfval 20323 . . . . 5
1918reseq1i 5217 . . . 4
20 resmpt 5267 . . . 4
2119, 20syl5eq 2507 . . 3