Step | Hyp | Ref
| Expression |
1 | | fvexd 6203 |
. . . 4
|
2 | | fvexd 6203 |
. . . . 5
|
3 | | fvexd 6203 |
. . . . . 6
Scalar |
4 | | id 22 |
. . . . . . . . 9
Scalar
Scalar |
5 | | simpll 790 |
. . . . . . . . . . 11
|
6 | 5 | fveq2d 6195 |
. . . . . . . . . 10
Scalar Scalar |
7 | | isphl.f |
. . . . . . . . . 10
Scalar |
8 | 6, 7 | syl6eqr 2674 |
. . . . . . . . 9
Scalar |
9 | 4, 8 | sylan9eqr 2678 |
. . . . . . . 8
Scalar |
10 | 9 | eleq1d 2686 |
. . . . . . 7
Scalar
|
11 | | simpllr 799 |
. . . . . . . . 9
Scalar |
12 | | simplll 798 |
. . . . . . . . . . 11
Scalar |
13 | 12 | fveq2d 6195 |
. . . . . . . . . 10
Scalar |
14 | | isphl.v |
. . . . . . . . . 10
|
15 | 13, 14 | syl6eqr 2674 |
. . . . . . . . 9
Scalar |
16 | 11, 15 | eqtrd 2656 |
. . . . . . . 8
Scalar |
17 | | simplr 792 |
. . . . . . . . . . . . 13
Scalar |
18 | 12 | fveq2d 6195 |
. . . . . . . . . . . . . 14
Scalar |
19 | | isphl.h |
. . . . . . . . . . . . . 14
|
20 | 18, 19 | syl6eqr 2674 |
. . . . . . . . . . . . 13
Scalar |
21 | 17, 20 | eqtrd 2656 |
. . . . . . . . . . . 12
Scalar |
22 | 21 | oveqd 6667 |
. . . . . . . . . . 11
Scalar |
23 | 16, 22 | mpteq12dv 4733 |
. . . . . . . . . 10
Scalar |
24 | 9 | fveq2d 6195 |
. . . . . . . . . . 11
Scalar ringLMod ringLMod |
25 | 12, 24 | oveq12d 6668 |
. . . . . . . . . 10
Scalar LMHom ringLMod LMHom ringLMod |
26 | 23, 25 | eleq12d 2695 |
. . . . . . . . 9
Scalar LMHom ringLMod LMHom ringLMod |
27 | 21 | oveqd 6667 |
. . . . . . . . . . 11
Scalar |
28 | 9 | fveq2d 6195 |
. . . . . . . . . . . 12
Scalar |
29 | | isphl.z |
. . . . . . . . . . . 12
|
30 | 28, 29 | syl6eqr 2674 |
. . . . . . . . . . 11
Scalar |
31 | 27, 30 | eqeq12d 2637 |
. . . . . . . . . 10
Scalar
|
32 | 12 | fveq2d 6195 |
. . . . . . . . . . . 12
Scalar |
33 | | isphl.o |
. . . . . . . . . . . 12
|
34 | 32, 33 | syl6eqr 2674 |
. . . . . . . . . . 11
Scalar |
35 | 34 | eqeq2d 2632 |
. . . . . . . . . 10
Scalar
|
36 | 31, 35 | imbi12d 334 |
. . . . . . . . 9
Scalar
|
37 | 9 | fveq2d 6195 |
. . . . . . . . . . . . 13
Scalar |
38 | | isphl.i |
. . . . . . . . . . . . 13
|
39 | 37, 38 | syl6eqr 2674 |
. . . . . . . . . . . 12
Scalar |
40 | 21 | oveqd 6667 |
. . . . . . . . . . . 12
Scalar |
41 | 39, 40 | fveq12d 6197 |
. . . . . . . . . . 11
Scalar |
42 | 41, 22 | eqeq12d 2637 |
. . . . . . . . . 10
Scalar
|
43 | 16, 42 | raleqbidv 3152 |
. . . . . . . . 9
Scalar
|
44 | 26, 36, 43 | 3anbi123d 1399 |
. . . . . . . 8
Scalar LMHom ringLMod
LMHom ringLMod
|
45 | 16, 44 | raleqbidv 3152 |
. . . . . . 7
Scalar
LMHom ringLMod
LMHom ringLMod
|
46 | 10, 45 | anbi12d 747 |
. . . . . 6
Scalar LMHom ringLMod
LMHom ringLMod
|
47 | 3, 46 | sbcied 3472 |
. . . . 5
Scalar LMHom ringLMod
LMHom ringLMod
|
48 | 2, 47 | sbcied 3472 |
. . . 4
Scalar LMHom ringLMod
LMHom ringLMod
|
49 | 1, 48 | sbcied 3472 |
. . 3
Scalar
LMHom ringLMod
LMHom ringLMod
|
50 | | df-phl 19971 |
. . 3
Scalar LMHom ringLMod
|
51 | 49, 50 | elrab2 3366 |
. 2
LMHom ringLMod
|
52 | | 3anass 1042 |
. 2
LMHom ringLMod
LMHom ringLMod
|
53 | 51, 52 | bitr4i 267 |
1
LMHom ringLMod
|