Step |
Hyp |
Ref |
Expression |
1 |
|
xrge0slmod.1 |
|- G = ( RR*s |`s ( 0 [,] +oo ) ) |
2 |
|
xrge0slmod.2 |
|- W = ( G |`v ( 0 [,) +oo ) ) |
3 |
|
xrge0cmn |
|- ( RR*s |`s ( 0 [,] +oo ) ) e. CMnd |
4 |
1 3
|
eqeltri |
|- G e. CMnd |
5 |
|
ovex |
|- ( 0 [,) +oo ) e. _V |
6 |
2
|
resvcmn |
|- ( ( 0 [,) +oo ) e. _V -> ( G e. CMnd <-> W e. CMnd ) ) |
7 |
5 6
|
ax-mp |
|- ( G e. CMnd <-> W e. CMnd ) |
8 |
4 7
|
mpbi |
|- W e. CMnd |
9 |
|
rge0srg |
|- ( CCfld |`s ( 0 [,) +oo ) ) e. SRing |
10 |
|
icossicc |
|- ( 0 [,) +oo ) C_ ( 0 [,] +oo ) |
11 |
|
simplr |
|- ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> r e. ( 0 [,) +oo ) ) |
12 |
10 11
|
sselid |
|- ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> r e. ( 0 [,] +oo ) ) |
13 |
|
simprr |
|- ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> w e. ( 0 [,] +oo ) ) |
14 |
|
ge0xmulcl |
|- ( ( r e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) -> ( r *e w ) e. ( 0 [,] +oo ) ) |
15 |
12 13 14
|
syl2anc |
|- ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> ( r *e w ) e. ( 0 [,] +oo ) ) |
16 |
|
simprl |
|- ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> x e. ( 0 [,] +oo ) ) |
17 |
|
xrge0adddi |
|- ( ( w e. ( 0 [,] +oo ) /\ x e. ( 0 [,] +oo ) /\ r e. ( 0 [,] +oo ) ) -> ( r *e ( w +e x ) ) = ( ( r *e w ) +e ( r *e x ) ) ) |
18 |
13 16 12 17
|
syl3anc |
|- ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> ( r *e ( w +e x ) ) = ( ( r *e w ) +e ( r *e x ) ) ) |
19 |
|
rge0ssre |
|- ( 0 [,) +oo ) C_ RR |
20 |
|
simpll |
|- ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> q e. ( 0 [,) +oo ) ) |
21 |
19 20
|
sselid |
|- ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> q e. RR ) |
22 |
19 11
|
sselid |
|- ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> r e. RR ) |
23 |
|
rexadd |
|- ( ( q e. RR /\ r e. RR ) -> ( q +e r ) = ( q + r ) ) |
24 |
21 22 23
|
syl2anc |
|- ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> ( q +e r ) = ( q + r ) ) |
25 |
24
|
oveq1d |
|- ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> ( ( q +e r ) *e w ) = ( ( q + r ) *e w ) ) |
26 |
10 20
|
sselid |
|- ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> q e. ( 0 [,] +oo ) ) |
27 |
|
xrge0adddir |
|- ( ( q e. ( 0 [,] +oo ) /\ r e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) -> ( ( q +e r ) *e w ) = ( ( q *e w ) +e ( r *e w ) ) ) |
28 |
26 12 13 27
|
syl3anc |
|- ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> ( ( q +e r ) *e w ) = ( ( q *e w ) +e ( r *e w ) ) ) |
29 |
25 28
|
eqtr3d |
|- ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> ( ( q + r ) *e w ) = ( ( q *e w ) +e ( r *e w ) ) ) |
30 |
15 18 29
|
3jca |
|- ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> ( ( r *e w ) e. ( 0 [,] +oo ) /\ ( r *e ( w +e x ) ) = ( ( r *e w ) +e ( r *e x ) ) /\ ( ( q + r ) *e w ) = ( ( q *e w ) +e ( r *e w ) ) ) ) |
31 |
|
rexmul |
|- ( ( q e. RR /\ r e. RR ) -> ( q *e r ) = ( q x. r ) ) |
32 |
21 22 31
|
syl2anc |
|- ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> ( q *e r ) = ( q x. r ) ) |
33 |
32
|
oveq1d |
|- ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> ( ( q *e r ) *e w ) = ( ( q x. r ) *e w ) ) |
34 |
21
|
rexrd |
|- ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> q e. RR* ) |
35 |
22
|
rexrd |
|- ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> r e. RR* ) |
36 |
|
iccssxr |
|- ( 0 [,] +oo ) C_ RR* |
37 |
36 13
|
sselid |
|- ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> w e. RR* ) |
38 |
|
xmulass |
|- ( ( q e. RR* /\ r e. RR* /\ w e. RR* ) -> ( ( q *e r ) *e w ) = ( q *e ( r *e w ) ) ) |
39 |
34 35 37 38
|
syl3anc |
|- ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> ( ( q *e r ) *e w ) = ( q *e ( r *e w ) ) ) |
40 |
33 39
|
eqtr3d |
|- ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> ( ( q x. r ) *e w ) = ( q *e ( r *e w ) ) ) |
41 |
|
xmulid2 |
|- ( w e. RR* -> ( 1 *e w ) = w ) |
42 |
37 41
|
syl |
|- ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> ( 1 *e w ) = w ) |
43 |
|
xmul02 |
|- ( w e. RR* -> ( 0 *e w ) = 0 ) |
44 |
37 43
|
syl |
|- ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> ( 0 *e w ) = 0 ) |
45 |
40 42 44
|
3jca |
|- ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> ( ( ( q x. r ) *e w ) = ( q *e ( r *e w ) ) /\ ( 1 *e w ) = w /\ ( 0 *e w ) = 0 ) ) |
46 |
30 45
|
jca |
|- ( ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) /\ ( x e. ( 0 [,] +oo ) /\ w e. ( 0 [,] +oo ) ) ) -> ( ( ( r *e w ) e. ( 0 [,] +oo ) /\ ( r *e ( w +e x ) ) = ( ( r *e w ) +e ( r *e x ) ) /\ ( ( q + r ) *e w ) = ( ( q *e w ) +e ( r *e w ) ) ) /\ ( ( ( q x. r ) *e w ) = ( q *e ( r *e w ) ) /\ ( 1 *e w ) = w /\ ( 0 *e w ) = 0 ) ) ) |
47 |
46
|
ralrimivva |
|- ( ( q e. ( 0 [,) +oo ) /\ r e. ( 0 [,) +oo ) ) -> A. x e. ( 0 [,] +oo ) A. w e. ( 0 [,] +oo ) ( ( ( r *e w ) e. ( 0 [,] +oo ) /\ ( r *e ( w +e x ) ) = ( ( r *e w ) +e ( r *e x ) ) /\ ( ( q + r ) *e w ) = ( ( q *e w ) +e ( r *e w ) ) ) /\ ( ( ( q x. r ) *e w ) = ( q *e ( r *e w ) ) /\ ( 1 *e w ) = w /\ ( 0 *e w ) = 0 ) ) ) |
48 |
47
|
rgen2 |
|- A. q e. ( 0 [,) +oo ) A. r e. ( 0 [,) +oo ) A. x e. ( 0 [,] +oo ) A. w e. ( 0 [,] +oo ) ( ( ( r *e w ) e. ( 0 [,] +oo ) /\ ( r *e ( w +e x ) ) = ( ( r *e w ) +e ( r *e x ) ) /\ ( ( q + r ) *e w ) = ( ( q *e w ) +e ( r *e w ) ) ) /\ ( ( ( q x. r ) *e w ) = ( q *e ( r *e w ) ) /\ ( 1 *e w ) = w /\ ( 0 *e w ) = 0 ) ) |
49 |
|
xrge0base |
|- ( 0 [,] +oo ) = ( Base ` ( RR*s |`s ( 0 [,] +oo ) ) ) |
50 |
1
|
fveq2i |
|- ( Base ` G ) = ( Base ` ( RR*s |`s ( 0 [,] +oo ) ) ) |
51 |
49 50
|
eqtr4i |
|- ( 0 [,] +oo ) = ( Base ` G ) |
52 |
2 51
|
resvbas |
|- ( ( 0 [,) +oo ) e. _V -> ( 0 [,] +oo ) = ( Base ` W ) ) |
53 |
5 52
|
ax-mp |
|- ( 0 [,] +oo ) = ( Base ` W ) |
54 |
|
xrge0plusg |
|- +e = ( +g ` ( RR*s |`s ( 0 [,] +oo ) ) ) |
55 |
1
|
fveq2i |
|- ( +g ` G ) = ( +g ` ( RR*s |`s ( 0 [,] +oo ) ) ) |
56 |
54 55
|
eqtr4i |
|- +e = ( +g ` G ) |
57 |
2 56
|
resvplusg |
|- ( ( 0 [,) +oo ) e. _V -> +e = ( +g ` W ) ) |
58 |
5 57
|
ax-mp |
|- +e = ( +g ` W ) |
59 |
|
ovex |
|- ( 0 [,] +oo ) e. _V |
60 |
|
ax-xrsvsca |
|- *e = ( .s ` RR*s ) |
61 |
1 60
|
ressvsca |
|- ( ( 0 [,] +oo ) e. _V -> *e = ( .s ` G ) ) |
62 |
59 61
|
ax-mp |
|- *e = ( .s ` G ) |
63 |
2 62
|
resvvsca |
|- ( ( 0 [,) +oo ) e. _V -> *e = ( .s ` W ) ) |
64 |
5 63
|
ax-mp |
|- *e = ( .s ` W ) |
65 |
|
xrge00 |
|- 0 = ( 0g ` ( RR*s |`s ( 0 [,] +oo ) ) ) |
66 |
1
|
fveq2i |
|- ( 0g ` G ) = ( 0g ` ( RR*s |`s ( 0 [,] +oo ) ) ) |
67 |
65 66
|
eqtr4i |
|- 0 = ( 0g ` G ) |
68 |
2 67
|
resv0g |
|- ( ( 0 [,) +oo ) e. _V -> 0 = ( 0g ` W ) ) |
69 |
5 68
|
ax-mp |
|- 0 = ( 0g ` W ) |
70 |
|
df-refld |
|- RRfld = ( CCfld |`s RR ) |
71 |
70
|
oveq1i |
|- ( RRfld |`s ( 0 [,) +oo ) ) = ( ( CCfld |`s RR ) |`s ( 0 [,) +oo ) ) |
72 |
|
reex |
|- RR e. _V |
73 |
|
ressress |
|- ( ( RR e. _V /\ ( 0 [,) +oo ) e. _V ) -> ( ( CCfld |`s RR ) |`s ( 0 [,) +oo ) ) = ( CCfld |`s ( RR i^i ( 0 [,) +oo ) ) ) ) |
74 |
72 5 73
|
mp2an |
|- ( ( CCfld |`s RR ) |`s ( 0 [,) +oo ) ) = ( CCfld |`s ( RR i^i ( 0 [,) +oo ) ) ) |
75 |
71 74
|
eqtri |
|- ( RRfld |`s ( 0 [,) +oo ) ) = ( CCfld |`s ( RR i^i ( 0 [,) +oo ) ) ) |
76 |
|
ax-xrssca |
|- RRfld = ( Scalar ` RR*s ) |
77 |
1 76
|
resssca |
|- ( ( 0 [,] +oo ) e. _V -> RRfld = ( Scalar ` G ) ) |
78 |
59 77
|
ax-mp |
|- RRfld = ( Scalar ` G ) |
79 |
|
rebase |
|- RR = ( Base ` RRfld ) |
80 |
2 78 79
|
resvsca |
|- ( ( 0 [,) +oo ) e. _V -> ( RRfld |`s ( 0 [,) +oo ) ) = ( Scalar ` W ) ) |
81 |
5 80
|
ax-mp |
|- ( RRfld |`s ( 0 [,) +oo ) ) = ( Scalar ` W ) |
82 |
|
incom |
|- ( ( 0 [,) +oo ) i^i RR ) = ( RR i^i ( 0 [,) +oo ) ) |
83 |
|
df-ss |
|- ( ( 0 [,) +oo ) C_ RR <-> ( ( 0 [,) +oo ) i^i RR ) = ( 0 [,) +oo ) ) |
84 |
19 83
|
mpbi |
|- ( ( 0 [,) +oo ) i^i RR ) = ( 0 [,) +oo ) |
85 |
82 84
|
eqtr3i |
|- ( RR i^i ( 0 [,) +oo ) ) = ( 0 [,) +oo ) |
86 |
85
|
oveq2i |
|- ( CCfld |`s ( RR i^i ( 0 [,) +oo ) ) ) = ( CCfld |`s ( 0 [,) +oo ) ) |
87 |
75 81 86
|
3eqtr3ri |
|- ( CCfld |`s ( 0 [,) +oo ) ) = ( Scalar ` W ) |
88 |
|
ax-resscn |
|- RR C_ CC |
89 |
19 88
|
sstri |
|- ( 0 [,) +oo ) C_ CC |
90 |
|
eqid |
|- ( CCfld |`s ( 0 [,) +oo ) ) = ( CCfld |`s ( 0 [,) +oo ) ) |
91 |
|
cnfldbas |
|- CC = ( Base ` CCfld ) |
92 |
90 91
|
ressbas2 |
|- ( ( 0 [,) +oo ) C_ CC -> ( 0 [,) +oo ) = ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) ) |
93 |
89 92
|
ax-mp |
|- ( 0 [,) +oo ) = ( Base ` ( CCfld |`s ( 0 [,) +oo ) ) ) |
94 |
|
cnfldadd |
|- + = ( +g ` CCfld ) |
95 |
90 94
|
ressplusg |
|- ( ( 0 [,) +oo ) e. _V -> + = ( +g ` ( CCfld |`s ( 0 [,) +oo ) ) ) ) |
96 |
5 95
|
ax-mp |
|- + = ( +g ` ( CCfld |`s ( 0 [,) +oo ) ) ) |
97 |
|
cnfldmul |
|- x. = ( .r ` CCfld ) |
98 |
90 97
|
ressmulr |
|- ( ( 0 [,) +oo ) e. _V -> x. = ( .r ` ( CCfld |`s ( 0 [,) +oo ) ) ) ) |
99 |
5 98
|
ax-mp |
|- x. = ( .r ` ( CCfld |`s ( 0 [,) +oo ) ) ) |
100 |
|
cndrng |
|- CCfld e. DivRing |
101 |
|
drngring |
|- ( CCfld e. DivRing -> CCfld e. Ring ) |
102 |
100 101
|
ax-mp |
|- CCfld e. Ring |
103 |
|
1re |
|- 1 e. RR |
104 |
|
0le1 |
|- 0 <_ 1 |
105 |
|
ltpnf |
|- ( 1 e. RR -> 1 < +oo ) |
106 |
103 105
|
ax-mp |
|- 1 < +oo |
107 |
103 104 106
|
3pm3.2i |
|- ( 1 e. RR /\ 0 <_ 1 /\ 1 < +oo ) |
108 |
|
0re |
|- 0 e. RR |
109 |
|
pnfxr |
|- +oo e. RR* |
110 |
|
elico2 |
|- ( ( 0 e. RR /\ +oo e. RR* ) -> ( 1 e. ( 0 [,) +oo ) <-> ( 1 e. RR /\ 0 <_ 1 /\ 1 < +oo ) ) ) |
111 |
108 109 110
|
mp2an |
|- ( 1 e. ( 0 [,) +oo ) <-> ( 1 e. RR /\ 0 <_ 1 /\ 1 < +oo ) ) |
112 |
107 111
|
mpbir |
|- 1 e. ( 0 [,) +oo ) |
113 |
|
cnfld1 |
|- 1 = ( 1r ` CCfld ) |
114 |
90 91 113
|
ress1r |
|- ( ( CCfld e. Ring /\ 1 e. ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ CC ) -> 1 = ( 1r ` ( CCfld |`s ( 0 [,) +oo ) ) ) ) |
115 |
102 112 89 114
|
mp3an |
|- 1 = ( 1r ` ( CCfld |`s ( 0 [,) +oo ) ) ) |
116 |
|
ringmnd |
|- ( CCfld e. Ring -> CCfld e. Mnd ) |
117 |
100 101 116
|
mp2b |
|- CCfld e. Mnd |
118 |
|
0e0icopnf |
|- 0 e. ( 0 [,) +oo ) |
119 |
|
cnfld0 |
|- 0 = ( 0g ` CCfld ) |
120 |
90 91 119
|
ress0g |
|- ( ( CCfld e. Mnd /\ 0 e. ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ CC ) -> 0 = ( 0g ` ( CCfld |`s ( 0 [,) +oo ) ) ) ) |
121 |
117 118 89 120
|
mp3an |
|- 0 = ( 0g ` ( CCfld |`s ( 0 [,) +oo ) ) ) |
122 |
53 58 64 69 87 93 96 99 115 121
|
isslmd |
|- ( W e. SLMod <-> ( W e. CMnd /\ ( CCfld |`s ( 0 [,) +oo ) ) e. SRing /\ A. q e. ( 0 [,) +oo ) A. r e. ( 0 [,) +oo ) A. x e. ( 0 [,] +oo ) A. w e. ( 0 [,] +oo ) ( ( ( r *e w ) e. ( 0 [,] +oo ) /\ ( r *e ( w +e x ) ) = ( ( r *e w ) +e ( r *e x ) ) /\ ( ( q + r ) *e w ) = ( ( q *e w ) +e ( r *e w ) ) ) /\ ( ( ( q x. r ) *e w ) = ( q *e ( r *e w ) ) /\ ( 1 *e w ) = w /\ ( 0 *e w ) = 0 ) ) ) ) |
123 |
8 9 48 122
|
mpbir3an |
|- W e. SLMod |