Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  marrepval Structured version   Unicode version

Theorem marrepval 19042
 Description: Third substitution for the definition of the matrix row replacement function. (Contributed by AV, 12-Feb-2019.)
Hypotheses
Ref Expression
marrepfval.a Mat
marrepfval.b
marrepfval.q matRRep
marrepfval.z
Assertion
Ref Expression
marrepval
Distinct variable groups:   ,,   ,,   ,,   ,,   ,,   ,,
Allowed substitution hints:   (,)   (,)   (,)   (,)

Proof of Theorem marrepval
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 marrepfval.a . . . 4 Mat
2 marrepfval.b . . . 4
3 marrepfval.q . . . 4 matRRep
4 marrepfval.z . . . 4
51, 2, 3, 4marrepval0 19041 . . 3
7 simprl 756 . . 3
8 simplrr 762 . . 3
91, 2matrcl 18892 . . . . . . 7
109simpld 459 . . . . . 6
1110, 10jca 532 . . . . 5
1211ad3antrrr 729 . . . 4
13 mpt2exga 6861 . . . 4
1412, 13syl 16 . . 3
15 eqeq2 2458 . . . . . . 7
1615adantr 465 . . . . . 6
17 eqeq2 2458 . . . . . . . 8
1817ifbid 3948 . . . . . . 7
1918adantl 466 . . . . . 6
2016, 19ifbieq1d 3949 . . . . 5
2120mpt2eq3dv 6348 . . . 4