Metamath Proof Explorer

Theorem coe1add

Description: The coefficient vector of an addition. (Contributed by Stefan O'Rear, 24-Mar-2015)

Ref Expression
Hypotheses coe1add.y 
|- Y = ( Poly1 ` R )
coe1add.b 
|- B = ( Base ` Y )
coe1add.p 
|- .+b = ( +g ` Y )
coe1add.q 
|- .+ = ( +g ` R )
Assertion coe1add 
|- ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( coe1 ` ( F .+b G ) ) = ( ( coe1 ` F ) oF .+ ( coe1 ` G ) ) )

Proof

Step Hyp Ref Expression
1 coe1add.y 
 |-  Y = ( Poly1 ` R )
2 coe1add.b 
 |-  B = ( Base ` Y )
3 coe1add.p 
 |-  .+b = ( +g ` Y )
4 coe1add.q 
 |-  .+ = ( +g ` R )
5 eqid 
 |-  ( 1o mPoly R ) = ( 1o mPoly R )
6 eqid 
 |-  ( PwSer1 ` R ) = ( PwSer1 ` R )
7 1 6 2 ply1bas 
 |-  B = ( Base ` ( 1o mPoly R ) )
8 1 5 3 ply1plusg 
 |-  .+b = ( +g ` ( 1o mPoly R ) )
9 simp2 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> F e. B )
10 simp3 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> G e. B )
11 5 7 4 8 9 10 mpladd 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( F .+b G ) = ( F oF .+ G ) )
12 11 coeq1d 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( ( F .+b G ) o. ( a e. NN0 |-> ( 1o X. { a } ) ) ) = ( ( F oF .+ G ) o. ( a e. NN0 |-> ( 1o X. { a } ) ) ) )
13 eqid 
 |-  ( Base ` R ) = ( Base ` R )
14 1 2 13 ply1basf 
 |-  ( F e. B -> F : ( NN0 ^m 1o ) --> ( Base ` R ) )
15 14 ffnd 
 |-  ( F e. B -> F Fn ( NN0 ^m 1o ) )
16 15 3ad2ant2 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> F Fn ( NN0 ^m 1o ) )
17 1 2 13 ply1basf 
 |-  ( G e. B -> G : ( NN0 ^m 1o ) --> ( Base ` R ) )
18 17 ffnd 
 |-  ( G e. B -> G Fn ( NN0 ^m 1o ) )
19 18 3ad2ant3 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> G Fn ( NN0 ^m 1o ) )
20 df1o2 
 |-  1o = { (/) }
21 nn0ex 
 |-  NN0 e. _V
22 0ex 
 |-  (/) e. _V
23 eqid 
 |-  ( a e. NN0 |-> ( 1o X. { a } ) ) = ( a e. NN0 |-> ( 1o X. { a } ) )
24 20 21 22 23 mapsnf1o3 
 |-  ( a e. NN0 |-> ( 1o X. { a } ) ) : NN0 -1-1-onto-> ( NN0 ^m 1o )
25 f1of 
 |-  ( ( a e. NN0 |-> ( 1o X. { a } ) ) : NN0 -1-1-onto-> ( NN0 ^m 1o ) -> ( a e. NN0 |-> ( 1o X. { a } ) ) : NN0 --> ( NN0 ^m 1o ) )
26 24 25 mp1i 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( a e. NN0 |-> ( 1o X. { a } ) ) : NN0 --> ( NN0 ^m 1o ) )
27 ovexd 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( NN0 ^m 1o ) e. _V )
28 21 a1i 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> NN0 e. _V )
29 inidm 
 |-  ( ( NN0 ^m 1o ) i^i ( NN0 ^m 1o ) ) = ( NN0 ^m 1o )
30 16 19 26 27 27 28 29 ofco 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( ( F oF .+ G ) o. ( a e. NN0 |-> ( 1o X. { a } ) ) ) = ( ( F o. ( a e. NN0 |-> ( 1o X. { a } ) ) ) oF .+ ( G o. ( a e. NN0 |-> ( 1o X. { a } ) ) ) ) )
31 12 30 eqtrd 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( ( F .+b G ) o. ( a e. NN0 |-> ( 1o X. { a } ) ) ) = ( ( F o. ( a e. NN0 |-> ( 1o X. { a } ) ) ) oF .+ ( G o. ( a e. NN0 |-> ( 1o X. { a } ) ) ) ) )
32 1 ply1ring 
 |-  ( R e. Ring -> Y e. Ring )
33 2 3 ringacl 
 |-  ( ( Y e. Ring /\ F e. B /\ G e. B ) -> ( F .+b G ) e. B )
34 32 33 syl3an1 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( F .+b G ) e. B )
35 eqid 
 |-  ( coe1 ` ( F .+b G ) ) = ( coe1 ` ( F .+b G ) )
36 35 2 1 23 coe1fval2 
 |-  ( ( F .+b G ) e. B -> ( coe1 ` ( F .+b G ) ) = ( ( F .+b G ) o. ( a e. NN0 |-> ( 1o X. { a } ) ) ) )
37 34 36 syl 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( coe1 ` ( F .+b G ) ) = ( ( F .+b G ) o. ( a e. NN0 |-> ( 1o X. { a } ) ) ) )
38 eqid 
 |-  ( coe1 ` F ) = ( coe1 ` F )
39 38 2 1 23 coe1fval2 
 |-  ( F e. B -> ( coe1 ` F ) = ( F o. ( a e. NN0 |-> ( 1o X. { a } ) ) ) )
40 39 3ad2ant2 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( coe1 ` F ) = ( F o. ( a e. NN0 |-> ( 1o X. { a } ) ) ) )
41 eqid 
 |-  ( coe1 ` G ) = ( coe1 ` G )
42 41 2 1 23 coe1fval2 
 |-  ( G e. B -> ( coe1 ` G ) = ( G o. ( a e. NN0 |-> ( 1o X. { a } ) ) ) )
43 42 3ad2ant3 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( coe1 ` G ) = ( G o. ( a e. NN0 |-> ( 1o X. { a } ) ) ) )
44 40 43 oveq12d 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( ( coe1 ` F ) oF .+ ( coe1 ` G ) ) = ( ( F o. ( a e. NN0 |-> ( 1o X. { a } ) ) ) oF .+ ( G o. ( a e. NN0 |-> ( 1o X. { a } ) ) ) ) )
45 31 37 44 3eqtr4d 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( coe1 ` ( F .+b G ) ) = ( ( coe1 ` F ) oF .+ ( coe1 ` G ) ) )