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

Metamath Proof Explorer

Theorem mat1f1o

Description: There is a 1-1 function from a ring onto the ring of matrices with dimension 1 over this ring. (Contributed by AV, 22-Dec-2019)

Ref Expression
Hypotheses mat1rhmval.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
mat1rhmval.a ⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 )
mat1rhmval.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
mat1rhmval.o ⊢ 𝑂 = ⟨ 𝐸 , 𝐸 ⟩
mat1rhmval.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐾 ↦ { ⟨ 𝑂 , 𝑥 ⟩ } )
Assertion mat1f1o ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐹 : 𝐾 –1-1-onto→ 𝐵 )

Proof

Step Hyp Ref Expression
1 mat1rhmval.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
2 mat1rhmval.a ⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 )
3 mat1rhmval.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
4 mat1rhmval.o ⊢ 𝑂 = ⟨ 𝐸 , 𝐸 ⟩
5 mat1rhmval.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐾 ↦ { ⟨ 𝑂 , 𝑥 ⟩ } )
6 1 fvexi ⊢ 𝐾 ∈ V
7 opex ⊢ ⟨ 𝐸 , 𝐸 ⟩ ∈ V
8 4 7 eqeltri ⊢ 𝑂 ∈ V
9 6 8 pm3.2i ⊢ ( 𝐾 ∈ V ∧ 𝑂 ∈ V )
10 vex ⊢ 𝑥 ∈ V
11 8 10 xpsn ⊢ ( { 𝑂 } × { 𝑥 } ) = { ⟨ 𝑂 , 𝑥 ⟩ }
12 11 eqcomi ⊢ { ⟨ 𝑂 , 𝑥 ⟩ } = ( { 𝑂 } × { 𝑥 } )
13 12 mpteq2i ⊢ ( 𝑥 ∈ 𝐾 ↦ { ⟨ 𝑂 , 𝑥 ⟩ } ) = ( 𝑥 ∈ 𝐾 ↦ ( { 𝑂 } × { 𝑥 } ) )
14 13 mapsnf1o ⊢ ( ( 𝐾 ∈ V ∧ 𝑂 ∈ V ) → ( 𝑥 ∈ 𝐾 ↦ { ⟨ 𝑂 , 𝑥 ⟩ } ) : 𝐾 –1-1-onto→ ( 𝐾 ↑m { 𝑂 } ) )
15 9 14 mp1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝑥 ∈ 𝐾 ↦ { ⟨ 𝑂 , 𝑥 ⟩ } ) : 𝐾 –1-1-onto→ ( 𝐾 ↑m { 𝑂 } ) )
16 5 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐹 = ( 𝑥 ∈ 𝐾 ↦ { ⟨ 𝑂 , 𝑥 ⟩ } ) )
17 eqidd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐾 = 𝐾 )
18 4 sneqi ⊢ { 𝑂 } = { ⟨ 𝐸 , 𝐸 ⟩ }
19 simpr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐸 ∈ 𝑉 )
20 xpsng ⊢ ( ( 𝐸 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉 ) → ( { 𝐸 } × { 𝐸 } ) = { ⟨ 𝐸 , 𝐸 ⟩ } )
21 19 20 sylancom ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( { 𝐸 } × { 𝐸 } ) = { ⟨ 𝐸 , 𝐸 ⟩ } )
22 18 21 eqtr4id ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → { 𝑂 } = ( { 𝐸 } × { 𝐸 } ) )
23 22 oveq2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝐾 ↑m { 𝑂 } ) = ( 𝐾 ↑m ( { 𝐸 } × { 𝐸 } ) ) )
24 snfi ⊢ { 𝐸 } ∈ Fin
25 simpl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝑅 ∈ Ring )
26 2 1 matbas2 ⊢ ( ( { 𝐸 } ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐾 ↑m ( { 𝐸 } × { 𝐸 } ) ) = ( Base ‘ 𝐴 ) )
27 24 25 26 sylancr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝐾 ↑m ( { 𝐸 } × { 𝐸 } ) ) = ( Base ‘ 𝐴 ) )
28 23 27 eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝐾 ↑m { 𝑂 } ) = ( Base ‘ 𝐴 ) )
29 3 28 eqtr4id ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐵 = ( 𝐾 ↑m { 𝑂 } ) )
30 16 17 29 f1oeq123d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝐹 : 𝐾 –1-1-onto→ 𝐵 ↔ ( 𝑥 ∈ 𝐾 ↦ { ⟨ 𝑂 , 𝑥 ⟩ } ) : 𝐾 –1-1-onto→ ( 𝐾 ↑m { 𝑂 } ) ) )
31 15 30 mpbird ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐹 : 𝐾 –1-1-onto→ 𝐵 )