Step |
Hyp |
Ref |
Expression |
1 |
|
baerlem3.v |
|
2 |
|
baerlem3.m |
|
3 |
|
baerlem3.o |
|
4 |
|
baerlem3.s |
|
5 |
|
baerlem3.n |
|
6 |
|
baerlem3.w |
|
7 |
|
baerlem3.x |
|
8 |
|
baerlem3.c |
|
9 |
|
baerlem3.d |
|
10 |
|
baerlem3.y |
|
11 |
|
baerlem3.z |
|
12 |
|
baerlem3.p |
|
13 |
|
baerlem3.t |
|
14 |
|
baerlem3.r |
|
15 |
|
baerlem3.b |
|
16 |
|
baerlem3.a |
|
17 |
|
baerlem3.l |
|
18 |
|
baerlem3.q |
|
19 |
|
baerlem3.i |
|
20 |
|
baerlem5a.a1 |
|
21 |
|
baerlem5a.b1 |
|
22 |
|
baerlem5a.d1 |
|
23 |
|
baerlem5a.e1 |
|
24 |
|
baerlem5a.j1 |
|
25 |
|
baerlem5a.j2 |
|
26 |
|
lveclmod |
|
27 |
6 26
|
syl |
|
28 |
10
|
eldifad |
|
29 |
1 13 14 15 2 27 20 7 28
|
lmodsubdi |
|
30 |
1 14 13 15
|
lmodvscl |
|
31 |
27 20 7 30
|
syl3anc |
|
32 |
1 12 2 13 14 15 19 27 20 31 28
|
lmodsubvs |
|
33 |
29 32
|
eqtrd |
|
34 |
33
|
oveq1d |
|
35 |
14
|
lmodring |
|
36 |
|
ringgrp |
|
37 |
27 35 36
|
3syl |
|
38 |
15 19
|
grpinvcl |
|
39 |
37 20 38
|
syl2anc |
|
40 |
1 14 13 15
|
lmodvscl |
|
41 |
27 39 28 40
|
syl3anc |
|
42 |
11
|
eldifad |
|
43 |
1 14 13 15
|
lmodvscl |
|
44 |
27 21 42 43
|
syl3anc |
|
45 |
1 12
|
lmodass |
|
46 |
27 31 41 44 45
|
syl13anc |
|
47 |
24 34 46
|
3eqtrd |
|
48 |
1 12
|
lmodvacl |
|
49 |
27 28 42 48
|
syl3anc |
|
50 |
1 14 13 15
|
lmodvscl |
|
51 |
27 20 49 50
|
syl3anc |
|
52 |
|
eqid |
|
53 |
1 12 52 2
|
grpsubval |
|
54 |
31 51 53
|
syl2anc |
|
55 |
1 13 14 15 2 27 20 7 49
|
lmodsubdi |
|
56 |
1 12 14 13 15
|
lmodvsdi |
|
57 |
27 39 28 42 56
|
syl13anc |
|
58 |
1 14 13 52 15 19 27 49 20
|
lmodvsneg |
|
59 |
15 19
|
grpinvcl |
|
60 |
37 22 59
|
syl2anc |
|
61 |
|
eqid |
|
62 |
1 61 5 27 28 42
|
lspprcl |
|
63 |
1 12 13 14 15 5 27 39 21 28 42
|
lsppreli |
|
64 |
1 12 13 14 15 5 27 23 60 28 42
|
lsppreli |
|
65 |
1 13 14 15 2 27 22 7 42
|
lmodsubdi |
|
66 |
1 14 13 15
|
lmodvscl |
|
67 |
27 22 7 66
|
syl3anc |
|
68 |
1 12 2 13 14 15 19 27 22 67 42
|
lmodsubvs |
|
69 |
65 68
|
eqtrd |
|
70 |
69
|
oveq1d |
|
71 |
|
lmodabl |
|
72 |
6 26 71
|
3syl |
|
73 |
1 14 13 15
|
lmodvscl |
|
74 |
27 60 42 73
|
syl3anc |
|
75 |
1 14 13 15
|
lmodvscl |
|
76 |
27 23 28 75
|
syl3anc |
|
77 |
1 12 72 67 74 76
|
abl32 |
|
78 |
1 12
|
lmodass |
|
79 |
27 67 76 74 78
|
syl13anc |
|
80 |
70 77 79
|
3eqtrd |
|
81 |
25 47 80
|
3eqtr3d |
|
82 |
1 12 14 15 13 61 6 62 7 8 63 64 20 22 81
|
lvecindp |
|
83 |
82
|
simprd |
|
84 |
1 12 14 15 13 3 5 6 10 11 39 21 23 60 9 83
|
lvecindp2 |
|
85 |
84
|
simprd |
|
86 |
82
|
simpld |
|
87 |
86
|
fveq2d |
|
88 |
85 87
|
eqtr4d |
|
89 |
88
|
oveq1d |
|
90 |
89
|
oveq2d |
|
91 |
57 58 90
|
3eqtr4rd |
|
92 |
91
|
oveq2d |
|
93 |
54 55 92
|
3eqtr4rd |
|
94 |
47 93
|
eqtrd |
|