Metamath Proof Explorer

Theorem mat1dimbas

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 mat1dimbas ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B → O X ∈ Base A

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 risset ⊢ X ∈ B ↔ ∃ r ∈ B r = X
5 eqcom ⊢ X = r ↔ r = X
6 5 rexbii ⊢ ∃ r ∈ B X = r ↔ ∃ r ∈ B r = X
7 4 6 sylbb2 ⊢ X ∈ B → ∃ r ∈ B X = r
8 7 3ad2ant3 ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B → ∃ r ∈ B X = r
9 opex ⊢ E E ∈ V
10 3 9 eqeltri ⊢ O ∈ V
11 simp3 ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B → X ∈ B
12 opthg ⊢ O ∈ V ∧ X ∈ B → O X = O r ↔ O = O ∧ X = r
13 10 11 12 sylancr ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B → O X = O r ↔ O = O ∧ X = r
14 opex ⊢ O X ∈ V
15 sneqbg ⊢ O X ∈ V → O X = O r ↔ O X = O r
16 14 15 ax-mp ⊢ O X = O r ↔ O X = O r
17 eqid ⊢ O = O
18 17 biantrur ⊢ X = r ↔ O = O ∧ X = r
19 13 16 18 3bitr4g ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B → O X = O r ↔ X = r
20 19 rexbidv ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B → ∃ r ∈ B O X = O r ↔ ∃ r ∈ B X = r
21 8 20 mpbird ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B → ∃ r ∈ B O X = O r
22 1 2 3 mat1dimelbas ⊢ R ∈ Ring ∧ E ∈ V → O X ∈ Base A ↔ ∃ r ∈ B O X = O r
23 22 3adant3 ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B → O X ∈ Base A ↔ ∃ r ∈ B O X = O r
24 21 23 mpbird ⊢ R ∈ Ring ∧ E ∈ V ∧ X ∈ B → O X ∈ Base A