Step |
Hyp |
Ref |
Expression |
1 |
|
lindfmm.b |
|
2 |
|
lindfmm.c |
|
3 |
|
rellindf |
|
4 |
3
|
brrelex1i |
|
5 |
|
simp3 |
|
6 |
|
dmfex |
|
7 |
4 5 6
|
syl2anr |
|
8 |
7
|
ex |
|
9 |
3
|
brrelex1i |
|
10 |
|
f1f |
|
11 |
|
fco |
|
12 |
10 11
|
sylan |
|
13 |
12
|
3adant1 |
|
14 |
|
dmfex |
|
15 |
9 13 14
|
syl2anr |
|
16 |
15
|
ex |
|
17 |
|
eldifi |
|
18 |
|
simpllr |
|
19 |
|
lmhmlmod1 |
|
20 |
19
|
ad3antrrr |
|
21 |
|
simprr |
|
22 |
|
simprl |
|
23 |
|
simpl |
|
24 |
|
ffvelrn |
|
25 |
22 23 24
|
syl2an |
|
26 |
|
eqid |
|
27 |
|
eqid |
|
28 |
|
eqid |
|
29 |
1 26 27 28
|
lmodvscl |
|
30 |
20 21 25 29
|
syl3anc |
|
31 |
|
imassrn |
|
32 |
|
frn |
|
33 |
32
|
adantr |
|
34 |
31 33
|
sstrid |
|
35 |
34
|
ad2antlr |
|
36 |
|
eqid |
|
37 |
1 36
|
lspssv |
|
38 |
20 35 37
|
syl2anc |
|
39 |
|
f1elima |
|
40 |
18 30 38 39
|
syl3anc |
|
41 |
|
simplll |
|
42 |
|
eqid |
|
43 |
26 28 1 27 42
|
lmhmlin |
|
44 |
41 21 25 43
|
syl3anc |
|
45 |
|
ffn |
|
46 |
45
|
ad2antrl |
|
47 |
|
fvco2 |
|
48 |
46 23 47
|
syl2an |
|
49 |
48
|
oveq2d |
|
50 |
44 49
|
eqtr4d |
|
51 |
|
eqid |
|
52 |
1 36 51
|
lmhmlsp |
|
53 |
41 35 52
|
syl2anc |
|
54 |
|
imaco |
|
55 |
54
|
fveq2i |
|
56 |
53 55
|
eqtr4di |
|
57 |
50 56
|
eleq12d |
|
58 |
40 57
|
bitr3d |
|
59 |
58
|
notbid |
|
60 |
59
|
anassrs |
|
61 |
17 60
|
sylan2 |
|
62 |
61
|
ralbidva |
|
63 |
|
eqid |
|
64 |
26 63
|
lmhmsca |
|
65 |
64
|
fveq2d |
|
66 |
64
|
fveq2d |
|
67 |
66
|
sneqd |
|
68 |
65 67
|
difeq12d |
|
69 |
68
|
ad3antrrr |
|
70 |
69
|
raleqdv |
|
71 |
62 70
|
bitr4d |
|
72 |
71
|
ralbidva |
|
73 |
19
|
ad2antrr |
|
74 |
|
simprr |
|
75 |
|
eqid |
|
76 |
1 27 36 26 28 75
|
islindf2 |
|
77 |
73 74 22 76
|
syl3anc |
|
78 |
|
lmhmlmod2 |
|
79 |
78
|
ad2antrr |
|
80 |
12
|
ad2ant2lr |
|
81 |
|
eqid |
|
82 |
|
eqid |
|
83 |
2 42 51 63 81 82
|
islindf2 |
|
84 |
79 74 80 83
|
syl3anc |
|
85 |
72 77 84
|
3bitr4d |
|
86 |
85
|
exp32 |
|
87 |
86
|
3impia |
|
88 |
8 16 87
|
pm5.21ndd |
|