Metamath Proof Explorer

Theorem mat1dimelbas

Description: A matrix with dimension 1 is an ordered pair with an ordered pair (of the one and only pair of indices) as first component. (Contributed by AV, 15-Aug-2019)

Ref Expression
Hypotheses mat1dim.a ⊢ A = E Mat R
mat1dim.b ⊢ B = Base R
mat1dim.o ⊢ O = E E
Assertion mat1dimelbas ⊢ R ∈ Ring ∧ E ∈ V → M ∈ Base A ↔ ∃ r ∈ B M = O r

Proof

Step Hyp Ref Expression
1 mat1dim.a ⊢ A = E Mat R
2 mat1dim.b ⊢ B = Base R
3 mat1dim.o ⊢ O = E E
4 snfi ⊢ E ∈ Fin
5 simpl ⊢ R ∈ Ring ∧ E ∈ V → R ∈ Ring
6 1 2 matbas2 ⊢ E ∈ Fin ∧ R ∈ Ring → B E × E = Base A
7 6 eqcomd ⊢ E ∈ Fin ∧ R ∈ Ring → Base A = B E × E
8 7 eleq2d ⊢ E ∈ Fin ∧ R ∈ Ring → M ∈ Base A ↔ M ∈ B E × E
9 4 5 8 sylancr ⊢ R ∈ Ring ∧ E ∈ V → M ∈ Base A ↔ M ∈ B E × E
10 2 fvexi ⊢ B ∈ V
11 snex ⊢ E ∈ V
12 11 11 pm3.2i ⊢ E ∈ V ∧ E ∈ V
13 xpexg ⊢ E ∈ V ∧ E ∈ V → E × E ∈ V
14 12 13 mp1i ⊢ R ∈ Ring ∧ E ∈ V → E × E ∈ V
15 elmapg ⊢ B ∈ V ∧ E × E ∈ V → M ∈ B E × E ↔ M : E × E ⟶ B
16 10 14 15 sylancr ⊢ R ∈ Ring ∧ E ∈ V → M ∈ B E × E ↔ M : E × E ⟶ B
17 9 16 bitrd ⊢ R ∈ Ring ∧ E ∈ V → M ∈ Base A ↔ M : E × E ⟶ B
18 xpsng ⊢ E ∈ V ∧ E ∈ V → E × E = E E
19 18 anidms ⊢ E ∈ V → E × E = E E
20 19 adantl ⊢ R ∈ Ring ∧ E ∈ V → E × E = E E
21 20 feq2d ⊢ R ∈ Ring ∧ E ∈ V → M : E × E ⟶ B ↔ M : E E ⟶ B
22 opex ⊢ E E ∈ V
23 22 fsn2 ⊢ M : E E ⟶ B ↔ M ⁡ E E ∈ B ∧ M = E E M ⁡ E E
24 risset ⊢ M ⁡ E E ∈ B ↔ ∃ r ∈ B r = M ⁡ E E
25 eqcom ⊢ r = M ⁡ E E ↔ M ⁡ E E = r
26 25 rexbii ⊢ ∃ r ∈ B r = M ⁡ E E ↔ ∃ r ∈ B M ⁡ E E = r
27 24 26 sylbb ⊢ M ⁡ E E ∈ B → ∃ r ∈ B M ⁡ E E = r
28 27 ad2antrl ⊢ R ∈ Ring ∧ E ∈ V ∧ M ⁡ E E ∈ B ∧ M = E E M ⁡ E E → ∃ r ∈ B M ⁡ E E = r
29 eqeq1 ⊢ M = E E M ⁡ E E → M = E E r ↔ E E M ⁡ E E = E E r
30 opex ⊢ E E M ⁡ E E ∈ V
31 sneqbg ⊢ E E M ⁡ E E ∈ V → E E M ⁡ E E = E E r ↔ E E M ⁡ E E = E E r
32 30 31 ax-mp ⊢ E E M ⁡ E E = E E r ↔ E E M ⁡ E E = E E r
33 eqid ⊢ E E = E E
34 vex ⊢ r ∈ V
35 22 34 opth2 ⊢ E E M ⁡ E E = E E r ↔ E E = E E ∧ M ⁡ E E = r
36 33 35 mpbiran ⊢ E E M ⁡ E E = E E r ↔ M ⁡ E E = r
37 32 36 bitri ⊢ E E M ⁡ E E = E E r ↔ M ⁡ E E = r
38 29 37 bitrdi ⊢ M = E E M ⁡ E E → M = E E r ↔ M ⁡ E E = r
39 38 adantl ⊢ M ⁡ E E ∈ B ∧ M = E E M ⁡ E E → M = E E r ↔ M ⁡ E E = r
40 39 adantl ⊢ R ∈ Ring ∧ E ∈ V ∧ M ⁡ E E ∈ B ∧ M = E E M ⁡ E E → M = E E r ↔ M ⁡ E E = r
41 40 rexbidv ⊢ R ∈ Ring ∧ E ∈ V ∧ M ⁡ E E ∈ B ∧ M = E E M ⁡ E E → ∃ r ∈ B M = E E r ↔ ∃ r ∈ B M ⁡ E E = r
42 28 41 mpbird ⊢ R ∈ Ring ∧ E ∈ V ∧ M ⁡ E E ∈ B ∧ M = E E M ⁡ E E → ∃ r ∈ B M = E E r
43 42 ex ⊢ R ∈ Ring ∧ E ∈ V → M ⁡ E E ∈ B ∧ M = E E M ⁡ E E → ∃ r ∈ B M = E E r
44 23 43 biimtrid ⊢ R ∈ Ring ∧ E ∈ V → M : E E ⟶ B → ∃ r ∈ B M = E E r
45 21 44 sylbid ⊢ R ∈ Ring ∧ E ∈ V → M : E × E ⟶ B → ∃ r ∈ B M = E E r
46 f1o2sn ⊢ E ∈ V ∧ r ∈ B → E E r : E × E ⟶ 1-1 onto r
47 f1of ⊢ E E r : E × E ⟶ 1-1 onto r → E E r : E × E ⟶ r
48 46 47 syl ⊢ E ∈ V ∧ r ∈ B → E E r : E × E ⟶ r
49 48 adantll ⊢ R ∈ Ring ∧ E ∈ V ∧ r ∈ B → E E r : E × E ⟶ r
50 snssi ⊢ r ∈ B → r ⊆ B
51 50 adantl ⊢ R ∈ Ring ∧ E ∈ V ∧ r ∈ B → r ⊆ B
52 49 51 fssd ⊢ R ∈ Ring ∧ E ∈ V ∧ r ∈ B → E E r : E × E ⟶ B
53 feq1 ⊢ M = E E r → M : E × E ⟶ B ↔ E E r : E × E ⟶ B
54 52 53 syl5ibrcom ⊢ R ∈ Ring ∧ E ∈ V ∧ r ∈ B → M = E E r → M : E × E ⟶ B
55 54 rexlimdva ⊢ R ∈ Ring ∧ E ∈ V → ∃ r ∈ B M = E E r → M : E × E ⟶ B
56 45 55 impbid ⊢ R ∈ Ring ∧ E ∈ V → M : E × E ⟶ B ↔ ∃ r ∈ B M = E E r
57 3 eqcomi ⊢ E E = O
58 57 opeq1i ⊢ E E r = O r
59 58 sneqi ⊢ E E r = O r
60 59 eqeq2i ⊢ M = E E r ↔ M = O r
61 60 a1i ⊢ R ∈ Ring ∧ E ∈ V → M = E E r ↔ M = O r
62 61 rexbidv ⊢ R ∈ Ring ∧ E ∈ V → ∃ r ∈ B M = E E r ↔ ∃ r ∈ B M = O r
63 56 62 bitrd ⊢ R ∈ Ring ∧ E ∈ V → M : E × E ⟶ B ↔ ∃ r ∈ B M = O r
64 17 63 bitrd ⊢ R ∈ Ring ∧ E ∈ V → M ∈ Base A ↔ ∃ r ∈ B M = O r