Step | Hyp | Ref
| Expression |
1 | | xrge0slmod.1 |
. . . 4
↾s |
2 | | xrge0cmn 19788 |
. . . 4
↾s CMnd |
3 | 1, 2 | eqeltri 2697 |
. . 3
CMnd |
4 | | ovex 6678 |
. . . 4
|
5 | | xrge0slmod.2 |
. . . . 5
↾v |
6 | 5 | resvcmn 29838 |
. . . 4
CMnd
CMnd |
7 | 4, 6 | ax-mp 5 |
. . 3
CMnd CMnd |
8 | 3, 7 | mpbi 220 |
. 2
CMnd |
9 | | rge0srg 19817 |
. 2
ℂfld
↾s SRing |
10 | | icossicc 12260 |
. . . . . . . 8
|
11 | | simplr 792 |
. . . . . . . 8
|
12 | 10, 11 | sseldi 3601 |
. . . . . . 7
|
13 | | simprr 796 |
. . . . . . 7
|
14 | | ge0xmulcl 12287 |
. . . . . . 7
|
15 | 12, 13, 14 | syl2anc 693 |
. . . . . 6
|
16 | | simprl 794 |
. . . . . . 7
|
17 | | xrge0adddi 29693 |
. . . . . . 7
|
18 | 13, 16, 12, 17 | syl3anc 1326 |
. . . . . 6
|
19 | | rge0ssre 12280 |
. . . . . . . . . 10
|
20 | | simpll 790 |
. . . . . . . . . 10
|
21 | 19, 20 | sseldi 3601 |
. . . . . . . . 9
|
22 | 19, 11 | sseldi 3601 |
. . . . . . . . 9
|
23 | | rexadd 12063 |
. . . . . . . . 9
|
24 | 21, 22, 23 | syl2anc 693 |
. . . . . . . 8
|
25 | 24 | oveq1d 6665 |
. . . . . . 7
|
26 | 10, 20 | sseldi 3601 |
. . . . . . . 8
|
27 | | xrge0adddir 29692 |
. . . . . . . 8
|
28 | 26, 12, 13, 27 | syl3anc 1326 |
. . . . . . 7
|
29 | 25, 28 | eqtr3d 2658 |
. . . . . 6
|
30 | 15, 18, 29 | 3jca 1242 |
. . . . 5
|
31 | | rexmul 12101 |
. . . . . . . . 9
|
32 | 21, 22, 31 | syl2anc 693 |
. . . . . . . 8
|
33 | 32 | oveq1d 6665 |
. . . . . . 7
|
34 | 21 | rexrd 10089 |
. . . . . . . 8
|
35 | 22 | rexrd 10089 |
. . . . . . . 8
|
36 | | iccssxr 12256 |
. . . . . . . . 9
|
37 | 36, 13 | sseldi 3601 |
. . . . . . . 8
|
38 | | xmulass 12117 |
. . . . . . . 8
|
39 | 34, 35, 37, 38 | syl3anc 1326 |
. . . . . . 7
|
40 | 33, 39 | eqtr3d 2658 |
. . . . . 6
|
41 | | xmulid2 12110 |
. . . . . . 7
|
42 | 37, 41 | syl 17 |
. . . . . 6
|
43 | | xmul02 12098 |
. . . . . . 7
|
44 | 37, 43 | syl 17 |
. . . . . 6
|
45 | 40, 42, 44 | 3jca 1242 |
. . . . 5
|
46 | 30, 45 | jca 554 |
. . . 4
|
47 | 46 | ralrimivva 2971 |
. . 3
|
48 | 47 | rgen2a 2977 |
. 2
|
49 | | xrge0base 29685 |
. . . . . 6
↾s |
50 | 1 | fveq2i 6194 |
. . . . . 6
↾s |
51 | 49, 50 | eqtr4i 2647 |
. . . . 5
|
52 | 5, 51 | resvbas 29832 |
. . . 4
|
53 | 4, 52 | ax-mp 5 |
. . 3
|
54 | | xrge0plusg 29687 |
. . . . . 6
↾s |
55 | 1 | fveq2i 6194 |
. . . . . 6
↾s |
56 | 54, 55 | eqtr4i 2647 |
. . . . 5
|
57 | 5, 56 | resvplusg 29833 |
. . . 4
|
58 | 4, 57 | ax-mp 5 |
. . 3
|
59 | | ovex 6678 |
. . . . . 6
|
60 | | ax-xrsvsca 29674 |
. . . . . . 7
|
61 | 1, 60 | ressvsca 16032 |
. . . . . 6
|
62 | 59, 61 | ax-mp 5 |
. . . . 5
|
63 | 5, 62 | resvvsca 29834 |
. . . 4
|
64 | 4, 63 | ax-mp 5 |
. . 3
|
65 | | xrge00 29686 |
. . . . . 6
↾s |
66 | 1 | fveq2i 6194 |
. . . . . 6
↾s |
67 | 65, 66 | eqtr4i 2647 |
. . . . 5
|
68 | 5, 67 | resv0g 29836 |
. . . 4
|
69 | 4, 68 | ax-mp 5 |
. . 3
|
70 | | df-refld 19951 |
. . . . . 6
RRfld ℂfld ↾s |
71 | 70 | oveq1i 6660 |
. . . . 5
RRfld ↾s
ℂfld
↾s
↾s |
72 | | reex 10027 |
. . . . . 6
|
73 | | ressress 15938 |
. . . . . 6
ℂfld ↾s ↾s ℂfld ↾s |
74 | 72, 4, 73 | mp2an 708 |
. . . . 5
ℂfld ↾s ↾s ℂfld
↾s |
75 | 71, 74 | eqtri 2644 |
. . . 4
RRfld ↾s
ℂfld ↾s |
76 | | ax-xrssca 29673 |
. . . . . . . 8
RRfld Scalar |
77 | 1, 76 | resssca 16031 |
. . . . . . 7
RRfld Scalar |
78 | 59, 77 | ax-mp 5 |
. . . . . 6
RRfld Scalar |
79 | | rebase 19952 |
. . . . . 6
RRfld |
80 | 5, 78, 79 | resvsca 29830 |
. . . . 5
RRfld
↾s Scalar |
81 | 4, 80 | ax-mp 5 |
. . . 4
RRfld ↾s
Scalar |
82 | | incom 3805 |
. . . . . 6
|
83 | | df-ss 3588 |
. . . . . . 7
|
84 | 19, 83 | mpbi 220 |
. . . . . 6
|
85 | 82, 84 | eqtr3i 2646 |
. . . . 5
|
86 | 85 | oveq2i 6661 |
. . . 4
ℂfld
↾s ℂfld ↾s |
87 | 75, 81, 86 | 3eqtr3ri 2653 |
. . 3
ℂfld
↾s Scalar |
88 | | ax-resscn 9993 |
. . . . 5
|
89 | 19, 88 | sstri 3612 |
. . . 4
|
90 | | eqid 2622 |
. . . . 5
ℂfld
↾s ℂfld ↾s |
91 | | cnfldbas 19750 |
. . . . 5
ℂfld |
92 | 90, 91 | ressbas2 15931 |
. . . 4
ℂfld ↾s
|
93 | 89, 92 | ax-mp 5 |
. . 3
ℂfld ↾s
|
94 | | cnfldadd 19751 |
. . . . 5
ℂfld |
95 | 90, 94 | ressplusg 15993 |
. . . 4
ℂfld
↾s |
96 | 4, 95 | ax-mp 5 |
. . 3
ℂfld
↾s |
97 | | cnfldmul 19752 |
. . . . 5
ℂfld |
98 | 90, 97 | ressmulr 16006 |
. . . 4
ℂfld
↾s |
99 | 4, 98 | ax-mp 5 |
. . 3
ℂfld
↾s |
100 | | cndrng 19775 |
. . . . 5
ℂfld |
101 | | drngring 18754 |
. . . . 5
ℂfld ℂfld |
102 | 100, 101 | ax-mp 5 |
. . . 4
ℂfld |
103 | | 1re 10039 |
. . . . . 6
|
104 | | 0le1 10551 |
. . . . . 6
|
105 | | ltpnf 11954 |
. . . . . . 7
|
106 | 103, 105 | ax-mp 5 |
. . . . . 6
|
107 | 103, 104,
106 | 3pm3.2i 1239 |
. . . . 5
|
108 | | 0re 10040 |
. . . . . 6
|
109 | | pnfxr 10092 |
. . . . . 6
|
110 | | elico2 12237 |
. . . . . 6
|
111 | 108, 109,
110 | mp2an 708 |
. . . . 5
|
112 | 107, 111 | mpbir 221 |
. . . 4
|
113 | | cnfld1 19771 |
. . . . 5
ℂfld |
114 | 90, 91, 113 | ress1r 29789 |
. . . 4
ℂfld ℂfld ↾s |
115 | 102, 112,
89, 114 | mp3an 1424 |
. . 3
ℂfld ↾s
|
116 | | ringmnd 18556 |
. . . . 5
ℂfld ℂfld |
117 | 100, 101,
116 | mp2b 10 |
. . . 4
ℂfld |
118 | | 0e0icopnf 12282 |
. . . 4
|
119 | | cnfld0 19770 |
. . . . 5
ℂfld |
120 | 90, 91, 119 | ress0g 17319 |
. . . 4
ℂfld
ℂfld
↾s |
121 | 117, 118,
89, 120 | mp3an 1424 |
. . 3
ℂfld ↾s
|
122 | 53, 58, 64, 69, 87, 93, 96, 99, 115, 121 | isslmd 29755 |
. 2
SLMod CMnd ℂfld ↾s
SRing
|
123 | 8, 9, 48, 122 | mpbir3an 1244 |
1
SLMod |