Step | Hyp | Ref
| Expression |
1 | | rellindf 20147 |
. . . . 5
LIndF |
2 | 1 | brrelexi 5158 |
. . . 4
LIndF
|
3 | | simp3 1063 |
. . . 4
LMHom
|
4 | | dmfex 7124 |
. . . 4
|
5 | 2, 3, 4 | syl2anr 495 |
. . 3
LMHom LIndF
|
6 | 5 | ex 450 |
. 2
LMHom
LIndF
|
7 | 1 | brrelexi 5158 |
. . . 4
LIndF
|
8 | | f1f 6101 |
. . . . . 6
|
9 | | fco 6058 |
. . . . . 6
|
10 | 8, 9 | sylan 488 |
. . . . 5
|
11 | 10 | 3adant1 1079 |
. . . 4
LMHom
|
12 | | dmfex 7124 |
. . . 4
|
13 | 7, 11, 12 | syl2anr 495 |
. . 3
LMHom
LIndF
|
14 | 13 | ex 450 |
. 2
LMHom
LIndF |
15 | | eldifi 3732 |
. . . . . . . . 9
Scalar
Scalar Scalar |
16 | | simpllr 799 |
. . . . . . . . . . . . 13
LMHom
Scalar
|
17 | | lmhmlmod1 19033 |
. . . . . . . . . . . . . . 15
LMHom
|
18 | 17 | ad3antrrr 766 |
. . . . . . . . . . . . . 14
LMHom
Scalar
|
19 | | simprr 796 |
. . . . . . . . . . . . . 14
LMHom
Scalar
Scalar |
20 | | simprl 794 |
. . . . . . . . . . . . . . 15
LMHom |
21 | | simpl 473 |
. . . . . . . . . . . . . . 15
Scalar |
22 | | ffvelrn 6357 |
. . . . . . . . . . . . . . 15
|
23 | 20, 21, 22 | syl2an 494 |
. . . . . . . . . . . . . 14
LMHom
Scalar
|
24 | | lindfmm.b |
. . . . . . . . . . . . . . 15
|
25 | | eqid 2622 |
. . . . . . . . . . . . . . 15
Scalar Scalar |
26 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
27 | | eqid 2622 |
. . . . . . . . . . . . . . 15
Scalar Scalar |
28 | 24, 25, 26, 27 | lmodvscl 18880 |
. . . . . . . . . . . . . 14
Scalar |
29 | 18, 19, 23, 28 | syl3anc 1326 |
. . . . . . . . . . . . 13
LMHom
Scalar
|
30 | | imassrn 5477 |
. . . . . . . . . . . . . . . 16
|
31 | | frn 6053 |
. . . . . . . . . . . . . . . . 17
|
32 | 31 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
33 | 30, 32 | syl5ss 3614 |
. . . . . . . . . . . . . . 15
|
34 | 33 | ad2antlr 763 |
. . . . . . . . . . . . . 14
LMHom
Scalar
|
35 | | eqid 2622 |
. . . . . . . . . . . . . . 15
|
36 | 24, 35 | lspssv 18983 |
. . . . . . . . . . . . . 14
|
37 | 18, 34, 36 | syl2anc 693 |
. . . . . . . . . . . . 13
LMHom
Scalar
|
38 | | f1elima 6520 |
. . . . . . . . . . . . 13
|
39 | 16, 29, 37, 38 | syl3anc 1326 |
. . . . . . . . . . . 12
LMHom
Scalar
|
40 | | simplll 798 |
. . . . . . . . . . . . . . 15
LMHom
Scalar
LMHom |
41 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
|
42 | 25, 27, 24, 26, 41 | lmhmlin 19035 |
. . . . . . . . . . . . . . 15
LMHom Scalar |
43 | 40, 19, 23, 42 | syl3anc 1326 |
. . . . . . . . . . . . . 14
LMHom
Scalar
|
44 | | ffn 6045 |
. . . . . . . . . . . . . . . . 17
|
45 | 44 | ad2antrl 764 |
. . . . . . . . . . . . . . . 16
LMHom
|
46 | | fvco2 6273 |
. . . . . . . . . . . . . . . 16
|
47 | 45, 21, 46 | syl2an 494 |
. . . . . . . . . . . . . . 15
LMHom
Scalar
|
48 | 47 | oveq2d 6666 |
. . . . . . . . . . . . . 14
LMHom
Scalar
|
49 | 43, 48 | eqtr4d 2659 |
. . . . . . . . . . . . 13
LMHom
Scalar
|
50 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
|
51 | 24, 35, 50 | lmhmlsp 19049 |
. . . . . . . . . . . . . . 15
LMHom
|
52 | 40, 34, 51 | syl2anc 693 |
. . . . . . . . . . . . . 14
LMHom
Scalar
|
53 | | imaco 5640 |
. . . . . . . . . . . . . . 15
|
54 | 53 | fveq2i 6194 |
. . . . . . . . . . . . . 14
|
55 | 52, 54 | syl6eqr 2674 |
. . . . . . . . . . . . 13
LMHom
Scalar
|
56 | 49, 55 | eleq12d 2695 |
. . . . . . . . . . . 12
LMHom
Scalar
|
57 | 39, 56 | bitr3d 270 |
. . . . . . . . . . 11
LMHom
Scalar
|
58 | 57 | notbid 308 |
. . . . . . . . . 10
LMHom
Scalar
|
59 | 58 | anassrs 680 |
. . . . . . . . 9
LMHom
Scalar
|
60 | 15, 59 | sylan2 491 |
. . . . . . . 8
LMHom
Scalar Scalar
|
61 | 60 | ralbidva 2985 |
. . . . . . 7
LMHom
Scalar Scalar Scalar Scalar |
62 | | eqid 2622 |
. . . . . . . . . . . 12
Scalar Scalar |
63 | 25, 62 | lmhmsca 19030 |
. . . . . . . . . . 11
LMHom
Scalar Scalar |
64 | 63 | fveq2d 6195 |
. . . . . . . . . 10
LMHom
Scalar Scalar |
65 | 63 | fveq2d 6195 |
. . . . . . . . . . 11
LMHom
Scalar Scalar |
66 | 65 | sneqd 4189 |
. . . . . . . . . 10
LMHom
Scalar Scalar |
67 | 64, 66 | difeq12d 3729 |
. . . . . . . . 9
LMHom
Scalar Scalar Scalar Scalar |
68 | 67 | ad3antrrr 766 |
. . . . . . . 8
LMHom
Scalar Scalar Scalar Scalar |
69 | 68 | raleqdv 3144 |
. . . . . . 7
LMHom
Scalar Scalar
Scalar Scalar |
70 | 61, 69 | bitr4d 271 |
. . . . . 6
LMHom
Scalar Scalar Scalar Scalar |
71 | 70 | ralbidva 2985 |
. . . . 5
LMHom Scalar Scalar
Scalar Scalar |
72 | 17 | ad2antrr 762 |
. . . . . 6
LMHom
|
73 | | simprr 796 |
. . . . . 6
LMHom
|
74 | | eqid 2622 |
. . . . . . 7
Scalar Scalar |
75 | 24, 26, 35, 25, 27, 74 | islindf2 20153 |
. . . . . 6
LIndF
Scalar Scalar |
76 | 72, 73, 20, 75 | syl3anc 1326 |
. . . . 5
LMHom LIndF
Scalar Scalar |
77 | | lmhmlmod2 19032 |
. . . . . . 7
LMHom
|
78 | 77 | ad2antrr 762 |
. . . . . 6
LMHom
|
79 | 10 | ad2ant2lr 784 |
. . . . . 6
LMHom |
80 | | lindfmm.c |
. . . . . . 7
|
81 | | eqid 2622 |
. . . . . . 7
Scalar Scalar |
82 | | eqid 2622 |
. . . . . . 7
Scalar Scalar |
83 | 80, 41, 50, 62, 81, 82 | islindf2 20153 |
. . . . . 6
LIndF
Scalar Scalar |
84 | 78, 73, 79, 83 | syl3anc 1326 |
. . . . 5
LMHom
LIndF
Scalar Scalar |
85 | 71, 76, 84 | 3bitr4d 300 |
. . . 4
LMHom LIndF
LIndF |
86 | 85 | exp32 631 |
. . 3
LMHom
LIndF LIndF |
87 | 86 | 3impia 1261 |
. 2
LMHom
LIndF
LIndF |
88 | 6, 14, 87 | pm5.21ndd 369 |
1
LMHom
LIndF
LIndF |