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

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 ffvelcdmda 
 |-  ( ( ( 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 ffvelcdmda 
 |-  ( ( ( 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 ffvelcdmda 
 |-  ( ( ( 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 ) ) )