Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  xrge0slmod Structured version   Visualization version   GIF version

Theorem xrge0slmod 29175
 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 19607 . . . 4 (ℝ*𝑠s (0[,]+∞)) ∈ CMnd
31, 2eqeltri 2684 . . 3 𝐺 ∈ CMnd
4 ovex 6577 . . . 4 (0[,)+∞) ∈ V
5 xrge0slmod.2 . . . . 5 𝑊 = (𝐺v (0[,)+∞))
65resvcmn 29169 . . . 4 ((0[,)+∞) ∈ V → (𝐺 ∈ CMnd ↔ 𝑊 ∈ CMnd))
74, 6ax-mp 5 . . 3 (𝐺 ∈ CMnd ↔ 𝑊 ∈ CMnd)
83, 7mpbi 219 . 2 𝑊 ∈ CMnd
9 rge0srg 19636 . 2 (ℂflds (0[,)+∞)) ∈ SRing
10 icossicc 12131 . . . . . . . 8 (0[,)+∞) ⊆ (0[,]+∞)
11 simplr 788 . . . . . . . 8 (((𝑞 ∈ (0[,)+∞) ∧ 𝑟 ∈ (0[,)+∞)) ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑤 ∈ (0[,]+∞))) → 𝑟 ∈ (0[,)+∞))
1210, 11sseldi 3566 . . . . . . 7 (((𝑞 ∈ (0[,)+∞) ∧ 𝑟 ∈ (0[,)+∞)) ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑤 ∈ (0[,]+∞))) → 𝑟 ∈ (0[,]+∞))
13 simprr 792 . . . . . . 7 (((𝑞 ∈ (0[,)+∞) ∧ 𝑟 ∈ (0[,)+∞)) ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑤 ∈ (0[,]+∞))) → 𝑤 ∈ (0[,]+∞))
14 ge0xmulcl 12158 . . . . . . 7 ((𝑟 ∈ (0[,]+∞) ∧ 𝑤 ∈ (0[,]+∞)) → (𝑟 ·e 𝑤) ∈ (0[,]+∞))
1512, 13, 14syl2anc 691 . . . . . 6 (((𝑞 ∈ (0[,)+∞) ∧ 𝑟 ∈ (0[,)+∞)) ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑤 ∈ (0[,]+∞))) → (𝑟 ·e 𝑤) ∈ (0[,]+∞))
16 simprl 790 . . . . . . 7 (((𝑞 ∈ (0[,)+∞) ∧ 𝑟 ∈ (0[,)+∞)) ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑤 ∈ (0[,]+∞))) → 𝑥 ∈ (0[,]+∞))
17 xrge0adddi 29024 . . . . . . 7 ((𝑤 ∈ (0[,]+∞) ∧ 𝑥 ∈ (0[,]+∞) ∧ 𝑟 ∈ (0[,]+∞)) → (𝑟 ·e (𝑤 +𝑒 𝑥)) = ((𝑟 ·e 𝑤) +𝑒 (𝑟 ·e 𝑥)))
1813, 16, 12, 17syl3anc 1318 . . . . . 6 (((𝑞 ∈ (0[,)+∞) ∧ 𝑟 ∈ (0[,)+∞)) ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑤 ∈ (0[,]+∞))) → (𝑟 ·e (𝑤 +𝑒 𝑥)) = ((𝑟 ·e 𝑤) +𝑒 (𝑟 ·e 𝑥)))
19 rge0ssre 12151 . . . . . . . . . 10 (0[,)+∞) ⊆ ℝ
20 simpll 786 . . . . . . . . . 10 (((𝑞 ∈ (0[,)+∞) ∧ 𝑟 ∈ (0[,)+∞)) ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑤 ∈ (0[,]+∞))) → 𝑞 ∈ (0[,)+∞))
2119, 20sseldi 3566 . . . . . . . . 9 (((𝑞 ∈ (0[,)+∞) ∧ 𝑟 ∈ (0[,)+∞)) ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑤 ∈ (0[,]+∞))) → 𝑞 ∈ ℝ)
2219, 11sseldi 3566 . . . . . . . . 9 (((𝑞 ∈ (0[,)+∞) ∧ 𝑟 ∈ (0[,)+∞)) ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑤 ∈ (0[,]+∞))) → 𝑟 ∈ ℝ)
23 rexadd 11937 . . . . . . . . 9 ((𝑞 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (𝑞 +𝑒 𝑟) = (𝑞 + 𝑟))
2421, 22, 23syl2anc 691 . . . . . . . 8 (((𝑞 ∈ (0[,)+∞) ∧ 𝑟 ∈ (0[,)+∞)) ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑤 ∈ (0[,]+∞))) → (𝑞 +𝑒 𝑟) = (𝑞 + 𝑟))
2524oveq1d 6564 . . . . . . 7 (((𝑞 ∈ (0[,)+∞) ∧ 𝑟 ∈ (0[,)+∞)) ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑤 ∈ (0[,]+∞))) → ((𝑞 +𝑒 𝑟) ·e 𝑤) = ((𝑞 + 𝑟) ·e 𝑤))
2610, 20sseldi 3566 . . . . . . . 8 (((𝑞 ∈ (0[,)+∞) ∧ 𝑟 ∈ (0[,)+∞)) ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑤 ∈ (0[,]+∞))) → 𝑞 ∈ (0[,]+∞))
27 xrge0adddir 29023 . . . . . . . 8 ((𝑞 ∈ (0[,]+∞) ∧ 𝑟 ∈ (0[,]+∞) ∧ 𝑤 ∈ (0[,]+∞)) → ((𝑞 +𝑒 𝑟) ·e 𝑤) = ((𝑞 ·e 𝑤) +𝑒 (𝑟 ·e 𝑤)))
2826, 12, 13, 27syl3anc 1318 . . . . . . 7 (((𝑞 ∈ (0[,)+∞) ∧ 𝑟 ∈ (0[,)+∞)) ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑤 ∈ (0[,]+∞))) → ((𝑞 +𝑒 𝑟) ·e 𝑤) = ((𝑞 ·e 𝑤) +𝑒 (𝑟 ·e 𝑤)))
2925, 28eqtr3d 2646 . . . . . 6 (((𝑞 ∈ (0[,)+∞) ∧ 𝑟 ∈ (0[,)+∞)) ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑤 ∈ (0[,]+∞))) → ((𝑞 + 𝑟) ·e 𝑤) = ((𝑞 ·e 𝑤) +𝑒 (𝑟 ·e 𝑤)))
3015, 18, 293jca 1235 . . . . 5 (((𝑞 ∈ (0[,)+∞) ∧ 𝑟 ∈ (0[,)+∞)) ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑤 ∈ (0[,]+∞))) → ((𝑟 ·e 𝑤) ∈ (0[,]+∞) ∧ (𝑟 ·e (𝑤 +𝑒 𝑥)) = ((𝑟 ·e 𝑤) +𝑒 (𝑟 ·e 𝑥)) ∧ ((𝑞 + 𝑟) ·e 𝑤) = ((𝑞 ·e 𝑤) +𝑒 (𝑟 ·e 𝑤))))
31 rexmul 11973 . . . . . . . . 9 ((𝑞 ∈ ℝ ∧ 𝑟 ∈ ℝ) → (𝑞 ·e 𝑟) = (𝑞 · 𝑟))
3221, 22, 31syl2anc 691 . . . . . . . 8 (((𝑞 ∈ (0[,)+∞) ∧ 𝑟 ∈ (0[,)+∞)) ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑤 ∈ (0[,]+∞))) → (𝑞 ·e 𝑟) = (𝑞 · 𝑟))
3332oveq1d 6564 . . . . . . 7 (((𝑞 ∈ (0[,)+∞) ∧ 𝑟 ∈ (0[,)+∞)) ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑤 ∈ (0[,]+∞))) → ((𝑞 ·e 𝑟) ·e 𝑤) = ((𝑞 · 𝑟) ·e 𝑤))
3421rexrd 9968 . . . . . . . 8 (((𝑞 ∈ (0[,)+∞) ∧ 𝑟 ∈ (0[,)+∞)) ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑤 ∈ (0[,]+∞))) → 𝑞 ∈ ℝ*)
3522rexrd 9968 . . . . . . . 8 (((𝑞 ∈ (0[,)+∞) ∧ 𝑟 ∈ (0[,)+∞)) ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑤 ∈ (0[,]+∞))) → 𝑟 ∈ ℝ*)
36 iccssxr 12127 . . . . . . . . 9 (0[,]+∞) ⊆ ℝ*
3736, 13sseldi 3566 . . . . . . . 8 (((𝑞 ∈ (0[,)+∞) ∧ 𝑟 ∈ (0[,)+∞)) ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑤 ∈ (0[,]+∞))) → 𝑤 ∈ ℝ*)
38 xmulass 11989 . . . . . . . 8 ((𝑞 ∈ ℝ*𝑟 ∈ ℝ*𝑤 ∈ ℝ*) → ((𝑞 ·e 𝑟) ·e 𝑤) = (𝑞 ·e (𝑟 ·e 𝑤)))
3934, 35, 37, 38syl3anc 1318 . . . . . . 7 (((𝑞 ∈ (0[,)+∞) ∧ 𝑟 ∈ (0[,)+∞)) ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑤 ∈ (0[,]+∞))) → ((𝑞 ·e 𝑟) ·e 𝑤) = (𝑞 ·e (𝑟 ·e 𝑤)))
4033, 39eqtr3d 2646 . . . . . 6 (((𝑞 ∈ (0[,)+∞) ∧ 𝑟 ∈ (0[,)+∞)) ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑤 ∈ (0[,]+∞))) → ((𝑞 · 𝑟) ·e 𝑤) = (𝑞 ·e (𝑟 ·e 𝑤)))
41 xmulid2 11982 . . . . . . 7 (𝑤 ∈ ℝ* → (1 ·e 𝑤) = 𝑤)
4237, 41syl 17 . . . . . 6 (((𝑞 ∈ (0[,)+∞) ∧ 𝑟 ∈ (0[,)+∞)) ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑤 ∈ (0[,]+∞))) → (1 ·e 𝑤) = 𝑤)
43 xmul02 11970 . . . . . . 7 (𝑤 ∈ ℝ* → (0 ·e 𝑤) = 0)
4437, 43syl 17 . . . . . 6 (((𝑞 ∈ (0[,)+∞) ∧ 𝑟 ∈ (0[,)+∞)) ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑤 ∈ (0[,]+∞))) → (0 ·e 𝑤) = 0)
4540, 42, 443jca 1235 . . . . 5 (((𝑞 ∈ (0[,)+∞) ∧ 𝑟 ∈ (0[,)+∞)) ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑤 ∈ (0[,]+∞))) → (((𝑞 · 𝑟) ·e 𝑤) = (𝑞 ·e (𝑟 ·e 𝑤)) ∧ (1 ·e 𝑤) = 𝑤 ∧ (0 ·e 𝑤) = 0))
4630, 45jca 553 . . . 4 (((𝑞 ∈ (0[,)+∞) ∧ 𝑟 ∈ (0[,)+∞)) ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑤 ∈ (0[,]+∞))) → (((𝑟 ·e 𝑤) ∈ (0[,]+∞) ∧ (𝑟 ·e (𝑤 +𝑒 𝑥)) = ((𝑟 ·e 𝑤) +𝑒 (𝑟 ·e 𝑥)) ∧ ((𝑞 + 𝑟) ·e 𝑤) = ((𝑞 ·e 𝑤) +𝑒 (𝑟 ·e 𝑤))) ∧ (((𝑞 · 𝑟) ·e 𝑤) = (𝑞 ·e (𝑟 ·e 𝑤)) ∧ (1 ·e 𝑤) = 𝑤 ∧ (0 ·e 𝑤) = 0)))
4746ralrimivva 2954 . . 3 ((𝑞 ∈ (0[,)+∞) ∧ 𝑟 ∈ (0[,)+∞)) → ∀𝑥 ∈ (0[,]+∞)∀𝑤 ∈ (0[,]+∞)(((𝑟 ·e 𝑤) ∈ (0[,]+∞) ∧ (𝑟 ·e (𝑤 +𝑒 𝑥)) = ((𝑟 ·e 𝑤) +𝑒 (𝑟 ·e 𝑥)) ∧ ((𝑞 + 𝑟) ·e 𝑤) = ((𝑞 ·e 𝑤) +𝑒 (𝑟 ·e 𝑤))) ∧ (((𝑞 · 𝑟) ·e 𝑤) = (𝑞 ·e (𝑟 ·e 𝑤)) ∧ (1 ·e 𝑤) = 𝑤 ∧ (0 ·e 𝑤) = 0)))
4847rgen2a 2960 . 2 𝑞 ∈ (0[,)+∞)∀𝑟 ∈ (0[,)+∞)∀𝑥 ∈ (0[,]+∞)∀𝑤 ∈ (0[,]+∞)(((𝑟 ·e 𝑤) ∈ (0[,]+∞) ∧ (𝑟 ·e (𝑤 +𝑒 𝑥)) = ((𝑟 ·e 𝑤) +𝑒 (𝑟 ·e 𝑥)) ∧ ((𝑞 + 𝑟) ·e 𝑤) = ((𝑞 ·e 𝑤) +𝑒 (𝑟 ·e 𝑤))) ∧ (((𝑞 · 𝑟) ·e 𝑤) = (𝑞 ·e (𝑟 ·e 𝑤)) ∧ (1 ·e 𝑤) = 𝑤 ∧ (0 ·e 𝑤) = 0))
49 xrge0base 29016 . . . . . 6 (0[,]+∞) = (Base‘(ℝ*𝑠s (0[,]+∞)))
501fveq2i 6106 . . . . . 6 (Base‘𝐺) = (Base‘(ℝ*𝑠s (0[,]+∞)))
5149, 50eqtr4i 2635 . . . . 5 (0[,]+∞) = (Base‘𝐺)
525, 51resvbas 29163 . . . 4 ((0[,)+∞) ∈ V → (0[,]+∞) = (Base‘𝑊))
534, 52ax-mp 5 . . 3 (0[,]+∞) = (Base‘𝑊)
54 xrge0plusg 29018 . . . . . 6 +𝑒 = (+g‘(ℝ*𝑠s (0[,]+∞)))
551fveq2i 6106 . . . . . 6 (+g𝐺) = (+g‘(ℝ*𝑠s (0[,]+∞)))
5654, 55eqtr4i 2635 . . . . 5 +𝑒 = (+g𝐺)
575, 56resvplusg 29164 . . . 4 ((0[,)+∞) ∈ V → +𝑒 = (+g𝑊))
584, 57ax-mp 5 . . 3 +𝑒 = (+g𝑊)
59 ovex 6577 . . . . . 6 (0[,]+∞) ∈ V
60 ax-xrsvsca 29005 . . . . . . 7 ·e = ( ·𝑠 ‘ℝ*𝑠)
611, 60ressvsca 15855 . . . . . 6 ((0[,]+∞) ∈ V → ·e = ( ·𝑠𝐺))
6259, 61ax-mp 5 . . . . 5 ·e = ( ·𝑠𝐺)
635, 62resvvsca 29165 . . . 4 ((0[,)+∞) ∈ V → ·e = ( ·𝑠𝑊))
644, 63ax-mp 5 . . 3 ·e = ( ·𝑠𝑊)
65 xrge00 29017 . . . . . 6 0 = (0g‘(ℝ*𝑠s (0[,]+∞)))
661fveq2i 6106 . . . . . 6 (0g𝐺) = (0g‘(ℝ*𝑠s (0[,]+∞)))
6765, 66eqtr4i 2635 . . . . 5 0 = (0g𝐺)
685, 67resv0g 29167 . . . 4 ((0[,)+∞) ∈ V → 0 = (0g𝑊))
694, 68ax-mp 5 . . 3 0 = (0g𝑊)
70 df-refld 19770 . . . . . 6 fld = (ℂflds ℝ)
7170oveq1i 6559 . . . . 5 (ℝflds (0[,)+∞)) = ((ℂflds ℝ) ↾s (0[,)+∞))
72 reex 9906 . . . . . 6 ℝ ∈ V
73 ressress 15765 . . . . . 6 ((ℝ ∈ V ∧ (0[,)+∞) ∈ V) → ((ℂflds ℝ) ↾s (0[,)+∞)) = (ℂflds (ℝ ∩ (0[,)+∞))))
7472, 4, 73mp2an 704 . . . . 5 ((ℂflds ℝ) ↾s (0[,)+∞)) = (ℂflds (ℝ ∩ (0[,)+∞)))
7571, 74eqtri 2632 . . . 4 (ℝflds (0[,)+∞)) = (ℂflds (ℝ ∩ (0[,)+∞)))
76 ax-xrssca 29004 . . . . . . . 8 fld = (Scalar‘ℝ*𝑠)
771, 76resssca 15854 . . . . . . 7 ((0[,]+∞) ∈ V → ℝfld = (Scalar‘𝐺))
7859, 77ax-mp 5 . . . . . 6 fld = (Scalar‘𝐺)
79 rebase 19771 . . . . . 6 ℝ = (Base‘ℝfld)
805, 78, 79resvsca 29161 . . . . 5 ((0[,)+∞) ∈ V → (ℝflds (0[,)+∞)) = (Scalar‘𝑊))
814, 80ax-mp 5 . . . 4 (ℝflds (0[,)+∞)) = (Scalar‘𝑊)
82 incom 3767 . . . . . 6 ((0[,)+∞) ∩ ℝ) = (ℝ ∩ (0[,)+∞))
83 df-ss 3554 . . . . . . 7 ((0[,)+∞) ⊆ ℝ ↔ ((0[,)+∞) ∩ ℝ) = (0[,)+∞))
8419, 83mpbi 219 . . . . . 6 ((0[,)+∞) ∩ ℝ) = (0[,)+∞)
8582, 84eqtr3i 2634 . . . . 5 (ℝ ∩ (0[,)+∞)) = (0[,)+∞)
8685oveq2i 6560 . . . 4 (ℂflds (ℝ ∩ (0[,)+∞))) = (ℂflds (0[,)+∞))
8775, 81, 863eqtr3ri 2641 . . 3 (ℂflds (0[,)+∞)) = (Scalar‘𝑊)
88 ax-resscn 9872 . . . . 5 ℝ ⊆ ℂ
8919, 88sstri 3577 . . . 4 (0[,)+∞) ⊆ ℂ
90 eqid 2610 . . . . 5 (ℂflds (0[,)+∞)) = (ℂflds (0[,)+∞))
91 cnfldbas 19571 . . . . 5 ℂ = (Base‘ℂfld)
9290, 91ressbas2 15758 . . . 4 ((0[,)+∞) ⊆ ℂ → (0[,)+∞) = (Base‘(ℂflds (0[,)+∞))))
9389, 92ax-mp 5 . . 3 (0[,)+∞) = (Base‘(ℂflds (0[,)+∞)))
94 cnfldadd 19572 . . . . 5 + = (+g‘ℂfld)
9590, 94ressplusg 15818 . . . 4 ((0[,)+∞) ∈ V → + = (+g‘(ℂflds (0[,)+∞))))
964, 95ax-mp 5 . . 3 + = (+g‘(ℂflds (0[,)+∞)))
97 cnfldmul 19573 . . . . 5 · = (.r‘ℂfld)
9890, 97ressmulr 15829 . . . 4 ((0[,)+∞) ∈ V → · = (.r‘(ℂflds (0[,)+∞))))
994, 98ax-mp 5 . . 3 · = (.r‘(ℂflds (0[,)+∞)))
100 cndrng 19594 . . . . 5 fld ∈ DivRing
101 drngring 18577 . . . . 5 (ℂfld ∈ DivRing → ℂfld ∈ Ring)
102100, 101ax-mp 5 . . . 4 fld ∈ Ring
103 1re 9918 . . . . . 6 1 ∈ ℝ
104 0le1 10430 . . . . . 6 0 ≤ 1
105 ltpnf 11830 . . . . . . 7 (1 ∈ ℝ → 1 < +∞)
106103, 105ax-mp 5 . . . . . 6 1 < +∞
107103, 104, 1063pm3.2i 1232 . . . . 5 (1 ∈ ℝ ∧ 0 ≤ 1 ∧ 1 < +∞)
108 0re 9919 . . . . . 6 0 ∈ ℝ
109 pnfxr 9971 . . . . . 6 +∞ ∈ ℝ*
110 elico2 12108 . . . . . 6 ((0 ∈ ℝ ∧ +∞ ∈ ℝ*) → (1 ∈ (0[,)+∞) ↔ (1 ∈ ℝ ∧ 0 ≤ 1 ∧ 1 < +∞)))
111108, 109, 110mp2an 704 . . . . 5 (1 ∈ (0[,)+∞) ↔ (1 ∈ ℝ ∧ 0 ≤ 1 ∧ 1 < +∞))
112107, 111mpbir 220 . . . 4 1 ∈ (0[,)+∞)
113 cnfld1 19590 . . . . 5 1 = (1r‘ℂfld)
11490, 91, 113ress1r 29120 . . . 4 ((ℂfld ∈ Ring ∧ 1 ∈ (0[,)+∞) ∧ (0[,)+∞) ⊆ ℂ) → 1 = (1r‘(ℂflds (0[,)+∞))))
115102, 112, 89, 114mp3an 1416 . . 3 1 = (1r‘(ℂflds (0[,)+∞)))
116 ringmnd 18379 . . . . 5 (ℂfld ∈ Ring → ℂfld ∈ Mnd)
117100, 101, 116mp2b 10 . . . 4 fld ∈ Mnd
118 0e0icopnf 12153 . . . 4 0 ∈ (0[,)+∞)
119 cnfld0 19589 . . . . 5 0 = (0g‘ℂfld)
12090, 91, 119ress0g 17142 . . . 4 ((ℂfld ∈ Mnd ∧ 0 ∈ (0[,)+∞) ∧ (0[,)+∞) ⊆ ℂ) → 0 = (0g‘(ℂflds (0[,)+∞))))
121117, 118, 89, 120mp3an 1416 . . 3 0 = (0g‘(ℂflds (0[,)+∞)))
12253, 58, 64, 69, 87, 93, 96, 99, 115, 121isslmd 29086 . 2 (𝑊 ∈ SLMod ↔ (𝑊 ∈ CMnd ∧ (ℂflds (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 1237 1 𝑊 ∈ SLMod
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∀wral 2896  Vcvv 3173   ∩ cin 3539   ⊆ wss 3540   class class class wbr 4583  ‘cfv 5804  (class class class)co 6549  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820  +∞cpnf 9950  ℝ*cxr 9952   < clt 9953   ≤ cle 9954   +𝑒 cxad 11820   ·e cxmu 11821  [,)cico 12048  [,]cicc 12049  Basecbs 15695   ↾s cress 15696  +gcplusg 15768  .rcmulr 15769  Scalarcsca 15771   ·𝑠 cvsca 15772  0gc0g 15923  ℝ*𝑠cxrs 15983  Mndcmnd 17117  CMndccmn 18016  1rcur 18324  SRingcsrg 18328  Ringcrg 18370  DivRingcdr 18570  ℂfldccnfld 19567  ℝfldcrefld 19769  SLModcslmd 29084   ↾v cresv 29155 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-addf 9894  ax-mulf 9895  ax-xrssca 29004  ax-xrsvsca 29005 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-tpos 7239  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-xneg 11822  df-xadd 11823  df-xmul 11824  df-ico 12052  df-icc 12053  df-fz 12198  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-mulr 15782  df-starv 15783  df-sca 15784  df-vsca 15785  df-tset 15787  df-ple 15788  df-ds 15791  df-unif 15792  df-0g 15925  df-xrs 15985  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-submnd 17159  df-grp 17248  df-minusg 17249  df-cmn 18018  df-abl 18019  df-mgp 18313  df-ur 18325  df-srg 18329  df-ring 18372  df-cring 18373  df-oppr 18446  df-dvdsr 18464  df-unit 18465  df-invr 18495  df-dvr 18506  df-drng 18572  df-cnfld 19568  df-refld 19770  df-slmd 29085  df-resv 29156 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator