Metamath Proof Explorer


Theorem minmar1fval

Description: First substitution for the definition of a matrix for a minor. (Contributed by AV, 31-Dec-2018)

Ref Expression
Hypotheses minmar1fval.a A = N Mat R
minmar1fval.b B = Base A
minmar1fval.q Q = N minMatR1 R
minmar1fval.o 1 ˙ = 1 R
minmar1fval.z 0 ˙ = 0 R
Assertion minmar1fval Q = m B k N , l N i N , j N if i = k if j = l 1 ˙ 0 ˙ i m j

Proof

Step Hyp Ref Expression
1 minmar1fval.a A = N Mat R
2 minmar1fval.b B = Base A
3 minmar1fval.q Q = N minMatR1 R
4 minmar1fval.o 1 ˙ = 1 R
5 minmar1fval.z 0 ˙ = 0 R
6 oveq12 n = N r = R n Mat r = N Mat R
7 6 1 syl6eqr n = N r = R n Mat r = A
8 7 fveq2d n = N r = R Base n Mat r = Base A
9 8 2 syl6eqr n = N r = R Base n Mat r = B
10 simpl n = N r = R n = N
11 fveq2 r = R 1 r = 1 R
12 11 4 syl6eqr r = R 1 r = 1 ˙
13 fveq2 r = R 0 r = 0 R
14 13 5 syl6eqr r = R 0 r = 0 ˙
15 12 14 ifeq12d r = R if j = l 1 r 0 r = if j = l 1 ˙ 0 ˙
16 15 ifeq1d r = R if i = k if j = l 1 r 0 r i m j = if i = k if j = l 1 ˙ 0 ˙ i m j
17 16 adantl n = N r = R if i = k if j = l 1 r 0 r i m j = if i = k if j = l 1 ˙ 0 ˙ i m j
18 10 10 17 mpoeq123dv n = N r = R i n , j n if i = k if j = l 1 r 0 r i m j = i N , j N if i = k if j = l 1 ˙ 0 ˙ i m j
19 10 10 18 mpoeq123dv n = N r = R k n , l n i n , j n if i = k if j = l 1 r 0 r i m j = k N , l N i N , j N if i = k if j = l 1 ˙ 0 ˙ i m j
20 9 19 mpteq12dv n = N r = R m Base n Mat r k n , l n i n , j n if i = k if j = l 1 r 0 r i m j = m B k N , l N i N , j N if i = k if j = l 1 ˙ 0 ˙ i m j
21 df-minmar1 minMatR1 = n V , r V m Base n Mat r k n , l n i n , j n if i = k if j = l 1 r 0 r i m j
22 2 fvexi B V
23 22 mptex m B k N , l N i N , j N if i = k if j = l 1 ˙ 0 ˙ i m j V
24 20 21 23 ovmpoa N V R V N minMatR1 R = m B k N , l N i N , j N if i = k if j = l 1 ˙ 0 ˙ i m j
25 21 mpondm0 ¬ N V R V N minMatR1 R =
26 mpt0 m k N , l N i N , j N if i = k if j = l 1 ˙ 0 ˙ i m j =
27 25 26 syl6eqr ¬ N V R V N minMatR1 R = m k N , l N i N , j N if i = k if j = l 1 ˙ 0 ˙ i m j
28 1 fveq2i Base A = Base N Mat R
29 2 28 eqtri B = Base N Mat R
30 matbas0pc ¬ N V R V Base N Mat R =
31 29 30 syl5eq ¬ N V R V B =
32 31 mpteq1d ¬ N V R V m B k N , l N i N , j N if i = k if j = l 1 ˙ 0 ˙ i m j = m k N , l N i N , j N if i = k if j = l 1 ˙ 0 ˙ i m j
33 27 32 eqtr4d ¬ N V R V N minMatR1 R = m B k N , l N i N , j N if i = k if j = l 1 ˙ 0 ˙ i m j
34 24 33 pm2.61i N minMatR1 R = m B k N , l N i N , j N if i = k if j = l 1 ˙ 0 ˙ i m j
35 3 34 eqtri Q = m B k N , l N i N , j N if i = k if j = l 1 ˙ 0 ˙ i m j