Metamath Proof Explorer

Theorem matplusgcell

Description: Addition in the matrix ring is cell-wise. (Contributed by AV, 2-Aug-2019)

Ref Expression
Hypotheses matplusgcell.a 
|- A = ( N Mat R )
matplusgcell.b 
|- B = ( Base ` A )
matplusgcell.p 
|- .+b = ( +g ` A )
matplusgcell.q 
|- .+ = ( +g ` R )
Assertion matplusgcell 
|- ( ( ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> ( I ( X .+b Y ) J ) = ( ( I X J ) .+ ( I Y J ) ) )

Proof

Step Hyp Ref Expression
1 matplusgcell.a 
 |-  A = ( N Mat R )
2 matplusgcell.b 
 |-  B = ( Base ` A )
3 matplusgcell.p 
 |-  .+b = ( +g ` A )
4 matplusgcell.q 
 |-  .+ = ( +g ` R )
5 1 2 3 4 matplusg2 
 |-  ( ( X e. B /\ Y e. B ) -> ( X .+b Y ) = ( X oF .+ Y ) )
6 5 oveqd 
 |-  ( ( X e. B /\ Y e. B ) -> ( I ( X .+b Y ) J ) = ( I ( X oF .+ Y ) J ) )
7 6 adantr 
 |-  ( ( ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> ( I ( X .+b Y ) J ) = ( I ( X oF .+ Y ) J ) )
8 df-ov 
 |-  ( I ( X oF .+ Y ) J ) = ( ( X oF .+ Y ) ` <. I , J >. )
9 8 a1i 
 |-  ( ( ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> ( I ( X oF .+ Y ) J ) = ( ( X oF .+ Y ) ` <. I , J >. ) )
10 opelxp 
 |-  ( <. I , J >. e. ( N X. N ) <-> ( I e. N /\ J e. N ) )
11 eqid 
 |-  ( Base ` R ) = ( Base ` R )
12 1 11 2 matbas2i 
 |-  ( X e. B -> X e. ( ( Base ` R ) ^m ( N X. N ) ) )
13 elmapfn 
 |-  ( X e. ( ( Base ` R ) ^m ( N X. N ) ) -> X Fn ( N X. N ) )
14 12 13 syl 
 |-  ( X e. B -> X Fn ( N X. N ) )
15 14 adantr 
 |-  ( ( X e. B /\ Y e. B ) -> X Fn ( N X. N ) )
16 1 11 2 matbas2i 
 |-  ( Y e. B -> Y e. ( ( Base ` R ) ^m ( N X. N ) ) )
17 elmapfn 
 |-  ( Y e. ( ( Base ` R ) ^m ( N X. N ) ) -> Y Fn ( N X. N ) )
18 16 17 syl 
 |-  ( Y e. B -> Y Fn ( N X. N ) )
19 18 adantl 
 |-  ( ( X e. B /\ Y e. B ) -> Y Fn ( N X. N ) )
20 1 2 matrcl 
 |-  ( X e. B -> ( N e. Fin /\ R e. _V ) )
21 xpfi 
 |-  ( ( N e. Fin /\ N e. Fin ) -> ( N X. N ) e. Fin )
22 21 anidms 
 |-  ( N e. Fin -> ( N X. N ) e. Fin )
23 22 adantr 
 |-  ( ( N e. Fin /\ R e. _V ) -> ( N X. N ) e. Fin )
24 20 23 syl 
 |-  ( X e. B -> ( N X. N ) e. Fin )
25 24 adantr 
 |-  ( ( X e. B /\ Y e. B ) -> ( N X. N ) e. Fin )
26 inidm 
 |-  ( ( N X. N ) i^i ( N X. N ) ) = ( N X. N )
27 df-ov 
 |-  ( I X J ) = ( X ` <. I , J >. )
28 27 eqcomi 
 |-  ( X ` <. I , J >. ) = ( I X J )
29 28 a1i 
 |-  ( ( ( X e. B /\ Y e. B ) /\ <. I , J >. e. ( N X. N ) ) -> ( X ` <. I , J >. ) = ( I X J ) )
30 df-ov 
 |-  ( I Y J ) = ( Y ` <. I , J >. )
31 30 eqcomi 
 |-  ( Y ` <. I , J >. ) = ( I Y J )
32 31 a1i 
 |-  ( ( ( X e. B /\ Y e. B ) /\ <. I , J >. e. ( N X. N ) ) -> ( Y ` <. I , J >. ) = ( I Y J ) )
33 15 19 25 25 26 29 32 ofval 
 |-  ( ( ( X e. B /\ Y e. B ) /\ <. I , J >. e. ( N X. N ) ) -> ( ( X oF .+ Y ) ` <. I , J >. ) = ( ( I X J ) .+ ( I Y J ) ) )
34 10 33 sylan2br 
 |-  ( ( ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> ( ( X oF .+ Y ) ` <. I , J >. ) = ( ( I X J ) .+ ( I Y J ) ) )
35 7 9 34 3eqtrd 
 |-  ( ( ( X e. B /\ Y e. B ) /\ ( I e. N /\ J e. N ) ) -> ( I ( X .+b Y ) J ) = ( ( I X J ) .+ ( I Y J ) ) )