Step | Hyp | Ref
| Expression |
1 | | anass 681 |
. 2
NrmGrp NrmRing
NrmGrp
NrmRing
|
2 | | df-3an 1039 |
. . . 4
NrmGrp
NrmRing NrmGrp NrmRing |
3 | | elin 3796 |
. . . . 5
NrmGrp NrmGrp |
4 | 3 | anbi1i 731 |
. . . 4
NrmGrp NrmRing NrmGrp
NrmRing |
5 | 2, 4 | bitr4i 267 |
. . 3
NrmGrp
NrmRing NrmGrp NrmRing |
6 | 5 | anbi1i 731 |
. 2
NrmGrp
NrmRing
NrmGrp
NrmRing
|
7 | | fvexd 6203 |
. . . 4
Scalar |
8 | | id 22 |
. . . . . . 7
Scalar
Scalar |
9 | | fveq2 6191 |
. . . . . . . 8
Scalar Scalar |
10 | | isnlm.f |
. . . . . . . 8
Scalar |
11 | 9, 10 | syl6eqr 2674 |
. . . . . . 7
Scalar |
12 | 8, 11 | sylan9eqr 2678 |
. . . . . 6
Scalar |
13 | 12 | eleq1d 2686 |
. . . . 5
Scalar
NrmRing
NrmRing |
14 | 12 | fveq2d 6195 |
. . . . . . 7
Scalar |
15 | | isnlm.k |
. . . . . . 7
|
16 | 14, 15 | syl6eqr 2674 |
. . . . . 6
Scalar |
17 | | simpl 473 |
. . . . . . . . 9
Scalar |
18 | 17 | fveq2d 6195 |
. . . . . . . 8
Scalar |
19 | | isnlm.v |
. . . . . . . 8
|
20 | 18, 19 | syl6eqr 2674 |
. . . . . . 7
Scalar |
21 | 17 | fveq2d 6195 |
. . . . . . . . . 10
Scalar |
22 | | isnlm.n |
. . . . . . . . . 10
|
23 | 21, 22 | syl6eqr 2674 |
. . . . . . . . 9
Scalar |
24 | 17 | fveq2d 6195 |
. . . . . . . . . . 11
Scalar |
25 | | isnlm.s |
. . . . . . . . . . 11
|
26 | 24, 25 | syl6eqr 2674 |
. . . . . . . . . 10
Scalar |
27 | 26 | oveqd 6667 |
. . . . . . . . 9
Scalar |
28 | 23, 27 | fveq12d 6197 |
. . . . . . . 8
Scalar |
29 | 12 | fveq2d 6195 |
. . . . . . . . . . 11
Scalar |
30 | | isnlm.a |
. . . . . . . . . . 11
|
31 | 29, 30 | syl6eqr 2674 |
. . . . . . . . . 10
Scalar |
32 | 31 | fveq1d 6193 |
. . . . . . . . 9
Scalar |
33 | 23 | fveq1d 6193 |
. . . . . . . . 9
Scalar |
34 | 32, 33 | oveq12d 6668 |
. . . . . . . 8
Scalar |
35 | 28, 34 | eqeq12d 2637 |
. . . . . . 7
Scalar
|
36 | 20, 35 | raleqbidv 3152 |
. . . . . 6
Scalar
|
37 | 16, 36 | raleqbidv 3152 |
. . . . 5
Scalar
|
38 | 13, 37 | anbi12d 747 |
. . . 4
Scalar NrmRing
NrmRing
|
39 | 7, 38 | sbcied 3472 |
. . 3
Scalar
NrmRing
NrmRing
|
40 | | df-nlm 22391 |
. . 3
NrmMod NrmGrp Scalar NrmRing
|
41 | 39, 40 | elrab2 3366 |
. 2
NrmMod NrmGrp
NrmRing
|
42 | 1, 6, 41 | 3bitr4ri 293 |
1
NrmMod NrmGrp
NrmRing
|