Metamath Proof Explorer


Theorem coe1subfv

Description: A particular coefficient of a subtraction. (Contributed by Stefan O'Rear, 23-Mar-2015)

Ref Expression
Hypotheses coe1sub.y
|- Y = ( Poly1 ` R )
coe1sub.b
|- B = ( Base ` Y )
coe1sub.p
|- .- = ( -g ` Y )
coe1sub.q
|- N = ( -g ` R )
Assertion coe1subfv
|- ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ X e. NN0 ) -> ( ( coe1 ` ( F .- G ) ) ` X ) = ( ( ( coe1 ` F ) ` X ) N ( ( coe1 ` G ) ` X ) ) )

Proof

Step Hyp Ref Expression
1 coe1sub.y
 |-  Y = ( Poly1 ` R )
2 coe1sub.b
 |-  B = ( Base ` Y )
3 coe1sub.p
 |-  .- = ( -g ` Y )
4 coe1sub.q
 |-  N = ( -g ` R )
5 simpl1
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ X e. NN0 ) -> R e. Ring )
6 1 ply1ring
 |-  ( R e. Ring -> Y e. Ring )
7 ringgrp
 |-  ( Y e. Ring -> Y e. Grp )
8 6 7 syl
 |-  ( R e. Ring -> Y e. Grp )
9 2 3 grpsubcl
 |-  ( ( Y e. Grp /\ F e. B /\ G e. B ) -> ( F .- G ) e. B )
10 8 9 syl3an1
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( F .- G ) e. B )
11 10 adantr
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ X e. NN0 ) -> ( F .- G ) e. B )
12 simpl3
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ X e. NN0 ) -> G e. B )
13 simpr
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ X e. NN0 ) -> X e. NN0 )
14 eqid
 |-  ( +g ` Y ) = ( +g ` Y )
15 eqid
 |-  ( +g ` R ) = ( +g ` R )
16 1 2 14 15 coe1addfv
 |-  ( ( ( R e. Ring /\ ( F .- G ) e. B /\ G e. B ) /\ X e. NN0 ) -> ( ( coe1 ` ( ( F .- G ) ( +g ` Y ) G ) ) ` X ) = ( ( ( coe1 ` ( F .- G ) ) ` X ) ( +g ` R ) ( ( coe1 ` G ) ` X ) ) )
17 5 11 12 13 16 syl31anc
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ X e. NN0 ) -> ( ( coe1 ` ( ( F .- G ) ( +g ` Y ) G ) ) ` X ) = ( ( ( coe1 ` ( F .- G ) ) ` X ) ( +g ` R ) ( ( coe1 ` G ) ` X ) ) )
18 8 3ad2ant1
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> Y e. Grp )
19 18 adantr
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ X e. NN0 ) -> Y e. Grp )
20 simpl2
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ X e. NN0 ) -> F e. B )
21 2 14 3 grpnpcan
 |-  ( ( Y e. Grp /\ F e. B /\ G e. B ) -> ( ( F .- G ) ( +g ` Y ) G ) = F )
22 19 20 12 21 syl3anc
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ X e. NN0 ) -> ( ( F .- G ) ( +g ` Y ) G ) = F )
23 22 fveq2d
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ X e. NN0 ) -> ( coe1 ` ( ( F .- G ) ( +g ` Y ) G ) ) = ( coe1 ` F ) )
24 23 fveq1d
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ X e. NN0 ) -> ( ( coe1 ` ( ( F .- G ) ( +g ` Y ) G ) ) ` X ) = ( ( coe1 ` F ) ` X ) )
25 17 24 eqtr3d
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ X e. NN0 ) -> ( ( ( coe1 ` ( F .- G ) ) ` X ) ( +g ` R ) ( ( coe1 ` G ) ` X ) ) = ( ( coe1 ` F ) ` X ) )
26 ringgrp
 |-  ( R e. Ring -> R e. Grp )
27 26 3ad2ant1
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> R e. Grp )
28 27 adantr
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ X e. NN0 ) -> R e. Grp )
29 eqid
 |-  ( coe1 ` F ) = ( coe1 ` F )
30 eqid
 |-  ( Base ` R ) = ( Base ` R )
31 29 2 1 30 coe1f
 |-  ( F e. B -> ( coe1 ` F ) : NN0 --> ( Base ` R ) )
32 31 3ad2ant2
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( coe1 ` F ) : NN0 --> ( Base ` R ) )
33 32 ffvelrnda
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ X e. NN0 ) -> ( ( coe1 ` F ) ` X ) e. ( Base ` R ) )
34 eqid
 |-  ( coe1 ` G ) = ( coe1 ` G )
35 34 2 1 30 coe1f
 |-  ( G e. B -> ( coe1 ` G ) : NN0 --> ( Base ` R ) )
36 35 3ad2ant3
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( coe1 ` G ) : NN0 --> ( Base ` R ) )
37 36 ffvelrnda
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ X e. NN0 ) -> ( ( coe1 ` G ) ` X ) e. ( Base ` R ) )
38 eqid
 |-  ( coe1 ` ( F .- G ) ) = ( coe1 ` ( F .- G ) )
39 38 2 1 30 coe1f
 |-  ( ( F .- G ) e. B -> ( coe1 ` ( F .- G ) ) : NN0 --> ( Base ` R ) )
40 10 39 syl
 |-  ( ( R e. Ring /\ F e. B /\ G e. B ) -> ( coe1 ` ( F .- G ) ) : NN0 --> ( Base ` R ) )
41 40 ffvelrnda
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ X e. NN0 ) -> ( ( coe1 ` ( F .- G ) ) ` X ) e. ( Base ` R ) )
42 30 15 4 grpsubadd
 |-  ( ( R e. Grp /\ ( ( ( coe1 ` F ) ` X ) e. ( Base ` R ) /\ ( ( coe1 ` G ) ` X ) e. ( Base ` R ) /\ ( ( coe1 ` ( F .- G ) ) ` X ) e. ( Base ` R ) ) ) -> ( ( ( ( coe1 ` F ) ` X ) N ( ( coe1 ` G ) ` X ) ) = ( ( coe1 ` ( F .- G ) ) ` X ) <-> ( ( ( coe1 ` ( F .- G ) ) ` X ) ( +g ` R ) ( ( coe1 ` G ) ` X ) ) = ( ( coe1 ` F ) ` X ) ) )
43 28 33 37 41 42 syl13anc
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ X e. NN0 ) -> ( ( ( ( coe1 ` F ) ` X ) N ( ( coe1 ` G ) ` X ) ) = ( ( coe1 ` ( F .- G ) ) ` X ) <-> ( ( ( coe1 ` ( F .- G ) ) ` X ) ( +g ` R ) ( ( coe1 ` G ) ` X ) ) = ( ( coe1 ` F ) ` X ) ) )
44 25 43 mpbird
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ X e. NN0 ) -> ( ( ( coe1 ` F ) ` X ) N ( ( coe1 ` G ) ` X ) ) = ( ( coe1 ` ( F .- G ) ) ` X ) )
45 44 eqcomd
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. B ) /\ X e. NN0 ) -> ( ( coe1 ` ( F .- G ) ) ` X ) = ( ( ( coe1 ` F ) ` X ) N ( ( coe1 ` G ) ` X ) ) )