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