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 ffvelcdmd 
 |-  ( ph -> ( O ` ( ( F ( quot1p ` R ) G ) ( .r ` P ) G ) ) e. ( Base ` ( R ^s K ) ) )
78 76 41 ffvelcdmd 
 |-  ( 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 ffvelcdmd 
 |-  ( ph -> ( O ` ( F ( quot1p ` R ) G ) ) e. ( Base ` ( R ^s K ) ) )
93 76 66 ffvelcdmd 
 |-  ( 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 ffvelcdmd 
 |-  ( 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 ffvelcdmd 
 |-  ( 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 ffvelcdm 
 |-  ( ( ( 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 ) ) )