Step | Hyp | Ref
| Expression |
1 | | eqlkr3.w |
. . . 4
|
2 | | eqlkr3.g |
. . . 4
|
3 | | eqlkr3.s |
. . . . 5
Scalar |
4 | | eqlkr3.r |
. . . . 5
|
5 | | eqlkr3.v |
. . . . 5
|
6 | | eqlkr3.f |
. . . . 5
LFnl |
7 | 3, 4, 5, 6 | lflf 34350 |
. . . 4
|
8 | 1, 2, 7 | syl2anc 693 |
. . 3
|
9 | | ffn 6045 |
. . 3
|
10 | 8, 9 | syl 17 |
. 2
|
11 | | eqlkr3.h |
. . . 4
|
12 | 3, 4, 5, 6 | lflf 34350 |
. . . 4
|
13 | 1, 11, 12 | syl2anc 693 |
. . 3
|
14 | | ffn 6045 |
. . 3
|
15 | 13, 14 | syl 17 |
. 2
|
16 | | eqlkr3.e |
. . . . . . 7
|
17 | | eqid 2622 |
. . . . . . . 8
|
18 | | eqlkr3.k |
. . . . . . . 8
LKer |
19 | 3, 4, 17, 5, 6, 18 | eqlkr 34386 |
. . . . . . 7
|
20 | 1, 2, 11, 16, 19 | syl121anc 1331 |
. . . . . 6
|
21 | | eqlkr3.x |
. . . . . . . . . . 11
|
22 | 21 | adantr 481 |
. . . . . . . . . 10
|
23 | | fveq2 6191 |
. . . . . . . . . . . 12
|
24 | | fveq2 6191 |
. . . . . . . . . . . . 13
|
25 | 24 | oveq1d 6665 |
. . . . . . . . . . . 12
|
26 | 23, 25 | eqeq12d 2637 |
. . . . . . . . . . 11
|
27 | 26 | rspcv 3305 |
. . . . . . . . . 10
|
28 | 22, 27 | syl 17 |
. . . . . . . . 9
|
29 | | eqlkr3.a |
. . . . . . . . . . . . . . 15
|
30 | 29 | adantr 481 |
. . . . . . . . . . . . . 14
|
31 | 30 | adantr 481 |
. . . . . . . . . . . . 13
|
32 | | simpr 477 |
. . . . . . . . . . . . 13
|
33 | 31, 32 | eqtr2d 2657 |
. . . . . . . . . . . 12
|
34 | 33 | oveq2d 6666 |
. . . . . . . . . . 11
|
35 | 3 | lvecdrng 19105 |
. . . . . . . . . . . . . . . . 17
|
36 | 1, 35 | syl 17 |
. . . . . . . . . . . . . . . 16
|
37 | 36 | adantr 481 |
. . . . . . . . . . . . . . 15
|
38 | 3, 4, 5, 6 | lflcl 34351 |
. . . . . . . . . . . . . . . . 17
|
39 | 1, 2, 21, 38 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
40 | 39 | adantr 481 |
. . . . . . . . . . . . . . 15
|
41 | | eqlkr3.n |
. . . . . . . . . . . . . . . 16
|
42 | 41 | adantr 481 |
. . . . . . . . . . . . . . 15
|
43 | | eqlkr3.o |
. . . . . . . . . . . . . . . 16
|
44 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
|
45 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
|
46 | 4, 43, 17, 44, 45 | drnginvrl 18766 |
. . . . . . . . . . . . . . 15
|
47 | 37, 40, 42, 46 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
48 | 47 | oveq1d 6665 |
. . . . . . . . . . . . 13
|
49 | | lveclmod 19106 |
. . . . . . . . . . . . . . . . 17
|
50 | 1, 49 | syl 17 |
. . . . . . . . . . . . . . . 16
|
51 | 3 | lmodring 18871 |
. . . . . . . . . . . . . . . 16
|
52 | 50, 51 | syl 17 |
. . . . . . . . . . . . . . 15
|
53 | 52 | adantr 481 |
. . . . . . . . . . . . . 14
|
54 | 4, 43, 45 | drnginvrcl 18764 |
. . . . . . . . . . . . . . 15
|
55 | 37, 40, 42, 54 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
56 | | simpr 477 |
. . . . . . . . . . . . . 14
|
57 | 4, 17 | ringass 18564 |
. . . . . . . . . . . . . 14
|
58 | 53, 55, 40, 56, 57 | syl13anc 1328 |
. . . . . . . . . . . . 13
|
59 | 4, 17, 44 | ringlidm 18571 |
. . . . . . . . . . . . . 14
|
60 | 53, 56, 59 | syl2anc 693 |
. . . . . . . . . . . . 13
|
61 | 48, 58, 60 | 3eqtr3d 2664 |
. . . . . . . . . . . 12
|
62 | 61 | adantr 481 |
. . . . . . . . . . 11
|
63 | 47 | adantr 481 |
. . . . . . . . . . 11
|
64 | 34, 62, 63 | 3eqtr3d 2664 |
. . . . . . . . . 10
|
65 | 64 | ex 450 |
. . . . . . . . 9
|
66 | 28, 65 | syld 47 |
. . . . . . . 8
|
67 | 66 | ancrd 577 |
. . . . . . 7
|
68 | 67 | reximdva 3017 |
. . . . . 6
|
69 | 20, 68 | mpd 15 |
. . . . 5
|
70 | 4, 44 | ringidcl 18568 |
. . . . . . 7
|
71 | 52, 70 | syl 17 |
. . . . . 6
|
72 | | oveq2 6658 |
. . . . . . . . 9
|
73 | 72 | eqeq2d 2632 |
. . . . . . . 8
|
74 | 73 | ralbidv 2986 |
. . . . . . 7
|
75 | 74 | ceqsrexv 3336 |
. . . . . 6
|
76 | 71, 75 | syl 17 |
. . . . 5
|
77 | 69, 76 | mpbid 222 |
. . . 4
|
78 | 77 | r19.21bi 2932 |
. . 3
|
79 | 50 | adantr 481 |
. . . . 5
|
80 | 79, 51 | syl 17 |
. . . 4
|
81 | 1 | adantr 481 |
. . . . 5
|
82 | 2 | adantr 481 |
. . . . 5
|
83 | | simpr 477 |
. . . . 5
|
84 | 3, 4, 5, 6 | lflcl 34351 |
. . . . 5
|
85 | 81, 82, 83, 84 | syl3anc 1326 |
. . . 4
|
86 | 4, 17, 44 | ringridm 18572 |
. . . 4
|
87 | 80, 85, 86 | syl2anc 693 |
. . 3
|
88 | 78, 87 | eqtr2d 2657 |
. 2
|
89 | 10, 15, 88 | eqfnfvd 6314 |
1
|