Step |
Hyp |
Ref |
Expression |
1 |
|
opsrring.o |
⊢ 𝑂 = ( ( 𝐼 ordPwSer 𝑅 ) ‘ 𝑇 ) |
2 |
|
opsrring.i |
⊢ ( 𝜑 → 𝐼 ∈ 𝑉 ) |
3 |
|
opsrring.r |
⊢ ( 𝜑 → 𝑅 ∈ Ring ) |
4 |
|
opsrring.t |
⊢ ( 𝜑 → 𝑇 ⊆ ( 𝐼 × 𝐼 ) ) |
5 |
|
eqid |
⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 ) |
6 |
5 2 3
|
psrring |
⊢ ( 𝜑 → ( 𝐼 mPwSer 𝑅 ) ∈ Ring ) |
7 |
|
eqidd |
⊢ ( 𝜑 → ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) |
8 |
5 1 4
|
opsrbas |
⊢ ( 𝜑 → ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ 𝑂 ) ) |
9 |
5 1 4
|
opsrplusg |
⊢ ( 𝜑 → ( +g ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( +g ‘ 𝑂 ) ) |
10 |
9
|
oveqdr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ) → ( 𝑥 ( +g ‘ ( 𝐼 mPwSer 𝑅 ) ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑂 ) 𝑦 ) ) |
11 |
5 1 4
|
opsrmulr |
⊢ ( 𝜑 → ( .r ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( .r ‘ 𝑂 ) ) |
12 |
11
|
oveqdr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑦 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ) → ( 𝑥 ( .r ‘ ( 𝐼 mPwSer 𝑅 ) ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝑂 ) 𝑦 ) ) |
13 |
7 8 10 12
|
ringpropd |
⊢ ( 𝜑 → ( ( 𝐼 mPwSer 𝑅 ) ∈ Ring ↔ 𝑂 ∈ Ring ) ) |
14 |
6 13
|
mpbid |
⊢ ( 𝜑 → 𝑂 ∈ Ring ) |