Description: Univariate power series form a ring. (Contributed by Stefan O'Rear, 22-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | psr1ring.s | ⊢ 𝑆 = ( PwSer1 ‘ 𝑅 ) | |
Assertion | psr1ring | ⊢ ( 𝑅 ∈ Ring → 𝑆 ∈ Ring ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | psr1ring.s | ⊢ 𝑆 = ( PwSer1 ‘ 𝑅 ) | |
2 | 1 | psr1val | ⊢ 𝑆 = ( ( 1o ordPwSer 𝑅 ) ‘ ∅ ) |
3 | 1on | ⊢ 1o ∈ On | |
4 | 3 | a1i | ⊢ ( 𝑅 ∈ Ring → 1o ∈ On ) |
5 | id | ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Ring ) | |
6 | 0ss | ⊢ ∅ ⊆ ( 1o × 1o ) | |
7 | 6 | a1i | ⊢ ( 𝑅 ∈ Ring → ∅ ⊆ ( 1o × 1o ) ) |
8 | 2 4 5 7 | opsrring | ⊢ ( 𝑅 ∈ Ring → 𝑆 ∈ Ring ) |