Metamath Proof Explorer

Theorem matplusg2

Description: Addition in the matrix ring is cell-wise. (Contributed by Stefan O'Rear, 5-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 matplusg2.a 
 |-  A = ( N Mat R )
2 matplusg2.b 
 |-  B = ( Base ` A )
3 matplusg2.p 
 |-  .+b = ( +g ` A )
4 matplusg2.q 
 |-  .+ = ( +g ` R )
5 1 2 matrcl 
 |-  ( X e. B -> ( N e. Fin /\ R e. _V ) )
6 5 adantr 
 |-  ( ( X e. B /\ Y e. B ) -> ( N e. Fin /\ R e. _V ) )
7 eqid 
 |-  ( R freeLMod ( N X. N ) ) = ( R freeLMod ( N X. N ) )
8 1 7 matplusg 
 |-  ( ( N e. Fin /\ R e. _V ) -> ( +g ` ( R freeLMod ( N X. N ) ) ) = ( +g ` A ) )
9 8 3 eqtr4di 
 |-  ( ( N e. Fin /\ R e. _V ) -> ( +g ` ( R freeLMod ( N X. N ) ) ) = .+b )
10 6 9 syl 
 |-  ( ( X e. B /\ Y e. B ) -> ( +g ` ( R freeLMod ( N X. N ) ) ) = .+b )
11 10 oveqd 
 |-  ( ( X e. B /\ Y e. B ) -> ( X ( +g ` ( R freeLMod ( N X. N ) ) ) Y ) = ( X .+b Y ) )
12 eqid 
 |-  ( Base ` ( R freeLMod ( N X. N ) ) ) = ( Base ` ( R freeLMod ( N X. N ) ) )
13 6 simprd 
 |-  ( ( X e. B /\ Y e. B ) -> R e. _V )
14 6 simpld 
 |-  ( ( X e. B /\ Y e. B ) -> N e. Fin )
15 xpfi 
 |-  ( ( N e. Fin /\ N e. Fin ) -> ( N X. N ) e. Fin )
16 14 14 15 syl2anc 
 |-  ( ( X e. B /\ Y e. B ) -> ( N X. N ) e. Fin )
17 simpl 
 |-  ( ( X e. B /\ Y e. B ) -> X e. B )
18 1 7 matbas 
 |-  ( ( N e. Fin /\ R e. _V ) -> ( Base ` ( R freeLMod ( N X. N ) ) ) = ( Base ` A ) )
19 6 18 syl 
 |-  ( ( X e. B /\ Y e. B ) -> ( Base ` ( R freeLMod ( N X. N ) ) ) = ( Base ` A ) )
20 19 2 eqtr4di 
 |-  ( ( X e. B /\ Y e. B ) -> ( Base ` ( R freeLMod ( N X. N ) ) ) = B )
21 17 20 eleqtrrd 
 |-  ( ( X e. B /\ Y e. B ) -> X e. ( Base ` ( R freeLMod ( N X. N ) ) ) )
22 simpr 
 |-  ( ( X e. B /\ Y e. B ) -> Y e. B )
23 22 20 eleqtrrd 
 |-  ( ( X e. B /\ Y e. B ) -> Y e. ( Base ` ( R freeLMod ( N X. N ) ) ) )
24 eqid 
 |-  ( +g ` ( R freeLMod ( N X. N ) ) ) = ( +g ` ( R freeLMod ( N X. N ) ) )
25 7 12 13 16 21 23 4 24 frlmplusgval 
 |-  ( ( X e. B /\ Y e. B ) -> ( X ( +g ` ( R freeLMod ( N X. N ) ) ) Y ) = ( X oF .+ Y ) )
26 11 25 eqtr3d 
 |-  ( ( X e. B /\ Y e. B ) -> ( X .+b Y ) = ( X oF .+ Y ) )