Description: Lemma for baerlem5b . (Contributed by NM, 13-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | baerlem3.v | |
|
baerlem3.m | |
||
baerlem3.o | |
||
baerlem3.s | |
||
baerlem3.n | |
||
baerlem3.w | |
||
baerlem3.x | |
||
baerlem3.c | |
||
baerlem3.d | |
||
baerlem3.y | |
||
baerlem3.z | |
||
baerlem3.p | |
||
baerlem3.t | |
||
baerlem3.r | |
||
baerlem3.b | |
||
baerlem3.a | |
||
baerlem3.l | |
||
baerlem3.q | |
||
baerlem3.i | |
||
Assertion | baerlem5blem2 | |
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 | lveclmod | |
|
21 | 6 20 | syl | |
22 | 10 | eldifad | |
23 | 11 | eldifad | |
24 | 1 12 5 4 | lspsntri | |
25 | 21 22 23 24 | syl3anc | |
26 | 1 12 | lmodvacl | |
27 | 21 22 23 26 | syl3anc | |
28 | 1 2 | lmodvsubcl | |
29 | 21 7 27 28 | syl3anc | |
30 | 1 2 5 21 29 7 | lspsnsub | |
31 | lmodabl | |
|
32 | 21 31 | syl | |
33 | 1 2 32 7 27 | ablnncan | |
34 | 33 | sneqd | |
35 | 34 | fveq2d | |
36 | 30 35 | eqtrd | |
37 | 1 2 4 5 | lspsntrim | |
38 | 21 29 7 37 | syl3anc | |
39 | 36 38 | eqsstrrd | |
40 | 25 39 | ssind | |
41 | elin | |
|
42 | 1 12 14 15 13 4 5 21 22 23 | lsmspsn | |
43 | 1 12 14 15 13 4 5 21 29 7 | lsmspsn | |
44 | 42 43 | anbi12d | |
45 | 41 44 | syl5bb | |
46 | simp11 | |
|
47 | 46 6 | syl | |
48 | 46 7 | syl | |
49 | 46 8 | syl | |
50 | 46 9 | syl | |
51 | 46 10 | syl | |
52 | 46 11 | syl | |
53 | simp12l | |
|
54 | simp12r | |
|
55 | simp2l | |
|
56 | simp2r | |
|
57 | simp13 | |
|
58 | simp3 | |
|
59 | 1 2 3 4 5 47 48 49 50 51 52 12 13 14 15 16 17 18 19 53 54 55 56 57 58 | baerlem5blem1 | |
60 | 46 21 | syl | |
61 | 14 | lmodring | |
62 | ringgrp | |
|
63 | 46 21 61 62 | 4syl | |
64 | 15 19 | grpinvcl | |
65 | 63 55 64 | syl2anc | |
66 | 46 27 | syl | |
67 | 1 13 14 15 5 60 65 66 | lspsneli | |
68 | 59 67 | eqeltrd | |
69 | 68 | 3exp | |
70 | 69 | rexlimdvv | |
71 | 70 | 3exp | |
72 | 71 | rexlimdvv | |
73 | 72 | impd | |
74 | 45 73 | sylbid | |
75 | 74 | ssrdv | |
76 | 40 75 | eqssd | |