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 eqtr4di ⊢ n = N ∧ r = R → n Mat r = A
8 7 fveq2d ⊢ n = N ∧ r = R → Base n Mat r = Base A
9 8 2 eqtr4di ⊢ 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 eqtr4di ⊢ r = R → 1 r = 1 ˙
13 fveq2 ⊢ r = R → 0 r = 0 R
14 13 5 eqtr4di ⊢ 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 eqtr4di ⊢ ¬ 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