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 32929
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 21271 . . . 4 (ℝ*𝑠 β†Ύs (0[,]+∞)) ∈ CMnd
31, 2eqeltri 2821 . . 3 𝐺 ∈ CMnd
4 ovex 7434 . . . 4 (0[,)+∞) ∈ V
5 xrge0slmod.2 . . . . 5 π‘Š = (𝐺 β†Ύv (0[,)+∞))
65resvcmn 32923 . . . 4 ((0[,)+∞) ∈ V β†’ (𝐺 ∈ CMnd ↔ π‘Š ∈ CMnd))
74, 6ax-mp 5 . . 3 (𝐺 ∈ CMnd ↔ π‘Š ∈ CMnd)
83, 7mpbi 229 . 2 π‘Š ∈ CMnd
9 rge0srg 21300 . 2 (β„‚fld β†Ύs (0[,)+∞)) ∈ SRing
10 icossicc 13410 . . . . . . . 8 (0[,)+∞) βŠ† (0[,]+∞)
11 simplr 766 . . . . . . . 8 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ π‘Ÿ ∈ (0[,)+∞))
1210, 11sselid 3972 . . . . . . 7 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ π‘Ÿ ∈ (0[,]+∞))
13 simprr 770 . . . . . . 7 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ 𝑀 ∈ (0[,]+∞))
14 ge0xmulcl 13437 . . . . . . 7 ((π‘Ÿ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞)) β†’ (π‘Ÿ Β·e 𝑀) ∈ (0[,]+∞))
1512, 13, 14syl2anc 583 . . . . . 6 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ (π‘Ÿ Β·e 𝑀) ∈ (0[,]+∞))
16 simprl 768 . . . . . . 7 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ π‘₯ ∈ (0[,]+∞))
17 xrge0adddi 32659 . . . . . . 7 ((𝑀 ∈ (0[,]+∞) ∧ π‘₯ ∈ (0[,]+∞) ∧ π‘Ÿ ∈ (0[,]+∞)) β†’ (π‘Ÿ Β·e (𝑀 +𝑒 π‘₯)) = ((π‘Ÿ Β·e 𝑀) +𝑒 (π‘Ÿ Β·e π‘₯)))
1813, 16, 12, 17syl3anc 1368 . . . . . 6 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ (π‘Ÿ Β·e (𝑀 +𝑒 π‘₯)) = ((π‘Ÿ Β·e 𝑀) +𝑒 (π‘Ÿ Β·e π‘₯)))
19 rge0ssre 13430 . . . . . . . . . 10 (0[,)+∞) βŠ† ℝ
20 simpll 764 . . . . . . . . . 10 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ π‘ž ∈ (0[,)+∞))
2119, 20sselid 3972 . . . . . . . . 9 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ π‘ž ∈ ℝ)
2219, 11sselid 3972 . . . . . . . . 9 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ π‘Ÿ ∈ ℝ)
23 rexadd 13208 . . . . . . . . 9 ((π‘ž ∈ ℝ ∧ π‘Ÿ ∈ ℝ) β†’ (π‘ž +𝑒 π‘Ÿ) = (π‘ž + π‘Ÿ))
2421, 22, 23syl2anc 583 . . . . . . . 8 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ (π‘ž +𝑒 π‘Ÿ) = (π‘ž + π‘Ÿ))
2524oveq1d 7416 . . . . . . 7 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ ((π‘ž +𝑒 π‘Ÿ) Β·e 𝑀) = ((π‘ž + π‘Ÿ) Β·e 𝑀))
2610, 20sselid 3972 . . . . . . . 8 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ π‘ž ∈ (0[,]+∞))
27 xrge0adddir 32658 . . . . . . . 8 ((π‘ž ∈ (0[,]+∞) ∧ π‘Ÿ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞)) β†’ ((π‘ž +𝑒 π‘Ÿ) Β·e 𝑀) = ((π‘ž Β·e 𝑀) +𝑒 (π‘Ÿ Β·e 𝑀)))
2826, 12, 13, 27syl3anc 1368 . . . . . . 7 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ ((π‘ž +𝑒 π‘Ÿ) Β·e 𝑀) = ((π‘ž Β·e 𝑀) +𝑒 (π‘Ÿ Β·e 𝑀)))
2925, 28eqtr3d 2766 . . . . . 6 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ ((π‘ž + π‘Ÿ) Β·e 𝑀) = ((π‘ž Β·e 𝑀) +𝑒 (π‘Ÿ Β·e 𝑀)))
3015, 18, 293jca 1125 . . . . 5 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ ((π‘Ÿ Β·e 𝑀) ∈ (0[,]+∞) ∧ (π‘Ÿ Β·e (𝑀 +𝑒 π‘₯)) = ((π‘Ÿ Β·e 𝑀) +𝑒 (π‘Ÿ Β·e π‘₯)) ∧ ((π‘ž + π‘Ÿ) Β·e 𝑀) = ((π‘ž Β·e 𝑀) +𝑒 (π‘Ÿ Β·e 𝑀))))
31 rexmul 13247 . . . . . . . . 9 ((π‘ž ∈ ℝ ∧ π‘Ÿ ∈ ℝ) β†’ (π‘ž Β·e π‘Ÿ) = (π‘ž Β· π‘Ÿ))
3221, 22, 31syl2anc 583 . . . . . . . 8 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ (π‘ž Β·e π‘Ÿ) = (π‘ž Β· π‘Ÿ))
3332oveq1d 7416 . . . . . . 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 3972 . . . . . . . 8 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ 𝑀 ∈ ℝ*)
38 xmulass 13263 . . . . . . . 8 ((π‘ž ∈ ℝ* ∧ π‘Ÿ ∈ ℝ* ∧ 𝑀 ∈ ℝ*) β†’ ((π‘ž Β·e π‘Ÿ) Β·e 𝑀) = (π‘ž Β·e (π‘Ÿ Β·e 𝑀)))
3934, 35, 37, 38syl3anc 1368 . . . . . . 7 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ ((π‘ž Β·e π‘Ÿ) Β·e 𝑀) = (π‘ž Β·e (π‘Ÿ Β·e 𝑀)))
4033, 39eqtr3d 2766 . . . . . 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 1125 . . . . 5 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ (((π‘ž Β· π‘Ÿ) Β·e 𝑀) = (π‘ž Β·e (π‘Ÿ Β·e 𝑀)) ∧ (1 Β·e 𝑀) = 𝑀 ∧ (0 Β·e 𝑀) = 0))
4630, 45jca 511 . . . 4 (((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) ∧ (π‘₯ ∈ (0[,]+∞) ∧ 𝑀 ∈ (0[,]+∞))) β†’ (((π‘Ÿ Β·e 𝑀) ∈ (0[,]+∞) ∧ (π‘Ÿ Β·e (𝑀 +𝑒 π‘₯)) = ((π‘Ÿ Β·e 𝑀) +𝑒 (π‘Ÿ Β·e π‘₯)) ∧ ((π‘ž + π‘Ÿ) Β·e 𝑀) = ((π‘ž Β·e 𝑀) +𝑒 (π‘Ÿ Β·e 𝑀))) ∧ (((π‘ž Β· π‘Ÿ) Β·e 𝑀) = (π‘ž Β·e (π‘Ÿ Β·e 𝑀)) ∧ (1 Β·e 𝑀) = 𝑀 ∧ (0 Β·e 𝑀) = 0)))
4746ralrimivva 3192 . . 3 ((π‘ž ∈ (0[,)+∞) ∧ π‘Ÿ ∈ (0[,)+∞)) β†’ βˆ€π‘₯ ∈ (0[,]+∞)βˆ€π‘€ ∈ (0[,]+∞)(((π‘Ÿ Β·e 𝑀) ∈ (0[,]+∞) ∧ (π‘Ÿ Β·e (𝑀 +𝑒 π‘₯)) = ((π‘Ÿ Β·e 𝑀) +𝑒 (π‘Ÿ Β·e π‘₯)) ∧ ((π‘ž + π‘Ÿ) Β·e 𝑀) = ((π‘ž Β·e 𝑀) +𝑒 (π‘Ÿ Β·e 𝑀))) ∧ (((π‘ž Β· π‘Ÿ) Β·e 𝑀) = (π‘ž Β·e (π‘Ÿ Β·e 𝑀)) ∧ (1 Β·e 𝑀) = 𝑀 ∧ (0 Β·e 𝑀) = 0)))
4847rgen2 3189 . 2 βˆ€π‘ž ∈ (0[,)+∞)βˆ€π‘Ÿ ∈ (0[,)+∞)βˆ€π‘₯ ∈ (0[,]+∞)βˆ€π‘€ ∈ (0[,]+∞)(((π‘Ÿ Β·e 𝑀) ∈ (0[,]+∞) ∧ (π‘Ÿ Β·e (𝑀 +𝑒 π‘₯)) = ((π‘Ÿ Β·e 𝑀) +𝑒 (π‘Ÿ Β·e π‘₯)) ∧ ((π‘ž + π‘Ÿ) Β·e 𝑀) = ((π‘ž Β·e 𝑀) +𝑒 (π‘Ÿ Β·e 𝑀))) ∧ (((π‘ž Β· π‘Ÿ) Β·e 𝑀) = (π‘ž Β·e (π‘Ÿ Β·e 𝑀)) ∧ (1 Β·e 𝑀) = 𝑀 ∧ (0 Β·e 𝑀) = 0))
49 xrge0base 32651 . . . . . 6 (0[,]+∞) = (Baseβ€˜(ℝ*𝑠 β†Ύs (0[,]+∞)))
501fveq2i 6884 . . . . . 6 (Baseβ€˜πΊ) = (Baseβ€˜(ℝ*𝑠 β†Ύs (0[,]+∞)))
5149, 50eqtr4i 2755 . . . . 5 (0[,]+∞) = (Baseβ€˜πΊ)
525, 51resvbas 32913 . . . 4 ((0[,)+∞) ∈ V β†’ (0[,]+∞) = (Baseβ€˜π‘Š))
534, 52ax-mp 5 . . 3 (0[,]+∞) = (Baseβ€˜π‘Š)
54 xrge0plusg 32653 . . . . . 6 +𝑒 = (+gβ€˜(ℝ*𝑠 β†Ύs (0[,]+∞)))
551fveq2i 6884 . . . . . 6 (+gβ€˜πΊ) = (+gβ€˜(ℝ*𝑠 β†Ύs (0[,]+∞)))
5654, 55eqtr4i 2755 . . . . 5 +𝑒 = (+gβ€˜πΊ)
575, 56resvplusg 32915 . . . 4 ((0[,)+∞) ∈ V β†’ +𝑒 = (+gβ€˜π‘Š))
584, 57ax-mp 5 . . 3 +𝑒 = (+gβ€˜π‘Š)
59 ovex 7434 . . . . . 6 (0[,]+∞) ∈ V
60 ax-xrsvsca 32642 . . . . . . 7 Β·e = ( ·𝑠 β€˜β„*𝑠)
611, 60ressvsca 17288 . . . . . 6 ((0[,]+∞) ∈ V β†’ Β·e = ( ·𝑠 β€˜πΊ))
6259, 61ax-mp 5 . . . . 5 Β·e = ( ·𝑠 β€˜πΊ)
635, 62resvvsca 32917 . . . 4 ((0[,)+∞) ∈ V β†’ Β·e = ( ·𝑠 β€˜π‘Š))
644, 63ax-mp 5 . . 3 Β·e = ( ·𝑠 β€˜π‘Š)
65 xrge00 32652 . . . . . 6 0 = (0gβ€˜(ℝ*𝑠 β†Ύs (0[,]+∞)))
661fveq2i 6884 . . . . . 6 (0gβ€˜πΊ) = (0gβ€˜(ℝ*𝑠 β†Ύs (0[,]+∞)))
6765, 66eqtr4i 2755 . . . . 5 0 = (0gβ€˜πΊ)
685, 67resv0g 32921 . . . 4 ((0[,)+∞) ∈ V β†’ 0 = (0gβ€˜π‘Š))
694, 68ax-mp 5 . . 3 0 = (0gβ€˜π‘Š)
70 df-refld 21466 . . . . . 6 ℝfld = (β„‚fld β†Ύs ℝ)
7170oveq1i 7411 . . . . 5 (ℝfld β†Ύs (0[,)+∞)) = ((β„‚fld β†Ύs ℝ) β†Ύs (0[,)+∞))
72 reex 11197 . . . . . 6 ℝ ∈ V
73 ressress 17192 . . . . . 6 ((ℝ ∈ V ∧ (0[,)+∞) ∈ V) β†’ ((β„‚fld β†Ύs ℝ) β†Ύs (0[,)+∞)) = (β„‚fld β†Ύs (ℝ ∩ (0[,)+∞))))
7472, 4, 73mp2an 689 . . . . 5 ((β„‚fld β†Ύs ℝ) β†Ύs (0[,)+∞)) = (β„‚fld β†Ύs (ℝ ∩ (0[,)+∞)))
7571, 74eqtri 2752 . . . 4 (ℝfld β†Ύs (0[,)+∞)) = (β„‚fld β†Ύs (ℝ ∩ (0[,)+∞)))
76 ax-xrssca 32641 . . . . . . . 8 ℝfld = (Scalarβ€˜β„*𝑠)
771, 76resssca 17287 . . . . . . 7 ((0[,]+∞) ∈ V β†’ ℝfld = (Scalarβ€˜πΊ))
7859, 77ax-mp 5 . . . . . 6 ℝfld = (Scalarβ€˜πΊ)
79 rebase 21467 . . . . . 6 ℝ = (Baseβ€˜β„fld)
805, 78, 79resvsca 32910 . . . . 5 ((0[,)+∞) ∈ V β†’ (ℝfld β†Ύs (0[,)+∞)) = (Scalarβ€˜π‘Š))
814, 80ax-mp 5 . . . 4 (ℝfld β†Ύs (0[,)+∞)) = (Scalarβ€˜π‘Š)
82 incom 4193 . . . . . 6 ((0[,)+∞) ∩ ℝ) = (ℝ ∩ (0[,)+∞))
83 df-ss 3957 . . . . . . 7 ((0[,)+∞) βŠ† ℝ ↔ ((0[,)+∞) ∩ ℝ) = (0[,)+∞))
8419, 83mpbi 229 . . . . . 6 ((0[,)+∞) ∩ ℝ) = (0[,)+∞)
8582, 84eqtr3i 2754 . . . . 5 (ℝ ∩ (0[,)+∞)) = (0[,)+∞)
8685oveq2i 7412 . . . 4 (β„‚fld β†Ύs (ℝ ∩ (0[,)+∞))) = (β„‚fld β†Ύs (0[,)+∞))
8775, 81, 863eqtr3ri 2761 . . 3 (β„‚fld β†Ύs (0[,)+∞)) = (Scalarβ€˜π‘Š)
88 ax-resscn 11163 . . . . 5 ℝ βŠ† β„‚
8919, 88sstri 3983 . . . 4 (0[,)+∞) βŠ† β„‚
90 eqid 2724 . . . . 5 (β„‚fld β†Ύs (0[,)+∞)) = (β„‚fld β†Ύs (0[,)+∞))
91 cnfldbas 21232 . . . . 5 β„‚ = (Baseβ€˜β„‚fld)
9290, 91ressbas2 17181 . . . 4 ((0[,)+∞) βŠ† β„‚ β†’ (0[,)+∞) = (Baseβ€˜(β„‚fld β†Ύs (0[,)+∞))))
9389, 92ax-mp 5 . . 3 (0[,)+∞) = (Baseβ€˜(β„‚fld β†Ύs (0[,)+∞)))
94 cnfldadd 21233 . . . . 5 + = (+gβ€˜β„‚fld)
9590, 94ressplusg 17234 . . . 4 ((0[,)+∞) ∈ V β†’ + = (+gβ€˜(β„‚fld β†Ύs (0[,)+∞))))
964, 95ax-mp 5 . . 3 + = (+gβ€˜(β„‚fld β†Ύs (0[,)+∞)))
97 cnfldmul 21234 . . . . 5 Β· = (.rβ€˜β„‚fld)
9890, 97ressmulr 17251 . . . 4 ((0[,)+∞) ∈ V β†’ Β· = (.rβ€˜(β„‚fld β†Ύs (0[,)+∞))))
994, 98ax-mp 5 . . 3 Β· = (.rβ€˜(β„‚fld β†Ύs (0[,)+∞)))
100 cndrng 21258 . . . . 5 β„‚fld ∈ DivRing
101 drngring 20584 . . . . 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 1336 . . . . 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 689 . . . . 5 (1 ∈ (0[,)+∞) ↔ (1 ∈ ℝ ∧ 0 ≀ 1 ∧ 1 < +∞))
112107, 111mpbir 230 . . . 4 1 ∈ (0[,)+∞)
113 cnfld1 21254 . . . . 5 1 = (1rβ€˜β„‚fld)
11490, 91, 113ress1r 32849 . . . 4 ((β„‚fld ∈ Ring ∧ 1 ∈ (0[,)+∞) ∧ (0[,)+∞) βŠ† β„‚) β†’ 1 = (1rβ€˜(β„‚fld β†Ύs (0[,)+∞))))
115102, 112, 89, 114mp3an 1457 . . 3 1 = (1rβ€˜(β„‚fld β†Ύs (0[,)+∞)))
116 ringmnd 20138 . . . . 5 (β„‚fld ∈ Ring β†’ β„‚fld ∈ Mnd)
117100, 101, 116mp2b 10 . . . 4 β„‚fld ∈ Mnd
118 0e0icopnf 13432 . . . 4 0 ∈ (0[,)+∞)
119 cnfld0 21253 . . . . 5 0 = (0gβ€˜β„‚fld)
12090, 91, 119ress0g 18685 . . . 4 ((β„‚fld ∈ Mnd ∧ 0 ∈ (0[,)+∞) ∧ (0[,)+∞) βŠ† β„‚) β†’ 0 = (0gβ€˜(β„‚fld β†Ύs (0[,)+∞))))
121117, 118, 89, 120mp3an 1457 . . 3 0 = (0gβ€˜(β„‚fld β†Ύs (0[,)+∞)))
12253, 58, 64, 69, 87, 93, 96, 99, 115, 121isslmd 32815 . 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 1338 1 π‘Š ∈ SLMod
Colors of variables: wff setvar class
Syntax hints:   ↔ wb 205   ∧ wa 395   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  βˆ€wral 3053  Vcvv 3466   ∩ cin 3939   βŠ† wss 3940   class class class wbr 5138  β€˜cfv 6533  (class class class)co 7401  β„‚cc 11104  β„cr 11105  0cc0 11106  1c1 11107   + caddc 11109   Β· cmul 11111  +∞cpnf 11242  β„*cxr 11244   < clt 11245   ≀ cle 11246   +𝑒 cxad 13087   Β·e cxmu 13088  [,)cico 13323  [,]cicc 13324  Basecbs 17143   β†Ύs cress 17172  +gcplusg 17196  .rcmulr 17197  Scalarcsca 17199   ·𝑠 cvsca 17200  0gc0g 17384  β„*𝑠cxrs 17445  Mndcmnd 18657  CMndccmn 19690  1rcur 20076  SRingcsrg 20081  Ringcrg 20128  DivRingcdr 20577  β„‚fldccnfld 21228  β„fldcrefld 21465  SLModcslmd 32813   β†Ύv cresv 32904
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-addf 11185  ax-mulf 11186  ax-xrssca 32641  ax-xrsvsca 32642
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-pss 3959  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-tp 4625  df-op 4627  df-uni 4900  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-tr 5256  df-id 5564  df-eprel 5570  df-po 5578  df-so 5579  df-fr 5621  df-we 5623  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7357  df-ov 7404  df-oprab 7405  df-mpo 7406  df-om 7849  df-1st 7968  df-2nd 7969  df-tpos 8206  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-1o 8461  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  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 17079  df-sets 17096  df-slot 17114  df-ndx 17126  df-base 17144  df-ress 17173  df-plusg 17209  df-mulr 17210  df-starv 17211  df-sca 17212  df-vsca 17213  df-tset 17215  df-ple 17216  df-ds 17218  df-unif 17219  df-0g 17386  df-xrs 17447  df-mgm 18563  df-sgrp 18642  df-mnd 18658  df-submnd 18704  df-grp 18856  df-minusg 18857  df-cmn 19692  df-abl 19693  df-mgp 20030  df-rng 20048  df-ur 20077  df-srg 20082  df-ring 20130  df-cring 20131  df-oppr 20226  df-dvdsr 20249  df-unit 20250  df-invr 20280  df-dvr 20293  df-drng 20579  df-cnfld 21229  df-refld 21466  df-slmd 32814  df-resv 32905
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator