Step |
Hyp |
Ref |
Expression |
1 |
|
mat1ric.a |
⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 ) |
2 |
|
eqid |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) |
3 |
|
eqid |
⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 ) |
4 |
|
eqid |
⊢ 〈 𝐸 , 𝐸 〉 = 〈 𝐸 , 𝐸 〉 |
5 |
|
opeq2 |
⊢ ( 𝑥 = 𝑦 → 〈 〈 𝐸 , 𝐸 〉 , 𝑥 〉 = 〈 〈 𝐸 , 𝐸 〉 , 𝑦 〉 ) |
6 |
5
|
sneqd |
⊢ ( 𝑥 = 𝑦 → { 〈 〈 𝐸 , 𝐸 〉 , 𝑥 〉 } = { 〈 〈 𝐸 , 𝐸 〉 , 𝑦 〉 } ) |
7 |
6
|
cbvmptv |
⊢ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ { 〈 〈 𝐸 , 𝐸 〉 , 𝑥 〉 } ) = ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ { 〈 〈 𝐸 , 𝐸 〉 , 𝑦 〉 } ) |
8 |
2 1 3 4 7
|
mat1rngiso |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ { 〈 〈 𝐸 , 𝐸 〉 , 𝑥 〉 } ) ∈ ( 𝑅 RingIso 𝐴 ) ) |
9 |
8
|
ne0d |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑅 RingIso 𝐴 ) ≠ ∅ ) |
10 |
|
brric |
⊢ ( 𝑅 ≃𝑟 𝐴 ↔ ( 𝑅 RingIso 𝐴 ) ≠ ∅ ) |
11 |
9 10
|
sylibr |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝑅 ≃𝑟 𝐴 ) |