This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem coe1addfv

Description: A particular coefficient of an addition. (Contributed by Stefan O'Rear, 23-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 coe1addfv 
|- ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ X e. NN0 ) -> ( ( coe1 ` ( F .+b G ) ) ` X ) = ( ( ( coe1 ` F ) ` X ) .+ ( ( coe1 ` G ) ` X ) ) )

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 1 2 3 4 coe1add 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( coe1 ` ( F .+b G ) ) = ( ( coe1 ` F ) oF .+ ( coe1 ` G ) ) )
6 5 adantr 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ X e. NN0 ) -> ( coe1 ` ( F .+b G ) ) = ( ( coe1 ` F ) oF .+ ( coe1 ` G ) ) )
7 6 fveq1d 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ X e. NN0 ) -> ( ( coe1 ` ( F .+b G ) ) ` X ) = ( ( ( coe1 ` F ) oF .+ ( coe1 ` G ) ) ` X ) )
8 eqid 
 |-  ( coe1 ` F ) = ( coe1 ` F )
9 eqid 
 |-  ( Base ` R ) = ( Base ` R )
10 8 2 1 9 coe1f 
 |-  ( F e. B -> ( coe1 ` F ) : NN0 --> ( Base ` R ) )
11 10 ffnd 
 |-  ( F e. B -> ( coe1 ` F ) Fn NN0 )
12 11 3ad2ant2 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( coe1 ` F ) Fn NN0 )
13 12 adantr 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ X e. NN0 ) -> ( coe1 ` F ) Fn NN0 )
14 eqid 
 |-  ( coe1 ` G ) = ( coe1 ` G )
15 14 2 1 9 coe1f 
 |-  ( G e. B -> ( coe1 ` G ) : NN0 --> ( Base ` R ) )
16 15 ffnd 
 |-  ( G e. B -> ( coe1 ` G ) Fn NN0 )
17 16 3ad2ant3 
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( coe1 ` G ) Fn NN0 )
18 17 adantr 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ X e. NN0 ) -> ( coe1 ` G ) Fn NN0 )
19 nn0ex 
 |-  NN0 e. _V
20 19 a1i 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ X e. NN0 ) -> NN0 e. _V )
21 simpr 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ X e. NN0 ) -> X e. NN0 )
22 fnfvof 
 |-  ( ( ( ( coe1 ` F ) Fn NN0 /\ ( coe1 ` G ) Fn NN0 ) /\ ( NN0 e. _V /\ X e. NN0 ) ) -> ( ( ( coe1 ` F ) oF .+ ( coe1 ` G ) ) ` X ) = ( ( ( coe1 ` F ) ` X ) .+ ( ( coe1 ` G ) ` X ) ) )
23 13 18 20 21 22 syl22anc 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ X e. NN0 ) -> ( ( ( coe1 ` F ) oF .+ ( coe1 ` G ) ) ` X ) = ( ( ( coe1 ` F ) ` X ) .+ ( ( coe1 ` G ) ` X ) ) )
24 7 23 eqtrd 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ X e. NN0 ) -> ( ( coe1 ` ( F .+b G ) ) ` X ) = ( ( ( coe1 ` F ) ` X ) .+ ( ( coe1 ` G ) ` X ) ) )