![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > lcfrlem1 | Structured version Visualization version Unicode version |
Description: Lemma for lcfr 35199. Note that ![]() |
Ref | Expression |
---|---|
lcfrlem1.v |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem1.s |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem1.q |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem1.z |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem1.i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem1.f |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem1.d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem1.t |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem1.m |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem1.u |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem1.e |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem1.g |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem1.x |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem1.n |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
lcfrlem1.h |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
lcfrlem1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lcfrlem1.h |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | fveq1i 5893 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | lcfrlem1.v |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | lcfrlem1.s |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | eqid 2462 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | lcfrlem1.f |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | lcfrlem1.d |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | lcfrlem1.m |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | lcfrlem1.u |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
10 | lveclmod 18384 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
11 | 9, 10 | syl 17 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
12 | lcfrlem1.e |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
13 | eqid 2462 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
14 | lcfrlem1.t |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
15 | 4 | lvecdrng 18383 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
16 | 9, 15 | syl 17 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
17 | lcfrlem1.g |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
18 | lcfrlem1.x |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
19 | 4, 13, 3, 6 | lflcl 32676 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
20 | 9, 17, 18, 19 | syl3anc 1276 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
21 | lcfrlem1.n |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
22 | lcfrlem1.z |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
23 | lcfrlem1.i |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
24 | 13, 22, 23 | drnginvrcl 18047 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
25 | 16, 20, 21, 24 | syl3anc 1276 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
26 | 4, 13, 3, 6 | lflcl 32676 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
27 | 9, 12, 18, 26 | syl3anc 1276 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
28 | lcfrlem1.q |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
29 | 4, 13, 28 | lmodmcl 18158 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
30 | 11, 25, 27, 29 | syl3anc 1276 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
31 | 6, 4, 13, 7, 14, 11, 30, 17 | ldualvscl 32751 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
32 | 3, 4, 5, 6, 7, 8, 11, 12, 31, 18 | ldualvsubval 32769 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
33 | 6, 3, 4, 13, 28, 7, 14, 9, 30, 17, 18 | ldualvsval 32750 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
34 | eqid 2462 |
. . . . . . . . 9
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
35 | 13, 22, 28, 34, 23 | drnginvrr 18050 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
36 | 16, 20, 21, 35 | syl3anc 1276 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
37 | 36 | oveq1d 6335 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
38 | 4 | lmodring 18154 |
. . . . . . . 8
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
39 | 11, 38 | syl 17 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
40 | 13, 28 | ringass 17852 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
41 | 39, 20, 25, 27, 40 | syl13anc 1278 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
42 | 13, 28, 34 | ringlidm 17859 |
. . . . . . 7
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
43 | 39, 27, 42 | syl2anc 671 |
. . . . . 6
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
44 | 37, 41, 43 | 3eqtr3d 2504 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
45 | 33, 44 | eqtrd 2496 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
46 | 45 | oveq2d 6336 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
47 | 4 | lmodfgrp 18155 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
48 | 11, 47 | syl 17 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
49 | 13, 22, 5 | grpsubid 16793 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
50 | 48, 27, 49 | syl2anc 671 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
51 | 32, 46, 50 | 3eqtrd 2500 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
52 | 2, 51 | syl5eq 2508 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-8 1900 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-rep 4531 ax-sep 4541 ax-nul 4550 ax-pow 4598 ax-pr 4656 ax-un 6615 ax-cnex 9626 ax-resscn 9627 ax-1cn 9628 ax-icn 9629 ax-addcl 9630 ax-addrcl 9631 ax-mulcl 9632 ax-mulrcl 9633 ax-mulcom 9634 ax-addass 9635 ax-mulass 9636 ax-distr 9637 ax-i2m1 9638 ax-1ne0 9639 ax-1rid 9640 ax-rnegex 9641 ax-rrecex 9642 ax-cnre 9643 ax-pre-lttri 9644 ax-pre-lttrn 9645 ax-pre-ltadd 9646 ax-pre-mulgt0 9647 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 992 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-nel 2636 df-ral 2754 df-rex 2755 df-reu 2756 df-rmo 2757 df-rab 2758 df-v 3059 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-pss 3432 df-nul 3744 df-if 3894 df-pw 3965 df-sn 3981 df-pr 3983 df-tp 3985 df-op 3987 df-uni 4213 df-int 4249 df-iun 4294 df-br 4419 df-opab 4478 df-mpt 4479 df-tr 4514 df-eprel 4767 df-id 4771 df-po 4777 df-so 4778 df-fr 4815 df-we 4817 df-xp 4862 df-rel 4863 df-cnv 4864 df-co 4865 df-dm 4866 df-rn 4867 df-res 4868 df-ima 4869 df-pred 5403 df-ord 5449 df-on 5450 df-lim 5451 df-suc 5452 df-iota 5569 df-fun 5607 df-fn 5608 df-f 5609 df-f1 5610 df-fo 5611 df-f1o 5612 df-fv 5613 df-riota 6282 df-ov 6323 df-oprab 6324 df-mpt2 6325 df-of 6563 df-om 6725 df-1st 6825 df-2nd 6826 df-tpos 7004 df-wrecs 7059 df-recs 7121 df-rdg 7159 df-1o 7213 df-oadd 7217 df-er 7394 df-map 7505 df-en 7601 df-dom 7602 df-sdom 7603 df-fin 7604 df-pnf 9708 df-mnf 9709 df-xr 9710 df-ltxr 9711 df-le 9712 df-sub 9893 df-neg 9894 df-nn 10643 df-2 10701 df-3 10702 df-4 10703 df-5 10704 df-6 10705 df-n0 10904 df-z 10972 df-uz 11194 df-fz 11820 df-struct 15178 df-ndx 15179 df-slot 15180 df-base 15181 df-sets 15182 df-ress 15183 df-plusg 15258 df-mulr 15259 df-sca 15261 df-vsca 15262 df-0g 15395 df-mgm 16543 df-sgrp 16582 df-mnd 16592 df-grp 16728 df-minusg 16729 df-sbg 16730 df-cmn 17487 df-abl 17488 df-mgp 17779 df-ur 17791 df-ring 17837 df-oppr 17906 df-dvdsr 17924 df-unit 17925 df-invr 17955 df-drng 18032 df-lmod 18148 df-lvec 18381 df-lfl 32670 df-ldual 32736 |
This theorem is referenced by: lcfrlem3 35158 |
Copyright terms: Public domain | W3C validator |