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 13 3 syl6reqr φ 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