Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . . . . 6
|
2 | | islmod.v |
. . . . . 6
|
3 | 1, 2 | syl6eqr 2674 |
. . . . 5
|
4 | | fveq2 6191 |
. . . . . . 7
|
5 | | islmod.a |
. . . . . . 7
|
6 | 4, 5 | syl6eqr 2674 |
. . . . . 6
|
7 | | fveq2 6191 |
. . . . . . . 8
Scalar Scalar |
8 | | islmod.f |
. . . . . . . 8
Scalar |
9 | 7, 8 | syl6eqr 2674 |
. . . . . . 7
Scalar |
10 | | fveq2 6191 |
. . . . . . . . 9
|
11 | | islmod.s |
. . . . . . . . 9
|
12 | 10, 11 | syl6eqr 2674 |
. . . . . . . 8
|
13 | 12 | sbceq1d 3440 |
. . . . . . 7
|
14 | 9, 13 | sbceqbid 3442 |
. . . . . 6
Scalar
|
15 | 6, 14 | sbceqbid 3442 |
. . . . 5
Scalar
|
16 | 3, 15 | sbceqbid 3442 |
. . . 4
Scalar
|
17 | | fvex 6201 |
. . . . . . 7
|
18 | 2, 17 | eqeltri 2697 |
. . . . . 6
|
19 | | fvex 6201 |
. . . . . . 7
|
20 | 5, 19 | eqeltri 2697 |
. . . . . 6
|
21 | | fvex 6201 |
. . . . . . 7
Scalar |
22 | 8, 21 | eqeltri 2697 |
. . . . . 6
|
23 | | simp3 1063 |
. . . . . . . . . 10
|
24 | 23 | fveq2d 6195 |
. . . . . . . . 9
|
25 | | islmod.k |
. . . . . . . . 9
|
26 | 24, 25 | syl6eqr 2674 |
. . . . . . . 8
|
27 | 23 | fveq2d 6195 |
. . . . . . . . . 10
|
28 | | islmod.p |
. . . . . . . . . 10
|
29 | 27, 28 | syl6eqr 2674 |
. . . . . . . . 9
|
30 | 23 | fveq2d 6195 |
. . . . . . . . . . . 12
|
31 | | islmod.t |
. . . . . . . . . . . 12
|
32 | 30, 31 | syl6eqr 2674 |
. . . . . . . . . . 11
|
33 | 32 | sbceq1d 3440 |
. . . . . . . . . 10
|
34 | | fvex 6201 |
. . . . . . . . . . . . 13
|
35 | 31, 34 | eqeltri 2697 |
. . . . . . . . . . . 12
|
36 | | oveq 6656 |
. . . . . . . . . . . . . . . . . . 19
|
37 | 36 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . 18
|
38 | 37 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . 17
|
39 | 38 | anbi1d 741 |
. . . . . . . . . . . . . . . 16
|
40 | 39 | anbi2d 740 |
. . . . . . . . . . . . . . 15
|
41 | 40 | 2ralbidv 2989 |
. . . . . . . . . . . . . 14
|
42 | 41 | 2ralbidv 2989 |
. . . . . . . . . . . . 13
|
43 | 42 | anbi2d 740 |
. . . . . . . . . . . 12
|
44 | 35, 43 | sbcie 3470 |
. . . . . . . . . . 11
|
45 | 23 | eleq1d 2686 |
. . . . . . . . . . . 12
|
46 | | simp1 1061 |
. . . . . . . . . . . . . 14
|
47 | 46 | eleq2d 2687 |
. . . . . . . . . . . . . . . . 17
|
48 | | simp2 1062 |
. . . . . . . . . . . . . . . . . . . 20
|
49 | 48 | oveqd 6667 |
. . . . . . . . . . . . . . . . . . 19
|
50 | 49 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
|
51 | 48 | oveqd 6667 |
. . . . . . . . . . . . . . . . . 18
|
52 | 50, 51 | eqeq12d 2637 |
. . . . . . . . . . . . . . . . 17
|
53 | 48 | oveqd 6667 |
. . . . . . . . . . . . . . . . . 18
|
54 | 53 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . 17
|
55 | 47, 52, 54 | 3anbi123d 1399 |
. . . . . . . . . . . . . . . 16
|
56 | 23 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . 20
|
57 | | islmod.u |
. . . . . . . . . . . . . . . . . . . 20
|
58 | 56, 57 | syl6eqr 2674 |
. . . . . . . . . . . . . . . . . . 19
|
59 | 58 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . 18
|
60 | 59 | eqeq1d 2624 |
. . . . . . . . . . . . . . . . 17
|
61 | 60 | anbi2d 740 |
. . . . . . . . . . . . . . . 16
|
62 | 55, 61 | anbi12d 747 |
. . . . . . . . . . . . . . 15
|
63 | 46, 62 | raleqbidv 3152 |
. . . . . . . . . . . . . 14
|
64 | 46, 63 | raleqbidv 3152 |
. . . . . . . . . . . . 13
|
65 | 64 | 2ralbidv 2989 |
. . . . . . . . . . . 12
|
66 | 45, 65 | anbi12d 747 |
. . . . . . . . . . 11
|
67 | 44, 66 | syl5bb 272 |
. . . . . . . . . 10
|
68 | 33, 67 | bitrd 268 |
. . . . . . . . 9
|
69 | 29, 68 | sbceqbid 3442 |
. . . . . . . 8
|
70 | 26, 69 | sbceqbid 3442 |
. . . . . . 7
|
71 | 70 | sbcbidv 3490 |
. . . . . 6
|
72 | 18, 20, 22, 71 | sbc3ie 3507 |
. . . . 5
|
73 | | fvex 6201 |
. . . . . . 7
|
74 | 11, 73 | eqeltri 2697 |
. . . . . 6
|
75 | | fvex 6201 |
. . . . . . 7
|
76 | 25, 75 | eqeltri 2697 |
. . . . . 6
|
77 | | fvex 6201 |
. . . . . . 7
|
78 | 28, 77 | eqeltri 2697 |
. . . . . 6
|
79 | | simp2 1062 |
. . . . . . . 8
|
80 | | simp1 1061 |
. . . . . . . . . . . . . 14
|
81 | 80 | oveqd 6667 |
. . . . . . . . . . . . 13
|
82 | 81 | eleq1d 2686 |
. . . . . . . . . . . 12
|
83 | 80 | oveqd 6667 |
. . . . . . . . . . . . 13
|
84 | 80 | oveqd 6667 |
. . . . . . . . . . . . . 14
|
85 | 81, 84 | oveq12d 6668 |
. . . . . . . . . . . . 13
|
86 | 83, 85 | eqeq12d 2637 |
. . . . . . . . . . . 12
|
87 | | simp3 1063 |
. . . . . . . . . . . . . . . 16
|
88 | 87 | oveqd 6667 |
. . . . . . . . . . . . . . 15
|
89 | 88 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
90 | 80 | oveqd 6667 |
. . . . . . . . . . . . . 14
|
91 | 89, 90 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
92 | 80 | oveqd 6667 |
. . . . . . . . . . . . . 14
|
93 | 92, 81 | oveq12d 6668 |
. . . . . . . . . . . . 13
|
94 | 91, 93 | eqeq12d 2637 |
. . . . . . . . . . . 12
|
95 | 82, 86, 94 | 3anbi123d 1399 |
. . . . . . . . . . 11
|
96 | 80 | oveqd 6667 |
. . . . . . . . . . . . 13
|
97 | 81 | oveq2d 6666 |
. . . . . . . . . . . . . 14
|
98 | 80 | oveqd 6667 |
. . . . . . . . . . . . . 14
|
99 | 97, 98 | eqtrd 2656 |
. . . . . . . . . . . . 13
|
100 | 96, 99 | eqeq12d 2637 |
. . . . . . . . . . . 12
|
101 | 80 | oveqd 6667 |
. . . . . . . . . . . . 13
|
102 | 101 | eqeq1d 2624 |
. . . . . . . . . . . 12
|
103 | 100, 102 | anbi12d 747 |
. . . . . . . . . . 11
|
104 | 95, 103 | anbi12d 747 |
. . . . . . . . . 10
|
105 | 104 | 2ralbidv 2989 |
. . . . . . . . 9
|
106 | 79, 105 | raleqbidv 3152 |
. . . . . . . 8
|
107 | 79, 106 | raleqbidv 3152 |
. . . . . . 7
|
108 | 107 | anbi2d 740 |
. . . . . 6
|
109 | 74, 76, 78, 108 | sbc3ie 3507 |
. . . . 5
|
110 | 72, 109 | bitri 264 |
. . . 4
|
111 | 16, 110 | syl6bb 276 |
. . 3
Scalar
|
112 | | df-lmod 18865 |
. . 3
Scalar |
113 | 111, 112 | elrab2 3366 |
. 2
|
114 | | 3anass 1042 |
. 2
|
115 | 113, 114 | bitr4i 267 |
1
|