This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mat1ric

Description: A ring is isomorphic to the ring of matrices with dimension 1 over this ring. (Contributed by AV, 30-Dec-2019)

Ref Expression
Hypothesis mat1ric.a ⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 )
Assertion mat1ric ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝑅 ≃𝑟 𝐴 )

Proof

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 ∧ 𝐸 ∈ 𝑉 ) → 𝑅 ≃𝑟 𝐴 )