Metamath Proof Explorer

Theorem marrepeval

Description: An entry of a matrix with a replaced row. (Contributed by AV, 12-Feb-2019)

Ref Expression
Hypotheses marrepfval.a 
|- A = ( N Mat R )
marrepfval.b 
|- B = ( Base ` A )
marrepfval.q 
|- Q = ( N matRRep R )
marrepfval.z 
|- .0. = ( 0g ` R )
Assertion marrepeval 
|- ( ( ( M e. B /\ S e. ( Base ` R ) ) /\ ( K e. N /\ L e. N ) /\ ( I e. N /\ J e. N ) ) -> ( I ( K ( M Q S ) L ) J ) = if ( I = K , if ( J = L , S , .0. ) , ( I M J ) ) )

Proof

Step Hyp Ref Expression
1 marrepfval.a 
 |-  A = ( N Mat R )
2 marrepfval.b 
 |-  B = ( Base ` A )
3 marrepfval.q 
 |-  Q = ( N matRRep R )
4 marrepfval.z 
 |-  .0. = ( 0g ` R )
5 1 2 3 4 marrepval 
 |-  ( ( ( M e. B /\ S e. ( Base ` R ) ) /\ ( K e. N /\ L e. N ) ) -> ( K ( M Q S ) L ) = ( i e. N , j e. N |-> if ( i = K , if ( j = L , S , .0. ) , ( i M j ) ) ) )
6 5 3adant3 
 |-  ( ( ( M e. B /\ S e. ( Base ` R ) ) /\ ( K e. N /\ L e. N ) /\ ( I e. N /\ J e. N ) ) -> ( K ( M Q S ) L ) = ( i e. N , j e. N |-> if ( i = K , if ( j = L , S , .0. ) , ( i M j ) ) ) )
7 simp3l 
 |-  ( ( ( M e. B /\ S e. ( Base ` R ) ) /\ ( K e. N /\ L e. N ) /\ ( I e. N /\ J e. N ) ) -> I e. N )
8 simpl3r 
 |-  ( ( ( ( M e. B /\ S e. ( Base ` R ) ) /\ ( K e. N /\ L e. N ) /\ ( I e. N /\ J e. N ) ) /\ i = I ) -> J e. N )
9 4 fvexi 
 |-  .0. e. _V
10 ifexg 
 |-  ( ( S e. ( Base ` R ) /\ .0. e. _V ) -> if ( j = L , S , .0. ) e. _V )
11 9 10 mpan2 
 |-  ( S e. ( Base ` R ) -> if ( j = L , S , .0. ) e. _V )
12 ovexd 
 |-  ( S e. ( Base ` R ) -> ( i M j ) e. _V )
13 11 12 ifcld 
 |-  ( S e. ( Base ` R ) -> if ( i = K , if ( j = L , S , .0. ) , ( i M j ) ) e. _V )
14 13 adantl 
 |-  ( ( M e. B /\ S e. ( Base ` R ) ) -> if ( i = K , if ( j = L , S , .0. ) , ( i M j ) ) e. _V )
15 14 3ad2ant1 
 |-  ( ( ( M e. B /\ S e. ( Base ` R ) ) /\ ( K e. N /\ L e. N ) /\ ( I e. N /\ J e. N ) ) -> if ( i = K , if ( j = L , S , .0. ) , ( i M j ) ) e. _V )
16 15 adantr 
 |-  ( ( ( ( M e. B /\ S e. ( Base ` R ) ) /\ ( K e. N /\ L e. N ) /\ ( I e. N /\ J e. N ) ) /\ ( i = I /\ j = J ) ) -> if ( i = K , if ( j = L , S , .0. ) , ( i M j ) ) e. _V )
17 eqeq1 
 |-  ( i = I -> ( i = K <-> I = K ) )
18 17 adantr 
 |-  ( ( i = I /\ j = J ) -> ( i = K <-> I = K ) )
19 eqeq1 
 |-  ( j = J -> ( j = L <-> J = L ) )
20 19 ifbid 
 |-  ( j = J -> if ( j = L , S , .0. ) = if ( J = L , S , .0. ) )
21 20 adantl 
 |-  ( ( i = I /\ j = J ) -> if ( j = L , S , .0. ) = if ( J = L , S , .0. ) )
22 oveq12 
 |-  ( ( i = I /\ j = J ) -> ( i M j ) = ( I M J ) )
23 18 21 22 ifbieq12d 
 |-  ( ( i = I /\ j = J ) -> if ( i = K , if ( j = L , S , .0. ) , ( i M j ) ) = if ( I = K , if ( J = L , S , .0. ) , ( I M J ) ) )
24 23 adantl 
 |-  ( ( ( ( M e. B /\ S e. ( Base ` R ) ) /\ ( K e. N /\ L e. N ) /\ ( I e. N /\ J e. N ) ) /\ ( i = I /\ j = J ) ) -> if ( i = K , if ( j = L , S , .0. ) , ( i M j ) ) = if ( I = K , if ( J = L , S , .0. ) , ( I M J ) ) )
25 7 8 16 24 ovmpodv2 
 |-  ( ( ( M e. B /\ S e. ( Base ` R ) ) /\ ( K e. N /\ L e. N ) /\ ( I e. N /\ J e. N ) ) -> ( ( K ( M Q S ) L ) = ( i e. N , j e. N |-> if ( i = K , if ( j = L , S , .0. ) , ( i M j ) ) ) -> ( I ( K ( M Q S ) L ) J ) = if ( I = K , if ( J = L , S , .0. ) , ( I M J ) ) ) )
26 6 25 mpd 
 |-  ( ( ( M e. B /\ S e. ( Base ` R ) ) /\ ( K e. N /\ L e. N ) /\ ( I e. N /\ J e. N ) ) -> ( I ( K ( M Q S ) L ) J ) = if ( I = K , if ( J = L , S , .0. ) , ( I M J ) ) )