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 ⊢ K = Base R
mat1rhmval.a ⊢ A = E Mat R
mat1rhmval.b ⊢ B = Base A
mat1rhmval.o ⊢ O = E E
mat1rhmval.f ⊢ F = x ∈ K ⟼ O x
Assertion mat1f1o ⊢ R ∈ Ring ∧ E ∈ V → F : K ⟶ 1-1 onto B

Proof

Step Hyp Ref Expression
1 mat1rhmval.k ⊢ K = Base R
2 mat1rhmval.a ⊢ A = E Mat R
3 mat1rhmval.b ⊢ B = Base A
4 mat1rhmval.o ⊢ O = E E
5 mat1rhmval.f ⊢ F = x ∈ K ⟼ O x
6 1 fvexi ⊢ K ∈ V
7 opex ⊢ E E ∈ V
8 4 7 eqeltri ⊢ O ∈ V
9 6 8 pm3.2i ⊢ K ∈ V ∧ O ∈ V
10 vex ⊢ x ∈ V
11 8 10 xpsn ⊢ O × x = O x
12 11 eqcomi ⊢ O x = O × x
13 12 mpteq2i ⊢ x ∈ K ⟼ O x = x ∈ K ⟼ O × x
14 13 mapsnf1o ⊢ K ∈ V ∧ O ∈ V → x ∈ K ⟼ O x : K ⟶ 1-1 onto K O
15 9 14 mp1i ⊢ R ∈ Ring ∧ E ∈ V → x ∈ K ⟼ O x : K ⟶ 1-1 onto K O
16 5 a1i ⊢ R ∈ Ring ∧ E ∈ V → F = x ∈ K ⟼ O x
17 eqidd ⊢ R ∈ Ring ∧ E ∈ V → K = K
18 4 sneqi ⊢ O = E E
19 simpr ⊢ R ∈ Ring ∧ E ∈ V → E ∈ V
20 xpsng ⊢ E ∈ V ∧ E ∈ V → E × E = E E
21 19 20 sylancom ⊢ R ∈ Ring ∧ E ∈ V → E × E = E E
22 18 21 eqtr4id ⊢ R ∈ Ring ∧ E ∈ V → O = E × E
23 22 oveq2d ⊢ R ∈ Ring ∧ E ∈ V → K O = K E × E
24 snfi ⊢ E ∈ Fin
25 simpl ⊢ R ∈ Ring ∧ E ∈ V → R ∈ Ring
26 2 1 matbas2 ⊢ E ∈ Fin ∧ R ∈ Ring → K E × E = Base A
27 24 25 26 sylancr ⊢ R ∈ Ring ∧ E ∈ V → K E × E = Base A
28 23 27 eqtrd ⊢ R ∈ Ring ∧ E ∈ V → K O = Base A
29 3 28 eqtr4id ⊢ R ∈ Ring ∧ E ∈ V → B = K O
30 16 17 29 f1oeq123d ⊢ R ∈ Ring ∧ E ∈ V → F : K ⟶ 1-1 onto B ↔ x ∈ K ⟼ O x : K ⟶ 1-1 onto K O
31 15 30 mpbird ⊢ R ∈ Ring ∧ E ∈ V → F : K ⟶ 1-1 onto B