Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  xrge0slmod Structured version   Visualization version   GIF version
Theorem xrge0slmod 32452
Description: The extended nonnegative real numbers form a semiring left module. One could also have used subringAlg to get the same structure. (Contributed by Thierry Arnoux, 6-Sep-2018.)
Hypotheses
Ref Expression
xrge0slmod.1 𝐺 = (ℝ*𝑠 β†Ύs (0[,]+∞))
xrge0slmod.2 π‘Š = (𝐺 β†Ύv (0[,)+∞))
Assertion
Ref Expression
xrge0slmod π‘Š ∈ SLMod
Proof of Theorem xrge0slmod
Dummy variables π‘Ÿ π‘ž 𝑀 π‘₯ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xrge0slmod.1 . . . 4 𝐺 = (ℝ*𝑠 β†Ύs (0[,]+∞))
2 xrge0cmn 20980 . . . 4 (ℝ*𝑠 β†Ύs (0[,]+∞)) ∈ CMnd
31, 2eqeltri 2830 . . 3 𝐺 ∈ CMnd
4 ovex 7439 . . . 4 (0[,)+∞) ∈ V
5 xrge0slmod.2 . . . . 5 π‘Š = (𝐺 β†Ύv (0[,)+∞))
65resvcmn 32446 . . . 4 ((0[,)+∞) ∈ V β†’ (𝐺 ∈ CMnd ↔ π‘Š ∈ CMnd))
74, 6ax-mp 5 . . 3 (𝐺 ∈ CMnd ↔ π‘Š ∈ CMnd)
83, 7mpbi 229 . 2 π‘Š ∈ CMnd
9 rge0srg 21009 . 2 (β„‚fld β†Ύs (0[,)+∞)) ∈ SRing
10 icossicc 13410 . . . . . . . 8 (0[,)+∞) βŠ† (0[,]+∞)
11 simplr 768 . . . . . . . 8 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ π‘Ÿ ∈ (0[,)+∞))
1210, 11sselid 3980 . . . . . . 7 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ π‘Ÿ ∈ (0[,]+∞))
13 simprr 772 . . . . . . 7 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ 𝑀 ∈ (0[,]+∞))
14 ge0xmulcl 13437 . . . . . . 7 ((π‘Ÿ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞)) β†’ (π‘Ÿ Β·e 𝑀) ∈ (0[,]+∞))
1512, 13, 14syl2anc 585 . . . . . 6 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ (π‘Ÿ Β·e 𝑀) ∈ (0[,]+∞))
16 simprl 770 . . . . . . 7 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ π‘₯ ∈ (0[,]+∞))
17 xrge0adddi 32182 . . . . . . 7 ((𝑀 ∈ (0[,]+∞) ∧ π‘₯ ∈ (0[,]+∞) ∧ π‘Ÿ ∈ (0[,]+∞)) β†’ (π‘Ÿ Β·e (𝑀 +𝑒 π‘₯)) = ((π‘Ÿ Β·e 𝑀) +𝑒 (π‘Ÿ Β·e π‘₯)))
1813, 16, 12, 17syl3anc 1372 . . . . . 6 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ (π‘Ÿ Β·e (𝑀 +𝑒 π‘₯)) = ((π‘Ÿ Β·e 𝑀) +𝑒 (π‘Ÿ Β·e π‘₯)))
19 rge0ssre 13430 . . . . . . . . . 10 (0[,)+∞) βŠ† ℝ
20 simpll 766 . . . . . . . . . 10 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ π‘ž ∈ (0[,)+∞))
2119, 20sselid 3980 . . . . . . . . 9 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ π‘ž ∈ ℝ)
2219, 11sselid 3980 . . . . . . . . 9 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ π‘Ÿ ∈ ℝ)
23 rexadd 13208 . . . . . . . . 9 ((π‘ž ∈ ℝ ∧ π‘Ÿ ∈ ℝ) β†’ (π‘ž +𝑒 π‘Ÿ) = (π‘ž + π‘Ÿ))
2421, 22, 23syl2anc 585 . . . . . . . 8 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ (π‘ž +𝑒 π‘Ÿ) = (π‘ž + π‘Ÿ))
2524oveq1d 7421 . . . . . . 7 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ ((π‘ž +𝑒 π‘Ÿ) Β·e 𝑀) = ((π‘ž + π‘Ÿ) Β·e 𝑀))
2610, 20sselid 3980 . . . . . . . 8 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ π‘ž ∈ (0[,]+∞))
27 xrge0adddir 32181 . . . . . . . 8 ((π‘ž ∈ (0[,]+∞) ∧ π‘Ÿ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞)) β†’ ((π‘ž +𝑒 π‘Ÿ) Β·e 𝑀) = ((π‘ž Β·e 𝑀) +𝑒 (π‘Ÿ Β·e 𝑀)))
2826, 12, 13, 27syl3anc 1372 . . . . . . 7 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ ((π‘ž +𝑒 π‘Ÿ) Β·e 𝑀) = ((π‘ž Β·e 𝑀) +𝑒 (π‘Ÿ Β·e 𝑀)))
2925, 28eqtr3d 2775 . . . . . 6 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ ((π‘ž + π‘Ÿ) Β·e 𝑀) = ((π‘ž Β·e 𝑀) +𝑒 (π‘Ÿ Β·e 𝑀)))
3015, 18, 293jca 1129 . . . . 5 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ ((π‘Ÿ Β·e 𝑀) ∈ (0[,]+∞) ∧ (π‘Ÿ Β·e (𝑀 +𝑒 π‘₯)) = ((π‘Ÿ Β·e 𝑀) +𝑒 (π‘Ÿ Β·e π‘₯)) ∧ ((π‘ž + π‘Ÿ) Β·e 𝑀) = ((π‘ž Β·e 𝑀) +𝑒 (π‘Ÿ Β·e 𝑀))))
31 rexmul 13247 . . . . . . . . 9 ((π‘ž ∈ ℝ ∧ π‘Ÿ ∈ ℝ) β†’ (π‘ž Β·e π‘Ÿ) = (π‘ž Β· π‘Ÿ))
3221, 22, 31syl2anc 585 . . . . . . . 8 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ (π‘ž Β·e π‘Ÿ) = (π‘ž Β· π‘Ÿ))
3332oveq1d 7421 . . . . . . 7 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ ((π‘ž Β·e π‘Ÿ) Β·e 𝑀) = ((π‘ž Β· π‘Ÿ) Β·e 𝑀))
3421rexrd 11261 . . . . . . . 8 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ π‘ž ∈ ℝ*)
3522rexrd 11261 . . . . . . . 8 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ π‘Ÿ ∈ ℝ*)
36 iccssxr 13404 . . . . . . . . 9 (0[,]+∞) βŠ† ℝ*
3736, 13sselid 3980 . . . . . . . 8 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ 𝑀 ∈ ℝ*)
38 xmulass 13263 . . . . . . . 8 ((π‘ž ∈ ℝ* ∧ π‘Ÿ ∈ ℝ* ∧ 𝑀 ∈ ℝ*) β†’ ((π‘ž Β·e π‘Ÿ) Β·e 𝑀) = (π‘ž Β·e (π‘Ÿ Β·e 𝑀)))
3934, 35, 37, 38syl3anc 1372 . . . . . . 7 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ ((π‘ž Β·e π‘Ÿ) Β·e 𝑀) = (π‘ž Β·e (π‘Ÿ Β·e 𝑀)))
4033, 39eqtr3d 2775 . . . . . 6 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ ((π‘ž Β· π‘Ÿ) Β·e 𝑀) = (π‘ž Β·e (π‘Ÿ Β·e 𝑀)))
41 xmullid 13256 . . . . . . 7 (𝑀 ∈ ℝ* β†’ (1 Β·e 𝑀) = 𝑀)
4237, 41syl 17 . . . . . 6 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ (1 Β·e 𝑀) = 𝑀)
43 xmul02 13244 . . . . . . 7 (𝑀 ∈ ℝ* β†’ (0 Β·e 𝑀) = 0)
4437, 43syl 17 . . . . . 6 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ (0 Β·e 𝑀) = 0)
4540, 42, 443jca 1129 . . . . 5 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ (((π‘ž Β· π‘Ÿ) Β·e 𝑀) = (π‘ž Β·e (π‘Ÿ Β·e 𝑀)) ∧ (1 Β·e 𝑀) = 𝑀 ∧ (0 Β·e 𝑀) = 0))
4630, 45jca 513 . . . 4 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ (((π‘Ÿ Β·e 𝑀) ∈ (0[,]+∞) ∧ (π‘Ÿ Β·e (𝑀 +𝑒 π‘₯)) = ((π‘Ÿ Β·e 𝑀) +𝑒 (π‘Ÿ Β·e π‘₯)) ∧ ((π‘ž + π‘Ÿ) Β·e 𝑀) = ((π‘ž Β·e 𝑀) +𝑒 (π‘Ÿ Β·e 𝑀))) ∧ (((π‘ž Β· π‘Ÿ) Β·e 𝑀) = (π‘ž Β·e (π‘Ÿ Β·e 𝑀)) ∧ (1 Β·e 𝑀) = 𝑀 ∧ (0 Β·e 𝑀) = 0)))
4746ralrimivva 3201 . . 3 ((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) β†’ βˆ€π‘₯ ∈ (0[,]+∞)βˆ€π‘€ ∈ (0[,]+∞)(((π‘Ÿ Β·e 𝑀) ∈ (0[,]+∞) ∧ (π‘Ÿ Β·e (𝑀 +𝑒 π‘₯)) = ((π‘Ÿ Β·e 𝑀) +𝑒 (π‘Ÿ Β·e π‘₯)) ∧ ((π‘ž + π‘Ÿ) Β·e 𝑀) = ((π‘ž Β·e 𝑀) +𝑒 (π‘Ÿ Β·e 𝑀))) ∧ (((π‘ž Β· π‘Ÿ) Β·e 𝑀) = (π‘ž Β·e (π‘Ÿ Β·e 𝑀)) ∧ (1 Β·e 𝑀) = 𝑀 ∧ (0 Β·e 𝑀) = 0)))
4847rgen2 3198 . 2 βˆ€π‘ž ∈ (0[,)+∞)βˆ€π‘Ÿ ∈ (0[,)+∞)βˆ€π‘₯ ∈ (0[,]+∞)βˆ€π‘€ ∈ (0[,]+∞)(((π‘Ÿ Β·e 𝑀) ∈ (0[,]+∞) ∧ (π‘Ÿ Β·e (𝑀 +𝑒 π‘₯)) = ((π‘Ÿ Β·e 𝑀) +𝑒 (π‘Ÿ Β·e π‘₯)) ∧ ((π‘ž + π‘Ÿ) Β·e 𝑀) = ((π‘ž Β·e 𝑀) +𝑒 (π‘Ÿ Β·e 𝑀))) ∧ (((π‘ž Β· π‘Ÿ) Β·e 𝑀) = (π‘ž Β·e (π‘Ÿ Β·e 𝑀)) ∧ (1 Β·e 𝑀) = 𝑀 ∧ (0 Β·e 𝑀) = 0))
49 xrge0base 32174 . . . . . 6 (0[,]+∞) = (Baseβ€˜(ℝ*𝑠 β†Ύs (0[,]+∞)))
501fveq2i 6892 . . . . . 6 (Baseβ€˜πΊ) = (Baseβ€˜(ℝ*𝑠 β†Ύs (0[,]+∞)))
5149, 50eqtr4i 2764 . . . . 5 (0[,]+∞) = (Baseβ€˜πΊ)
525, 51resvbas 32436 . . . 4 ((0[,)+∞) ∈ V β†’ (0[,]+∞) = (Baseβ€˜π‘Š))
534, 52ax-mp 5 . . 3 (0[,]+∞) = (Baseβ€˜π‘Š)
54 xrge0plusg 32176 . . . . . 6 +𝑒 = (+gβ€˜(ℝ*𝑠 β†Ύs (0[,]+∞)))
551fveq2i 6892 . . . . . 6 (+gβ€˜πΊ) = (+gβ€˜(ℝ*𝑠 β†Ύs (0[,]+∞)))
5654, 55eqtr4i 2764 . . . . 5 +𝑒 = (+gβ€˜πΊ)
575, 56resvplusg 32438 . . . 4 ((0[,)+∞) ∈ V β†’ +𝑒 = (+gβ€˜π‘Š))
584, 57ax-mp 5 . . 3 +𝑒 = (+gβ€˜π‘Š)
59 ovex 7439 . . . . . 6 (0[,]+∞) ∈ V
60 ax-xrsvsca 32163 . . . . . . 7 Β·e = ( ·𝑠 β€˜β„*𝑠)
611, 60ressvsca 17286 . . . . . 6 ((0[,]+∞) ∈ V β†’ Β·e = ( ·𝑠 β€˜πΊ))
6259, 61ax-mp 5 . . . . 5 Β·e = ( ·𝑠 β€˜πΊ)
635, 62resvvsca 32440 . . . 4 ((0[,)+∞) ∈ V β†’ Β·e = ( ·𝑠 β€˜π‘Š))
644, 63ax-mp 5 . . 3 Β·e = ( ·𝑠 β€˜π‘Š)
65 xrge00 32175 . . . . . 6 0 = (0gβ€˜(ℝ*𝑠 β†Ύs (0[,]+∞)))
661fveq2i 6892 . . . . . 6 (0gβ€˜πΊ) = (0gβ€˜(ℝ*𝑠 β†Ύs (0[,]+∞)))
6765, 66eqtr4i 2764 . . . . 5 0 = (0gβ€˜πΊ)
685, 67resv0g 32444 . . . 4 ((0[,)+∞) ∈ V β†’ 0 = (0gβ€˜π‘Š))
694, 68ax-mp 5 . . 3 0 = (0gβ€˜π‘Š)
70 df-refld 21150 . . . . . 6 ℝfld = (β„‚fld β†Ύs ℝ)
7170oveq1i 7416 . . . . 5 (ℝfld β†Ύs (0[,)+∞)) = ((β„‚fld β†Ύs ℝ) β†Ύs (0[,)+∞))
72 reex 11198 . . . . . 6 ℝ ∈ V
73 ressress 17190 . . . . . 6 ((ℝ ∈ V ∧ (0[,)+∞) ∈ V) β†’ ((β„‚fld β†Ύs ℝ) β†Ύs (0[,)+∞)) = (β„‚fld β†Ύs (ℝ ∩ (0[,)+∞))))
7472, 4, 73mp2an 691 . . . . 5 ((β„‚fld β†Ύs ℝ) β†Ύs (0[,)+∞)) = (β„‚fld β†Ύs (ℝ ∩ (0[,)+∞)))
7571, 74eqtri 2761 . . . 4 (ℝfld β†Ύs (0[,)+∞)) = (β„‚fld β†Ύs (ℝ ∩ (0[,)+∞)))
76 ax-xrssca 32162 . . . . . . . 8 ℝfld = (Scalarβ€˜β„*𝑠)
771, 76resssca 17285 . . . . . . 7 ((0[,]+∞) ∈ V β†’ ℝfld = (Scalarβ€˜πΊ))
7859, 77ax-mp 5 . . . . . 6 ℝfld = (Scalarβ€˜πΊ)
79 rebase 21151 . . . . . 6 ℝ = (Baseβ€˜β„fld)
805, 78, 79resvsca 32433 . . . . 5 ((0[,)+∞) ∈ V β†’ (ℝfld β†Ύs (0[,)+∞)) = (Scalarβ€˜π‘Š))
814, 80ax-mp 5 . . . 4 (ℝfld β†Ύs (0[,)+∞)) = (Scalarβ€˜π‘Š)
82 incom 4201 . . . . . 6 ((0[,)+∞) ∩ ℝ) = (ℝ ∩ (0[,)+∞))
83 df-ss 3965 . . . . . . 7 ((0[,)+∞) βŠ† ℝ ↔ ((0[,)+∞) ∩ ℝ) = (0[,)+∞))
8419, 83mpbi 229 . . . . . 6 ((0[,)+∞) ∩ ℝ) = (0[,)+∞)
8582, 84eqtr3i 2763 . . . . 5 (ℝ ∩ (0[,)+∞)) = (0[,)+∞)
8685oveq2i 7417 . . . 4 (β„‚fld β†Ύs (ℝ ∩ (0[,)+∞))) = (β„‚fld β†Ύs (0[,)+∞))
8775, 81, 863eqtr3ri 2770 . . 3 (β„‚fld β†Ύs (0[,)+∞)) = (Scalarβ€˜π‘Š)
88 ax-resscn 11164 . . . . 5 ℝ βŠ† β„‚
8919, 88sstri 3991 . . . 4 (0[,)+∞) βŠ† β„‚
90 eqid 2733 . . . . 5 (β„‚fld β†Ύs (0[,)+∞)) = (β„‚fld β†Ύs (0[,)+∞))
91 cnfldbas 20941 . . . . 5 β„‚ = (Baseβ€˜β„‚fld)
9290, 91ressbas2 17179 . . . 4 ((0[,)+∞) βŠ† β„‚ β†’ (0[,)+∞) = (Baseβ€˜(β„‚fld β†Ύs (0[,)+∞))))
9389, 92ax-mp 5 . . 3 (0[,)+∞) = (Baseβ€˜(β„‚fld β†Ύs (0[,)+∞)))
94 cnfldadd 20942 . . . . 5 + = (+gβ€˜β„‚fld)
9590, 94ressplusg 17232 . . . 4 ((0[,)+∞) ∈ V β†’ + = (+gβ€˜(β„‚fld β†Ύs (0[,)+∞))))
964, 95ax-mp 5 . . 3 + = (+gβ€˜(β„‚fld β†Ύs (0[,)+∞)))
97 cnfldmul 20943 . . . . 5 Β· = (.rβ€˜β„‚fld)
9890, 97ressmulr 17249 . . . 4 ((0[,)+∞) ∈ V β†’ Β· = (.rβ€˜(β„‚fld β†Ύs (0[,)+∞))))
994, 98ax-mp 5 . . 3 Β· = (.rβ€˜(β„‚fld β†Ύs (0[,)+∞)))
100 cndrng 20967 . . . . 5 β„‚fld ∈ DivRing
101 drngring 20315 . . . . 5 (β„‚fld ∈ DivRing β†’ β„‚fld ∈ Ring)
102100, 101ax-mp 5 . . . 4 β„‚fld ∈ Ring
103 1re 11211 . . . . . 6 1 ∈ ℝ
104 0le1 11734 . . . . . 6 0 ≀ 1
105 ltpnf 13097 . . . . . . 7 (1 ∈ ℝ β†’ 1 < +∞)
106103, 105ax-mp 5 . . . . . 6 1 < +∞
107103, 104, 1063pm3.2i 1340 . . . . 5 (1 ∈ ℝ ∧ 0 ≀ 1 ∧ 1 < +∞)
108 0re 11213 . . . . . 6 0 ∈ ℝ
109 pnfxr 11265 . . . . . 6 +∞ ∈ ℝ*
110 elico2 13385 . . . . . 6 ((0 ∈ ℝ ∧ +∞ ∈ ℝ*) β†’ (1 ∈ (0[,)+∞) ↔ (1 ∈ ℝ ∧ 0 ≀ 1 ∧ 1 < +∞)))
111108, 109, 110mp2an 691 . . . . 5 (1 ∈ (0[,)+∞) ↔ (1 ∈ ℝ ∧ 0 ≀ 1 ∧ 1 < +∞))
112107, 111mpbir 230 . . . 4 1 ∈ (0[,)+∞)
113 cnfld1 20963 . . . . 5 1 = (1rβ€˜β„‚fld)
11490, 91, 113ress1r 32372 . . . 4 ((β„‚fld ∈ Ring ∧ 1 ∈ (0[,)+∞) ∧ (0[,)+∞) βŠ† β„‚) β†’ 1 = (1rβ€˜(β„‚fld β†Ύs (0[,)+∞))))
115102, 112, 89, 114mp3an 1462 . . 3 1 = (1rβ€˜(β„‚fld β†Ύs (0[,)+∞)))
116 ringmnd 20060 . . . . 5 (β„‚fld ∈ Ring β†’ β„‚fld ∈ Mnd)
117100, 101, 116mp2b 10 . . . 4 β„‚fld ∈ Mnd
118 0e0icopnf 13432 . . . 4 0 ∈ (0[,)+∞)
119 cnfld0 20962 . . . . 5 0 = (0gβ€˜β„‚fld)
12090, 91, 119ress0g 18650 . . . 4 ((β„‚fld ∈ Mnd ∧ 0 ∈ (0[,)+∞) ∧ (0[,)+∞) βŠ† β„‚) β†’ 0 = (0gβ€˜(β„‚fld β†Ύs (0[,)+∞))))
121117, 118, 89, 120mp3an 1462 . . 3 0 = (0gβ€˜(β„‚fld β†Ύs (0[,)+∞)))
12253, 58, 64, 69, 87, 93, 96, 99, 115, 121isslmd 32335 . 2 (π‘Š ∈ SLMod ↔ (π‘Š ∈ CMnd ∧ (β„‚fld β†Ύs (0[,)+∞)) ∈ SRing ∧ βˆ€π‘ž ∈ (0[,)+∞)βˆ€π‘Ÿ ∈ (0[,)+∞)βˆ€π‘₯ ∈ (0[,]+∞)βˆ€π‘€ ∈ (0[,]+∞)(((π‘Ÿ Β·e 𝑀) ∈ (0[,]+∞) ∧ (π‘Ÿ Β·e (𝑀 +𝑒 π‘₯)) = ((π‘Ÿ Β·e 𝑀) +𝑒 (π‘Ÿ Β·e π‘₯)) ∧ ((π‘ž + π‘Ÿ) Β·e 𝑀) = ((π‘ž Β·e 𝑀) +𝑒 (π‘Ÿ Β·e 𝑀))) ∧ (((π‘ž Β· π‘Ÿ) Β·e 𝑀) = (π‘ž Β·e (π‘Ÿ Β·e 𝑀)) ∧ (1 Β·e 𝑀) = 𝑀 ∧ (0 Β·e 𝑀) = 0))))
1238, 9, 48, 122mpbir3an 1342 1 π‘Š ∈ SLMod
Colors of variables: wff setvar class
Syntax hints:   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆ€wral 3062  Vcvv 3475   ∩ cin 3947   βŠ† wss 3948   class class class wbr 5148  β€˜cfv 6541  (class class class)co 7406  β„‚cc 11105  β„cr 11106  0cc0 11107  1c1 11108   + caddc 11110   Β· cmul 11112  +∞cpnf 11242  β„*cxr 11244   < clt 11245   ≀ cle 11246   +𝑒 cxad 13087   Β·e cxmu 13088  [,)cico 13323  [,]cicc 13324  Basecbs 17141   β†Ύs cress 17170  +gcplusg 17194  .rcmulr 17195  Scalarcsca 17197   ·𝑠 cvsca 17198  0gc0g 17382  β„*𝑠cxrs 17443  Mndcmnd 18622  CMndccmn 19643  1rcur 19999  SRingcsrg 20003  Ringcrg 20050  DivRingcdr 20308  β„‚fldccnfld 20937  β„fldcrefld 21149  SLModcslmd 32333   β†Ύv cresv 32427
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184  ax-addf 11186  ax-mulf 11187  ax-xrssca 32162  ax-xrsvsca 32163
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-1st 7972  df-2nd 7973  df-tpos 8208  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-1o 8463  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-4 12274  df-5 12275  df-6 12276  df-7 12277  df-8 12278  df-9 12279  df-n0 12470  df-z 12556  df-dec 12675  df-uz 12820  df-xneg 13089  df-xadd 13090  df-xmul 13091  df-ico 13327  df-icc 13328  df-fz 13482  df-struct 17077  df-sets 17094  df-slot 17112  df-ndx 17124  df-base 17142  df-ress 17171  df-plusg 17207  df-mulr 17208  df-starv 17209  df-sca 17210  df-vsca 17211  df-tset 17213  df-ple 17214  df-ds 17216  df-unif 17217  df-0g 17384  df-xrs 17445  df-mgm 18558  df-sgrp 18607  df-mnd 18623  df-submnd 18669  df-grp 18819  df-minusg 18820  df-cmn 19645  df-abl 19646  df-mgp 19983  df-ur 20000  df-srg 20004  df-ring 20052  df-cring 20053  df-oppr 20143  df-dvdsr 20164  df-unit 20165  df-invr 20195  df-dvr 20208  df-drng 20310  df-cnfld 20938  df-refld 21150  df-slmd 32334  df-resv 32428
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator