Description: The scalar ring of the ordered power series structure. (Contributed by Mario Carneiro, 8-Feb-2015) (Revised by Mario Carneiro, 30-Aug-2015) (Revised by AV, 1-Nov-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | opsrbas.s | ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 ) | |
opsrbas.o | ⊢ 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 ) | ||
opsrbas.t | ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐼 × 𝐼 ) ) | ||
opsrsca.i | ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 ) | ||
opsrsca.r | ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 ) | ||
Assertion | opsrsca | ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑂 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opsrbas.s | ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 ) | |
2 | opsrbas.o | ⊢ 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 ) | |
3 | opsrbas.t | ⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐼 × 𝐼 ) ) | |
4 | opsrsca.i | ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 ) | |
5 | opsrsca.r | ⊢ ( 𝜑 → 𝑅 ∈ 𝑊 ) | |
6 | 1 4 5 | psrsca | ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑆 ) ) |
7 | scaid | ⊢ Scalar = Slot ( Scalar ‘ ndx ) | |
8 | plendxnscandx | ⊢ ( le ‘ ndx ) ≠ ( Scalar ‘ ndx ) | |
9 | 8 | necomi | ⊢ ( Scalar ‘ ndx ) ≠ ( le ‘ ndx ) |
10 | 1 2 3 7 9 | opsrbaslem | ⊢ ( 𝜑 → ( Scalar ‘ 𝑆 ) = ( Scalar ‘ 𝑂 ) ) |
11 | 6 10 | eqtrd | ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑂 ) ) |