Metamath Proof Explorer

Theorem matbas2d

Description: The base set of the matrix ring as a mapping operation. (Contributed by Stefan O'Rear, 11-Jul-2018)

Ref Expression
Hypotheses matbas2.a ⊢ A = N Mat R
matbas2.k ⊢ K = Base R
matbas2i.b ⊢ B = Base A
matbas2d.n ⊢ φ → N ∈ Fin
matbas2d.r ⊢ φ → R ∈ V
matbas2d.c ⊢ φ ∧ x ∈ N ∧ y ∈ N → C ∈ K
Assertion matbas2d ⊢ φ → x ∈ N , y ∈ N ⟼ C ∈ B

Proof

Step Hyp Ref Expression
1 matbas2.a ⊢ A = N Mat R
2 matbas2.k ⊢ K = Base R
3 matbas2i.b ⊢ B = Base A
4 matbas2d.n ⊢ φ → N ∈ Fin
5 matbas2d.r ⊢ φ → R ∈ V
6 matbas2d.c ⊢ φ ∧ x ∈ N ∧ y ∈ N → C ∈ K
7 6 3expb ⊢ φ ∧ x ∈ N ∧ y ∈ N → C ∈ K
8 7 ralrimivva ⊢ φ → ∀ x ∈ N ∀ y ∈ N C ∈ K
9 eqid ⊢ x ∈ N , y ∈ N ⟼ C = x ∈ N , y ∈ N ⟼ C
10 9 fmpo ⊢ ∀ x ∈ N ∀ y ∈ N C ∈ K ↔ x ∈ N , y ∈ N ⟼ C : N × N ⟶ K
11 8 10 sylib ⊢ φ → x ∈ N , y ∈ N ⟼ C : N × N ⟶ K
12 1 2 matbas2 ⊢ N ∈ Fin ∧ R ∈ V → K N × N = Base A
13 4 5 12 syl2anc ⊢ φ → K N × N = Base A
14 3 13 eqtr4id ⊢ φ → B = K N × N
15 14 eleq2d ⊢ φ → x ∈ N , y ∈ N ⟼ C ∈ B ↔ x ∈ N , y ∈ N ⟼ C ∈ K N × N
16 2 fvexi ⊢ K ∈ V
17 4 4 xpexd ⊢ φ → N × N ∈ V
18 elmapg ⊢ K ∈ V ∧ N × N ∈ V → x ∈ N , y ∈ N ⟼ C ∈ K N × N ↔ x ∈ N , y ∈ N ⟼ C : N × N ⟶ K
19 16 17 18 sylancr ⊢ φ → x ∈ N , y ∈ N ⟼ C ∈ K N × N ↔ x ∈ N , y ∈ N ⟼ C : N × N ⟶ K
20 15 19 bitrd ⊢ φ → x ∈ N , y ∈ N ⟼ C ∈ B ↔ x ∈ N , y ∈ N ⟼ C : N × N ⟶ K
21 11 20 mpbird ⊢ φ → x ∈ N , y ∈ N ⟼ C ∈ B