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=NMatR
minmar1fval.b ⊢B=BaseA
minmar1fval.q ⊢Q=NminMatR1R
minmar1fval.o ⊢1˙=1R
minmar1fval.z ⊢0˙=0R
Assertion minmar1fval ⊢Q=m∈B⟼k∈N,l∈N⟼i∈N,j∈N⟼ifi=kifj=l1˙0˙imj

Proof

Step Hyp Ref Expression
1 minmar1fval.a ⊢A=NMatR
2 minmar1fval.b ⊢B=BaseA
3 minmar1fval.q ⊢Q=NminMatR1R
4 minmar1fval.o ⊢1˙=1R
5 minmar1fval.z ⊢0˙=0R
6 oveq12 ⊢n=N∧r=R→nMatr=NMatR
7 6 1 eqtr4di ⊢n=N∧r=R→nMatr=A
8 7 fveq2d ⊢n=N∧r=R→BasenMatr=BaseA
9 8 2 eqtr4di ⊢n=N∧r=R→BasenMatr=B
10 simpl ⊢n=N∧r=R→n=N
11 fveq2 ⊢r=R→1r=1R
12 11 4 eqtr4di ⊢r=R→1r=1˙
13 fveq2 ⊢r=R→0r=0R
14 13 5 eqtr4di ⊢r=R→0r=0˙
15 12 14 ifeq12d ⊢r=R→ifj=l1r0r=ifj=l1˙0˙
16 15 ifeq1d ⊢r=R→ifi=kifj=l1r0rimj=ifi=kifj=l1˙0˙imj
17 16 adantl ⊢n=N∧r=R→ifi=kifj=l1r0rimj=ifi=kifj=l1˙0˙imj
18 10 10 17 mpoeq123dv ⊢n=N∧r=R→i∈n,j∈n⟼ifi=kifj=l1r0rimj=i∈N,j∈N⟼ifi=kifj=l1˙0˙imj
19 10 10 18 mpoeq123dv ⊢n=N∧r=R→k∈n,l∈n⟼i∈n,j∈n⟼ifi=kifj=l1r0rimj=k∈N,l∈N⟼i∈N,j∈N⟼ifi=kifj=l1˙0˙imj
20 9 19 mpteq12dv ⊢n=N∧r=R→m∈BasenMatr⟼k∈n,l∈n⟼i∈n,j∈n⟼ifi=kifj=l1r0rimj=m∈B⟼k∈N,l∈N⟼i∈N,j∈N⟼ifi=kifj=l1˙0˙imj
21 df-minmar1 ⊢minMatR1=n∈V,r∈V⟼m∈BasenMatr⟼k∈n,l∈n⟼i∈n,j∈n⟼ifi=kifj=l1r0rimj
22 2 fvexi ⊢B∈V
23 22 mptex ⊢m∈B⟼k∈N,l∈N⟼i∈N,j∈N⟼ifi=kifj=l1˙0˙imj∈V
24 20 21 23 ovmpoa ⊢N∈V∧R∈V→NminMatR1R=m∈B⟼k∈N,l∈N⟼i∈N,j∈N⟼ifi=kifj=l1˙0˙imj
25 21 mpondm0 ⊢¬N∈V∧R∈V→NminMatR1R=∅
26 mpt0 ⊢m∈∅⟼k∈N,l∈N⟼i∈N,j∈N⟼ifi=kifj=l1˙0˙imj=∅
27 25 26 eqtr4di ⊢¬N∈V∧R∈V→NminMatR1R=m∈∅⟼k∈N,l∈N⟼i∈N,j∈N⟼ifi=kifj=l1˙0˙imj
28 1 fveq2i ⊢BaseA=BaseNMatR
29 2 28 eqtri ⊢B=BaseNMatR
30 matbas0pc ⊢¬N∈V∧R∈V→BaseNMatR=∅
31 29 30 eqtrid ⊢¬N∈V∧R∈V→B=∅
32 31 mpteq1d ⊢¬N∈V∧R∈V→m∈B⟼k∈N,l∈N⟼i∈N,j∈N⟼ifi=kifj=l1˙0˙imj=m∈∅⟼k∈N,l∈N⟼i∈N,j∈N⟼ifi=kifj=l1˙0˙imj
33 27 32 eqtr4d ⊢¬N∈V∧R∈V→NminMatR1R=m∈B⟼k∈N,l∈N⟼i∈N,j∈N⟼ifi=kifj=l1˙0˙imj
34 24 33 pm2.61i ⊢NminMatR1R=m∈B⟼k∈N,l∈N⟼i∈N,j∈N⟼ifi=kifj=l1˙0˙imj
35 3 34 eqtri ⊢Q=m∈B⟼k∈N,l∈N⟼i∈N,j∈N⟼ifi=kifj=l1˙0˙imj