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→ 𝐵 )