Metamath Proof Explorer


Theorem ply1rem

Description: The polynomial remainder theorem, or little Bézout's theorem (by contrast to the regular Bézout's theorem bezout ). If a polynomial F is divided by the linear factor x - A , the remainder is equal to F ( A ) , the evaluation of the polynomial at A (interpreted as a constant polynomial). (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses ply1rem.p
|- P = ( Poly1 ` R )
ply1rem.b
|- B = ( Base ` P )
ply1rem.k
|- K = ( Base ` R )
ply1rem.x
|- X = ( var1 ` R )
ply1rem.m
|- .- = ( -g ` P )
ply1rem.a
|- A = ( algSc ` P )
ply1rem.g
|- G = ( X .- ( A ` N ) )
ply1rem.o
|- O = ( eval1 ` R )
ply1rem.1
|- ( ph -> R e. NzRing )
ply1rem.2
|- ( ph -> R e. CRing )
ply1rem.3
|- ( ph -> N e. K )
ply1rem.4
|- ( ph -> F e. B )
ply1rem.e
|- E = ( rem1p ` R )
Assertion ply1rem
|- ( ph -> ( F E G ) = ( A ` ( ( O ` F ) ` N ) ) )

Proof

Step Hyp Ref Expression
1 ply1rem.p
 |-  P = ( Poly1 ` R )
2 ply1rem.b
 |-  B = ( Base ` P )
3 ply1rem.k
 |-  K = ( Base ` R )
4 ply1rem.x
 |-  X = ( var1 ` R )
5 ply1rem.m
 |-  .- = ( -g ` P )
6 ply1rem.a
 |-  A = ( algSc ` P )
7 ply1rem.g
 |-  G = ( X .- ( A ` N ) )
8 ply1rem.o
 |-  O = ( eval1 ` R )
9 ply1rem.1
 |-  ( ph -> R e. NzRing )
10 ply1rem.2
 |-  ( ph -> R e. CRing )
11 ply1rem.3
 |-  ( ph -> N e. K )
12 ply1rem.4
 |-  ( ph -> F e. B )
13 ply1rem.e
 |-  E = ( rem1p ` R )
14 nzrring
 |-  ( R e. NzRing -> R e. Ring )
15 9 14 syl
 |-  ( ph -> R e. Ring )
16 eqid
 |-  ( Monic1p ` R ) = ( Monic1p ` R )
17 eqid
 |-  ( deg1 ` R ) = ( deg1 ` R )
18 eqid
 |-  ( 0g ` R ) = ( 0g ` R )
19 1 2 3 4 5 6 7 8 9 10 11 16 17 18 ply1remlem
 |-  ( ph -> ( G e. ( Monic1p ` R ) /\ ( ( deg1 ` R ) ` G ) = 1 /\ ( `' ( O ` G ) " { ( 0g ` R ) } ) = { N } ) )
20 19 simp1d
 |-  ( ph -> G e. ( Monic1p ` R ) )
21 eqid
 |-  ( Unic1p ` R ) = ( Unic1p ` R )
22 21 16 mon1puc1p
 |-  ( ( R e. Ring /\ G e. ( Monic1p ` R ) ) -> G e. ( Unic1p ` R ) )
23 15 20 22 syl2anc
 |-  ( ph -> G e. ( Unic1p ` R ) )
24 13 1 2 21 17 r1pdeglt
 |-  ( ( R e. Ring /\ F e. B /\ G e. ( Unic1p ` R ) ) -> ( ( deg1 ` R ) ` ( F E G ) ) < ( ( deg1 ` R ) ` G ) )
25 15 12 23 24 syl3anc
 |-  ( ph -> ( ( deg1 ` R ) ` ( F E G ) ) < ( ( deg1 ` R ) ` G ) )
26 19 simp2d
 |-  ( ph -> ( ( deg1 ` R ) ` G ) = 1 )
27 25 26 breqtrd
 |-  ( ph -> ( ( deg1 ` R ) ` ( F E G ) ) < 1 )
28 1e0p1
 |-  1 = ( 0 + 1 )
29 27 28 breqtrdi
 |-  ( ph -> ( ( deg1 ` R ) ` ( F E G ) ) < ( 0 + 1 ) )
30 0nn0
 |-  0 e. NN0
31 nn0leltp1
 |-  ( ( ( ( deg1 ` R ) ` ( F E G ) ) e. NN0 /\ 0 e. NN0 ) -> ( ( ( deg1 ` R ) ` ( F E G ) ) <_ 0 <-> ( ( deg1 ` R ) ` ( F E G ) ) < ( 0 + 1 ) ) )
32 30 31 mpan2
 |-  ( ( ( deg1 ` R ) ` ( F E G ) ) e. NN0 -> ( ( ( deg1 ` R ) ` ( F E G ) ) <_ 0 <-> ( ( deg1 ` R ) ` ( F E G ) ) < ( 0 + 1 ) ) )
33 29 32 syl5ibrcom
 |-  ( ph -> ( ( ( deg1 ` R ) ` ( F E G ) ) e. NN0 -> ( ( deg1 ` R ) ` ( F E G ) ) <_ 0 ) )
34 elsni
 |-  ( ( ( deg1 ` R ) ` ( F E G ) ) e. { -oo } -> ( ( deg1 ` R ) ` ( F E G ) ) = -oo )
35 0xr
 |-  0 e. RR*
36 mnfle
 |-  ( 0 e. RR* -> -oo <_ 0 )
37 35 36 ax-mp
 |-  -oo <_ 0
38 34 37 eqbrtrdi
 |-  ( ( ( deg1 ` R ) ` ( F E G ) ) e. { -oo } -> ( ( deg1 ` R ) ` ( F E G ) ) <_ 0 )
39 38 a1i
 |-  ( ph -> ( ( ( deg1 ` R ) ` ( F E G ) ) e. { -oo } -> ( ( deg1 ` R ) ` ( F E G ) ) <_ 0 ) )
40 13 1 2 21 r1pcl
 |-  ( ( R e. Ring /\ F e. B /\ G e. ( Unic1p ` R ) ) -> ( F E G ) e. B )
41 15 12 23 40 syl3anc
 |-  ( ph -> ( F E G ) e. B )
42 17 1 2 deg1cl
 |-  ( ( F E G ) e. B -> ( ( deg1 ` R ) ` ( F E G ) ) e. ( NN0 u. { -oo } ) )
43 41 42 syl
 |-  ( ph -> ( ( deg1 ` R ) ` ( F E G ) ) e. ( NN0 u. { -oo } ) )
44 elun
 |-  ( ( ( deg1 ` R ) ` ( F E G ) ) e. ( NN0 u. { -oo } ) <-> ( ( ( deg1 ` R ) ` ( F E G ) ) e. NN0 \/ ( ( deg1 ` R ) ` ( F E G ) ) e. { -oo } ) )
45 43 44 sylib
 |-  ( ph -> ( ( ( deg1 ` R ) ` ( F E G ) ) e. NN0 \/ ( ( deg1 ` R ) ` ( F E G ) ) e. { -oo } ) )
46 33 39 45 mpjaod
 |-  ( ph -> ( ( deg1 ` R ) ` ( F E G ) ) <_ 0 )
47 17 1 2 6 deg1le0
 |-  ( ( R e. Ring /\ ( F E G ) e. B ) -> ( ( ( deg1 ` R ) ` ( F E G ) ) <_ 0 <-> ( F E G ) = ( A ` ( ( coe1 ` ( F E G ) ) ` 0 ) ) ) )
48 15 41 47 syl2anc
 |-  ( ph -> ( ( ( deg1 ` R ) ` ( F E G ) ) <_ 0 <-> ( F E G ) = ( A ` ( ( coe1 ` ( F E G ) ) ` 0 ) ) ) )
49 46 48 mpbid
 |-  ( ph -> ( F E G ) = ( A ` ( ( coe1 ` ( F E G ) ) ` 0 ) ) )
50 eqid
 |-  ( quot1p ` R ) = ( quot1p ` R )
51 eqid
 |-  ( .r ` P ) = ( .r ` P )
52 eqid
 |-  ( +g ` P ) = ( +g ` P )
53 1 2 21 50 13 51 52 r1pid
 |-  ( ( R e. Ring /\ F e. B /\ G e. ( Unic1p ` R ) ) -> F = ( ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ( +g ` P ) ( F E G ) ) )
54 15 12 23 53 syl3anc
 |-  ( ph -> F = ( ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ( +g ` P ) ( F E G ) ) )
55 54 fveq2d
 |-  ( ph -> ( O ` F ) = ( O ` ( ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ( +g ` P ) ( F E G ) ) ) )
56 eqid
 |-  ( R ^s K ) = ( R ^s K )
57 8 1 56 3 evl1rhm
 |-  ( R e. CRing -> O e. ( P RingHom ( R ^s K ) ) )
58 10 57 syl
 |-  ( ph -> O e. ( P RingHom ( R ^s K ) ) )
59 rhmghm
 |-  ( O e. ( P RingHom ( R ^s K ) ) -> O e. ( P GrpHom ( R ^s K ) ) )
60 58 59 syl
 |-  ( ph -> O e. ( P GrpHom ( R ^s K ) ) )
61 1 ply1ring
 |-  ( R e. Ring -> P e. Ring )
62 15 61 syl
 |-  ( ph -> P e. Ring )
63 50 1 2 21 q1pcl
 |-  ( ( R e. Ring /\ F e. B /\ G e. ( Unic1p ` R ) ) -> ( F ( quot1p ` R ) G ) e. B )
64 15 12 23 63 syl3anc
 |-  ( ph -> ( F ( quot1p ` R ) G ) e. B )
65 1 2 16 mon1pcl
 |-  ( G e. ( Monic1p ` R ) -> G e. B )
66 20 65 syl
 |-  ( ph -> G e. B )
67 2 51 ringcl
 |-  ( ( P e. Ring /\ ( F ( quot1p ` R ) G ) e. B /\ G e. B ) -> ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) e. B )
68 62 64 66 67 syl3anc
 |-  ( ph -> ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) e. B )
69 eqid
 |-  ( +g ` ( R ^s K ) ) = ( +g ` ( R ^s K ) )
70 2 52 69 ghmlin
 |-  ( ( O e. ( P GrpHom ( R ^s K ) ) /\ ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) e. B /\ ( F E G ) e. B ) -> ( O ` ( ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ( +g ` P ) ( F E G ) ) ) = ( ( O ` ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) ( +g ` ( R ^s K ) ) ( O ` ( F E G ) ) ) )
71 60 68 41 70 syl3anc
 |-  ( ph -> ( O ` ( ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ( +g ` P ) ( F E G ) ) ) = ( ( O ` ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) ( +g ` ( R ^s K ) ) ( O ` ( F E G ) ) ) )
72 eqid
 |-  ( Base ` ( R ^s K ) ) = ( Base ` ( R ^s K ) )
73 3 fvexi
 |-  K e. _V
74 73 a1i
 |-  ( ph -> K e. _V )
75 2 72 rhmf
 |-  ( O e. ( P RingHom ( R ^s K ) ) -> O : B --> ( Base ` ( R ^s K ) ) )
76 58 75 syl
 |-  ( ph -> O : B --> ( Base ` ( R ^s K ) ) )
77 76 68 ffvelrnd
 |-  ( ph -> ( O ` ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) e. ( Base ` ( R ^s K ) ) )
78 76 41 ffvelrnd
 |-  ( ph -> ( O ` ( F E G ) ) e. ( Base ` ( R ^s K ) ) )
79 eqid
 |-  ( +g ` R ) = ( +g ` R )
80 56 72 9 74 77 78 79 69 pwsplusgval
 |-  ( ph -> ( ( O ` ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) ( +g ` ( R ^s K ) ) ( O ` ( F E G ) ) ) = ( ( O ` ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) oF ( +g ` R ) ( O ` ( F E G ) ) ) )
81 55 71 80 3eqtrd
 |-  ( ph -> ( O ` F ) = ( ( O ` ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) oF ( +g ` R ) ( O ` ( F E G ) ) ) )
82 81 fveq1d
 |-  ( ph -> ( ( O ` F ) ` N ) = ( ( ( O ` ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) oF ( +g ` R ) ( O ` ( F E G ) ) ) ` N ) )
83 56 3 72 9 74 77 pwselbas
 |-  ( ph -> ( O ` ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) : K --> K )
84 83 ffnd
 |-  ( ph -> ( O ` ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) Fn K )
85 56 3 72 9 74 78 pwselbas
 |-  ( ph -> ( O ` ( F E G ) ) : K --> K )
86 85 ffnd
 |-  ( ph -> ( O ` ( F E G ) ) Fn K )
87 fnfvof
 |-  ( ( ( ( O ` ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) Fn K /\ ( O ` ( F E G ) ) Fn K ) /\ ( K e. _V /\ N e. K ) ) -> ( ( ( O ` ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) oF ( +g ` R ) ( O ` ( F E G ) ) ) ` N ) = ( ( ( O ` ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) ` N ) ( +g ` R ) ( ( O ` ( F E G ) ) ` N ) ) )
88 84 86 74 11 87 syl22anc
 |-  ( ph -> ( ( ( O ` ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) oF ( +g ` R ) ( O ` ( F E G ) ) ) ` N ) = ( ( ( O ` ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) ` N ) ( +g ` R ) ( ( O ` ( F E G ) ) ` N ) ) )
89 eqid
 |-  ( .r ` ( R ^s K ) ) = ( .r ` ( R ^s K ) )
90 2 51 89 rhmmul
 |-  ( ( O e. ( P RingHom ( R ^s K ) ) /\ ( F ( quot1p ` R ) G ) e. B /\ G e. B ) -> ( O ` ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) = ( ( O ` ( F ( quot1p ` R ) G ) ) ( .r ` ( R ^s K ) ) ( O ` G ) ) )
91 58 64 66 90 syl3anc
 |-  ( ph -> ( O ` ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) = ( ( O ` ( F ( quot1p ` R ) G ) ) ( .r ` ( R ^s K ) ) ( O ` G ) ) )
92 76 64 ffvelrnd
 |-  ( ph -> ( O ` ( F ( quot1p ` R ) G ) ) e. ( Base ` ( R ^s K ) ) )
93 76 66 ffvelrnd
 |-  ( ph -> ( O ` G ) e. ( Base ` ( R ^s K ) ) )
94 eqid
 |-  ( .r ` R ) = ( .r ` R )
95 56 72 9 74 92 93 94 89 pwsmulrval
 |-  ( ph -> ( ( O ` ( F ( quot1p ` R ) G ) ) ( .r ` ( R ^s K ) ) ( O ` G ) ) = ( ( O ` ( F ( quot1p ` R ) G ) ) oF ( .r ` R ) ( O ` G ) ) )
96 91 95 eqtrd
 |-  ( ph -> ( O ` ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) = ( ( O ` ( F ( quot1p ` R ) G ) ) oF ( .r ` R ) ( O ` G ) ) )
97 96 fveq1d
 |-  ( ph -> ( ( O ` ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) ` N ) = ( ( ( O ` ( F ( quot1p ` R ) G ) ) oF ( .r ` R ) ( O ` G ) ) ` N ) )
98 56 3 72 9 74 92 pwselbas
 |-  ( ph -> ( O ` ( F ( quot1p ` R ) G ) ) : K --> K )
99 98 ffnd
 |-  ( ph -> ( O ` ( F ( quot1p ` R ) G ) ) Fn K )
100 56 3 72 9 74 93 pwselbas
 |-  ( ph -> ( O ` G ) : K --> K )
101 100 ffnd
 |-  ( ph -> ( O ` G ) Fn K )
102 fnfvof
 |-  ( ( ( ( O ` ( F ( quot1p ` R ) G ) ) Fn K /\ ( O ` G ) Fn K ) /\ ( K e. _V /\ N e. K ) ) -> ( ( ( O ` ( F ( quot1p ` R ) G ) ) oF ( .r ` R ) ( O ` G ) ) ` N ) = ( ( ( O ` ( F ( quot1p ` R ) G ) ) ` N ) ( .r ` R ) ( ( O ` G ) ` N ) ) )
103 99 101 74 11 102 syl22anc
 |-  ( ph -> ( ( ( O ` ( F ( quot1p ` R ) G ) ) oF ( .r ` R ) ( O ` G ) ) ` N ) = ( ( ( O ` ( F ( quot1p ` R ) G ) ) ` N ) ( .r ` R ) ( ( O ` G ) ` N ) ) )
104 snidg
 |-  ( N e. K -> N e. { N } )
105 11 104 syl
 |-  ( ph -> N e. { N } )
106 19 simp3d
 |-  ( ph -> ( `' ( O ` G ) " { ( 0g ` R ) } ) = { N } )
107 105 106 eleqtrrd
 |-  ( ph -> N e. ( `' ( O ` G ) " { ( 0g ` R ) } ) )
108 fniniseg
 |-  ( ( O ` G ) Fn K -> ( N e. ( `' ( O ` G ) " { ( 0g ` R ) } ) <-> ( N e. K /\ ( ( O ` G ) ` N ) = ( 0g ` R ) ) ) )
109 101 108 syl
 |-  ( ph -> ( N e. ( `' ( O ` G ) " { ( 0g ` R ) } ) <-> ( N e. K /\ ( ( O ` G ) ` N ) = ( 0g ` R ) ) ) )
110 107 109 mpbid
 |-  ( ph -> ( N e. K /\ ( ( O ` G ) ` N ) = ( 0g ` R ) ) )
111 110 simprd
 |-  ( ph -> ( ( O ` G ) ` N ) = ( 0g ` R ) )
112 111 oveq2d
 |-  ( ph -> ( ( ( O ` ( F ( quot1p ` R ) G ) ) ` N ) ( .r ` R ) ( ( O ` G ) ` N ) ) = ( ( ( O ` ( F ( quot1p ` R ) G ) ) ` N ) ( .r ` R ) ( 0g ` R ) ) )
113 98 11 ffvelrnd
 |-  ( ph -> ( ( O ` ( F ( quot1p ` R ) G ) ) ` N ) e. K )
114 3 94 18 ringrz
 |-  ( ( R e. Ring /\ ( ( O ` ( F ( quot1p ` R ) G ) ) ` N ) e. K ) -> ( ( ( O ` ( F ( quot1p ` R ) G ) ) ` N ) ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
115 15 113 114 syl2anc
 |-  ( ph -> ( ( ( O ` ( F ( quot1p ` R ) G ) ) ` N ) ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
116 112 115 eqtrd
 |-  ( ph -> ( ( ( O ` ( F ( quot1p ` R ) G ) ) ` N ) ( .r ` R ) ( ( O ` G ) ` N ) ) = ( 0g ` R ) )
117 97 103 116 3eqtrd
 |-  ( ph -> ( ( O ` ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) ` N ) = ( 0g ` R ) )
118 117 oveq1d
 |-  ( ph -> ( ( ( O ` ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) ` N ) ( +g ` R ) ( ( O ` ( F E G ) ) ` N ) ) = ( ( 0g ` R ) ( +g ` R ) ( ( O ` ( F E G ) ) ` N ) ) )
119 ringgrp
 |-  ( R e. Ring -> R e. Grp )
120 15 119 syl
 |-  ( ph -> R e. Grp )
121 85 11 ffvelrnd
 |-  ( ph -> ( ( O ` ( F E G ) ) ` N ) e. K )
122 3 79 18 grplid
 |-  ( ( R e. Grp /\ ( ( O ` ( F E G ) ) ` N ) e. K ) -> ( ( 0g ` R ) ( +g ` R ) ( ( O ` ( F E G ) ) ` N ) ) = ( ( O ` ( F E G ) ) ` N ) )
123 120 121 122 syl2anc
 |-  ( ph -> ( ( 0g ` R ) ( +g ` R ) ( ( O ` ( F E G ) ) ` N ) ) = ( ( O ` ( F E G ) ) ` N ) )
124 88 118 123 3eqtrd
 |-  ( ph -> ( ( ( O ` ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) oF ( +g ` R ) ( O ` ( F E G ) ) ) ` N ) = ( ( O ` ( F E G ) ) ` N ) )
125 49 fveq2d
 |-  ( ph -> ( O ` ( F E G ) ) = ( O ` ( A ` ( ( coe1 ` ( F E G ) ) ` 0 ) ) ) )
126 eqid
 |-  ( coe1 ` ( F E G ) ) = ( coe1 ` ( F E G ) )
127 126 2 1 3 coe1f
 |-  ( ( F E G ) e. B -> ( coe1 ` ( F E G ) ) : NN0 --> K )
128 41 127 syl
 |-  ( ph -> ( coe1 ` ( F E G ) ) : NN0 --> K )
129 ffvelrn
 |-  ( ( ( coe1 ` ( F E G ) ) : NN0 --> K /\ 0 e. NN0 ) -> ( ( coe1 ` ( F E G ) ) ` 0 ) e. K )
130 128 30 129 sylancl
 |-  ( ph -> ( ( coe1 ` ( F E G ) ) ` 0 ) e. K )
131 8 1 3 6 evl1sca
 |-  ( ( R e. CRing /\ ( ( coe1 ` ( F E G ) ) ` 0 ) e. K ) -> ( O ` ( A ` ( ( coe1 ` ( F E G ) ) ` 0 ) ) ) = ( K X. { ( ( coe1 ` ( F E G ) ) ` 0 ) } ) )
132 10 130 131 syl2anc
 |-  ( ph -> ( O ` ( A ` ( ( coe1 ` ( F E G ) ) ` 0 ) ) ) = ( K X. { ( ( coe1 ` ( F E G ) ) ` 0 ) } ) )
133 125 132 eqtrd
 |-  ( ph -> ( O ` ( F E G ) ) = ( K X. { ( ( coe1 ` ( F E G ) ) ` 0 ) } ) )
134 133 fveq1d
 |-  ( ph -> ( ( O ` ( F E G ) ) ` N ) = ( ( K X. { ( ( coe1 ` ( F E G ) ) ` 0 ) } ) ` N ) )
135 fvex
 |-  ( ( coe1 ` ( F E G ) ) ` 0 ) e. _V
136 135 fvconst2
 |-  ( N e. K -> ( ( K X. { ( ( coe1 ` ( F E G ) ) ` 0 ) } ) ` N ) = ( ( coe1 ` ( F E G ) ) ` 0 ) )
137 11 136 syl
 |-  ( ph -> ( ( K X. { ( ( coe1 ` ( F E G ) ) ` 0 ) } ) ` N ) = ( ( coe1 ` ( F E G ) ) ` 0 ) )
138 134 137 eqtrd
 |-  ( ph -> ( ( O ` ( F E G ) ) ` N ) = ( ( coe1 ` ( F E G ) ) ` 0 ) )
139 82 124 138 3eqtrd
 |-  ( ph -> ( ( O ` F ) ` N ) = ( ( coe1 ` ( F E G ) ) ` 0 ) )
140 139 fveq2d
 |-  ( ph -> ( A ` ( ( O ` F ) ` N ) ) = ( A ` ( ( coe1 ` ( F E G ) ) ` 0 ) ) )
141 49 140 eqtr4d
 |-  ( ph -> ( F E G ) = ( A ` ( ( O ` F ) ` N ) ) )