Step | Hyp | Ref
| Expression |
1 | | cnlm 24089 |
. 2
class
NrmMod |
2 | | vf |
. . . . . . 7
setvar π |
3 | 2 | cv 1541 |
. . . . . 6
class π |
4 | | cnrg 24088 |
. . . . . 6
class
NrmRing |
5 | 3, 4 | wcel 2107 |
. . . . 5
wff π β NrmRing |
6 | | vx |
. . . . . . . . . . 11
setvar π₯ |
7 | 6 | cv 1541 |
. . . . . . . . . 10
class π₯ |
8 | | vy |
. . . . . . . . . . 11
setvar π¦ |
9 | 8 | cv 1541 |
. . . . . . . . . 10
class π¦ |
10 | | vw |
. . . . . . . . . . . 12
setvar π€ |
11 | 10 | cv 1541 |
. . . . . . . . . . 11
class π€ |
12 | | cvsca 17201 |
. . . . . . . . . . 11
class
Β·π |
13 | 11, 12 | cfv 6544 |
. . . . . . . . . 10
class (
Β·π βπ€) |
14 | 7, 9, 13 | co 7409 |
. . . . . . . . 9
class (π₯(
Β·π βπ€)π¦) |
15 | | cnm 24085 |
. . . . . . . . . 10
class
norm |
16 | 11, 15 | cfv 6544 |
. . . . . . . . 9
class
(normβπ€) |
17 | 14, 16 | cfv 6544 |
. . . . . . . 8
class
((normβπ€)β(π₯( Β·π
βπ€)π¦)) |
18 | 3, 15 | cfv 6544 |
. . . . . . . . . 10
class
(normβπ) |
19 | 7, 18 | cfv 6544 |
. . . . . . . . 9
class
((normβπ)βπ₯) |
20 | 9, 16 | cfv 6544 |
. . . . . . . . 9
class
((normβπ€)βπ¦) |
21 | | cmul 11115 |
. . . . . . . . 9
class
Β· |
22 | 19, 20, 21 | co 7409 |
. . . . . . . 8
class
(((normβπ)βπ₯) Β· ((normβπ€)βπ¦)) |
23 | 17, 22 | wceq 1542 |
. . . . . . 7
wff
((normβπ€)β(π₯( Β·π
βπ€)π¦)) = (((normβπ)βπ₯) Β· ((normβπ€)βπ¦)) |
24 | | cbs 17144 |
. . . . . . . 8
class
Base |
25 | 11, 24 | cfv 6544 |
. . . . . . 7
class
(Baseβπ€) |
26 | 23, 8, 25 | wral 3062 |
. . . . . 6
wff
βπ¦ β
(Baseβπ€)((normβπ€)β(π₯( Β·π
βπ€)π¦)) = (((normβπ)βπ₯) Β· ((normβπ€)βπ¦)) |
27 | 3, 24 | cfv 6544 |
. . . . . 6
class
(Baseβπ) |
28 | 26, 6, 27 | wral 3062 |
. . . . 5
wff
βπ₯ β
(Baseβπ)βπ¦ β (Baseβπ€)((normβπ€)β(π₯( Β·π
βπ€)π¦)) = (((normβπ)βπ₯) Β· ((normβπ€)βπ¦)) |
29 | 5, 28 | wa 397 |
. . . 4
wff (π β NrmRing β§
βπ₯ β
(Baseβπ)βπ¦ β (Baseβπ€)((normβπ€)β(π₯( Β·π
βπ€)π¦)) = (((normβπ)βπ₯) Β· ((normβπ€)βπ¦))) |
30 | | csca 17200 |
. . . . 5
class
Scalar |
31 | 11, 30 | cfv 6544 |
. . . 4
class
(Scalarβπ€) |
32 | 29, 2, 31 | wsbc 3778 |
. . 3
wff
[(Scalarβπ€) / π](π β NrmRing β§ βπ₯ β (Baseβπ)βπ¦ β (Baseβπ€)((normβπ€)β(π₯( Β·π
βπ€)π¦)) = (((normβπ)βπ₯) Β· ((normβπ€)βπ¦))) |
33 | | cngp 24086 |
. . . 4
class
NrmGrp |
34 | | clmod 20471 |
. . . 4
class
LMod |
35 | 33, 34 | cin 3948 |
. . 3
class (NrmGrp
β© LMod) |
36 | 32, 10, 35 | crab 3433 |
. 2
class {π€ β (NrmGrp β© LMod)
β£ [(Scalarβπ€) / π](π β NrmRing β§ βπ₯ β (Baseβπ)βπ¦ β (Baseβπ€)((normβπ€)β(π₯( Β·π
βπ€)π¦)) = (((normβπ)βπ₯) Β· ((normβπ€)βπ¦)))} |
37 | 1, 36 | wceq 1542 |
1
wff NrmMod =
{π€ β (NrmGrp β©
LMod) β£ [(Scalarβπ€) / π](π β NrmRing β§ βπ₯ β (Baseβπ)βπ¦ β (Baseβπ€)((normβπ€)β(π₯( Β·π
βπ€)π¦)) = (((normβπ)βπ₯) Β· ((normβπ€)βπ¦)))} |