Step |
Hyp |
Ref |
Expression |
1 |
|
pf1ind.cb |
โข ๐ต = ( Base โ ๐
) |
2 |
|
pf1ind.cp |
โข + = ( +g โ ๐
) |
3 |
|
pf1ind.ct |
โข ยท = ( .r โ ๐
) |
4 |
|
pf1ind.cq |
โข ๐ = ran ( eval1 โ ๐
) |
5 |
|
pf1ind.ad |
โข ( ( ๐ โง ( ( ๐ โ ๐ โง ๐ ) โง ( ๐ โ ๐ โง ๐ ) ) ) โ ๐ ) |
6 |
|
pf1ind.mu |
โข ( ( ๐ โง ( ( ๐ โ ๐ โง ๐ ) โง ( ๐ โ ๐ โง ๐ ) ) ) โ ๐ ) |
7 |
|
pf1ind.wa |
โข ( ๐ฅ = ( ๐ต ร { ๐ } ) โ ( ๐ โ ๐ ) ) |
8 |
|
pf1ind.wb |
โข ( ๐ฅ = ( I โพ ๐ต ) โ ( ๐ โ ๐ ) ) |
9 |
|
pf1ind.wc |
โข ( ๐ฅ = ๐ โ ( ๐ โ ๐ ) ) |
10 |
|
pf1ind.wd |
โข ( ๐ฅ = ๐ โ ( ๐ โ ๐ ) ) |
11 |
|
pf1ind.we |
โข ( ๐ฅ = ( ๐ โf + ๐ ) โ ( ๐ โ ๐ ) ) |
12 |
|
pf1ind.wf |
โข ( ๐ฅ = ( ๐ โf ยท ๐ ) โ ( ๐ โ ๐ ) ) |
13 |
|
pf1ind.wg |
โข ( ๐ฅ = ๐ด โ ( ๐ โ ๐ ) ) |
14 |
|
pf1ind.co |
โข ( ( ๐ โง ๐ โ ๐ต ) โ ๐ ) |
15 |
|
pf1ind.pr |
โข ( ๐ โ ๐ ) |
16 |
|
pf1ind.a |
โข ( ๐ โ ๐ด โ ๐ ) |
17 |
|
coass |
โข ( ( ๐ด โ ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ โ
) ) ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) = ( ๐ด โ ( ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ โ
) ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) ) |
18 |
|
df1o2 |
โข 1o = { โ
} |
19 |
1
|
fvexi |
โข ๐ต โ V |
20 |
|
0ex |
โข โ
โ V |
21 |
|
eqid |
โข ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ โ
) ) = ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ โ
) ) |
22 |
18 19 20 21
|
mapsncnv |
โข โก ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ โ
) ) = ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) |
23 |
22
|
coeq2i |
โข ( ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ โ
) ) โ โก ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ โ
) ) ) = ( ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ โ
) ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) |
24 |
18 19 20 21
|
mapsnf1o2 |
โข ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ โ
) ) : ( ๐ต โm 1o ) โ1-1-ontoโ ๐ต |
25 |
|
f1ococnv2 |
โข ( ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ โ
) ) : ( ๐ต โm 1o ) โ1-1-ontoโ ๐ต โ ( ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ โ
) ) โ โก ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ โ
) ) ) = ( I โพ ๐ต ) ) |
26 |
24 25
|
mp1i |
โข ( ๐ โ ( ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ โ
) ) โ โก ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ โ
) ) ) = ( I โพ ๐ต ) ) |
27 |
23 26
|
eqtr3id |
โข ( ๐ โ ( ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ โ
) ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) = ( I โพ ๐ต ) ) |
28 |
27
|
coeq2d |
โข ( ๐ โ ( ๐ด โ ( ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ โ
) ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) ) = ( ๐ด โ ( I โพ ๐ต ) ) ) |
29 |
17 28
|
eqtrid |
โข ( ๐ โ ( ( ๐ด โ ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ โ
) ) ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) = ( ๐ด โ ( I โพ ๐ต ) ) ) |
30 |
4 1
|
pf1f |
โข ( ๐ด โ ๐ โ ๐ด : ๐ต โถ ๐ต ) |
31 |
|
fcoi1 |
โข ( ๐ด : ๐ต โถ ๐ต โ ( ๐ด โ ( I โพ ๐ต ) ) = ๐ด ) |
32 |
16 30 31
|
3syl |
โข ( ๐ โ ( ๐ด โ ( I โพ ๐ต ) ) = ๐ด ) |
33 |
29 32
|
eqtrd |
โข ( ๐ โ ( ( ๐ด โ ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ โ
) ) ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) = ๐ด ) |
34 |
|
eqid |
โข ( 1o eval ๐
) = ( 1o eval ๐
) |
35 |
34 1
|
evlval |
โข ( 1o eval ๐
) = ( ( 1o evalSub ๐
) โ ๐ต ) |
36 |
35
|
rneqi |
โข ran ( 1o eval ๐
) = ran ( ( 1o evalSub ๐
) โ ๐ต ) |
37 |
|
an4 |
โข ( ( ( ๐ โ ran ( 1o eval ๐
) โง ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) โง ( ๐ โ ran ( 1o eval ๐
) โง ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) ) โ ( ( ๐ โ ran ( 1o eval ๐
) โง ๐ โ ran ( 1o eval ๐
) ) โง ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โง ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) ) ) |
38 |
|
eqid |
โข ran ( 1o eval ๐
) = ran ( 1o eval ๐
) |
39 |
4 1 38
|
mpfpf1 |
โข ( ๐ โ ran ( 1o eval ๐
) โ ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ ๐ ) |
40 |
4 1 38
|
mpfpf1 |
โข ( ๐ โ ran ( 1o eval ๐
) โ ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ ๐ ) |
41 |
|
vex |
โข ๐ โ V |
42 |
41 9
|
elab |
โข ( ๐ โ { ๐ฅ โฃ ๐ } โ ๐ ) |
43 |
|
eleq1 |
โข ( ๐ = ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ ( ๐ โ { ๐ฅ โฃ ๐ } โ ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) ) |
44 |
42 43
|
bitr3id |
โข ( ๐ = ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ ( ๐ โ ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) ) |
45 |
44
|
anbi1d |
โข ( ๐ = ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ ( ( ๐ โง ๐ ) โ ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โง ๐ ) ) ) |
46 |
45
|
anbi1d |
โข ( ๐ = ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ ( ( ( ๐ โง ๐ ) โง ๐ ) โ ( ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โง ๐ ) โง ๐ ) ) ) |
47 |
|
ovex |
โข ( ๐ โf + ๐ ) โ V |
48 |
47 11
|
elab |
โข ( ( ๐ โf + ๐ ) โ { ๐ฅ โฃ ๐ } โ ๐ ) |
49 |
|
oveq1 |
โข ( ๐ = ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ ( ๐ โf + ๐ ) = ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โf + ๐ ) ) |
50 |
49
|
eleq1d |
โข ( ๐ = ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ ( ( ๐ โf + ๐ ) โ { ๐ฅ โฃ ๐ } โ ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โf + ๐ ) โ { ๐ฅ โฃ ๐ } ) ) |
51 |
48 50
|
bitr3id |
โข ( ๐ = ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ ( ๐ โ ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โf + ๐ ) โ { ๐ฅ โฃ ๐ } ) ) |
52 |
46 51
|
imbi12d |
โข ( ๐ = ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ ( ( ( ( ๐ โง ๐ ) โง ๐ ) โ ๐ ) โ ( ( ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โง ๐ ) โง ๐ ) โ ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โf + ๐ ) โ { ๐ฅ โฃ ๐ } ) ) ) |
53 |
|
vex |
โข ๐ โ V |
54 |
53 10
|
elab |
โข ( ๐ โ { ๐ฅ โฃ ๐ } โ ๐ ) |
55 |
|
eleq1 |
โข ( ๐ = ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ ( ๐ โ { ๐ฅ โฃ ๐ } โ ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) ) |
56 |
54 55
|
bitr3id |
โข ( ๐ = ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ ( ๐ โ ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) ) |
57 |
56
|
anbi2d |
โข ( ๐ = ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ ( ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โง ๐ ) โ ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โง ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) ) ) |
58 |
57
|
anbi1d |
โข ( ๐ = ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ ( ( ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โง ๐ ) โง ๐ ) โ ( ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โง ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) โง ๐ ) ) ) |
59 |
|
oveq2 |
โข ( ๐ = ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โf + ๐ ) = ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โf + ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) ) ) |
60 |
59
|
eleq1d |
โข ( ๐ = ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ ( ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โf + ๐ ) โ { ๐ฅ โฃ ๐ } โ ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โf + ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) ) โ { ๐ฅ โฃ ๐ } ) ) |
61 |
58 60
|
imbi12d |
โข ( ๐ = ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ ( ( ( ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โง ๐ ) โง ๐ ) โ ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โf + ๐ ) โ { ๐ฅ โฃ ๐ } ) โ ( ( ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โง ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) โง ๐ ) โ ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โf + ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) ) โ { ๐ฅ โฃ ๐ } ) ) ) |
62 |
5
|
expcom |
โข ( ( ( ๐ โ ๐ โง ๐ ) โง ( ๐ โ ๐ โง ๐ ) ) โ ( ๐ โ ๐ ) ) |
63 |
62
|
an4s |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐ โง ๐ ) ) โ ( ๐ โ ๐ ) ) |
64 |
63
|
expimpd |
โข ( ( ๐ โ ๐ โง ๐ โ ๐ ) โ ( ( ( ๐ โง ๐ ) โง ๐ ) โ ๐ ) ) |
65 |
52 61 64
|
vtocl2ga |
โข ( ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ ๐ โง ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ ๐ ) โ ( ( ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โง ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) โง ๐ ) โ ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โf + ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) ) โ { ๐ฅ โฃ ๐ } ) ) |
66 |
39 40 65
|
syl2an |
โข ( ( ๐ โ ran ( 1o eval ๐
) โง ๐ โ ran ( 1o eval ๐
) ) โ ( ( ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โง ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) โง ๐ ) โ ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โf + ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) ) โ { ๐ฅ โฃ ๐ } ) ) |
67 |
66
|
expcomd |
โข ( ( ๐ โ ran ( 1o eval ๐
) โง ๐ โ ran ( 1o eval ๐
) ) โ ( ๐ โ ( ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โง ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) โ ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โf + ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) ) โ { ๐ฅ โฃ ๐ } ) ) ) |
68 |
67
|
impcom |
โข ( ( ๐ โง ( ๐ โ ran ( 1o eval ๐
) โง ๐ โ ran ( 1o eval ๐
) ) ) โ ( ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โง ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) โ ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โf + ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) ) โ { ๐ฅ โฃ ๐ } ) ) |
69 |
36 1
|
mpff |
โข ( ๐ โ ran ( 1o eval ๐
) โ ๐ : ( ๐ต โm 1o ) โถ ๐ต ) |
70 |
69
|
ad2antrl |
โข ( ( ๐ โง ( ๐ โ ran ( 1o eval ๐
) โง ๐ โ ran ( 1o eval ๐
) ) ) โ ๐ : ( ๐ต โm 1o ) โถ ๐ต ) |
71 |
70
|
ffnd |
โข ( ( ๐ โง ( ๐ โ ran ( 1o eval ๐
) โง ๐ โ ran ( 1o eval ๐
) ) ) โ ๐ Fn ( ๐ต โm 1o ) ) |
72 |
36 1
|
mpff |
โข ( ๐ โ ran ( 1o eval ๐
) โ ๐ : ( ๐ต โm 1o ) โถ ๐ต ) |
73 |
72
|
ad2antll |
โข ( ( ๐ โง ( ๐ โ ran ( 1o eval ๐
) โง ๐ โ ran ( 1o eval ๐
) ) ) โ ๐ : ( ๐ต โm 1o ) โถ ๐ต ) |
74 |
73
|
ffnd |
โข ( ( ๐ โง ( ๐ โ ran ( 1o eval ๐
) โง ๐ โ ran ( 1o eval ๐
) ) ) โ ๐ Fn ( ๐ต โm 1o ) ) |
75 |
|
eqid |
โข ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) = ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) |
76 |
18 19 20 75
|
mapsnf1o3 |
โข ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) : ๐ต โ1-1-ontoโ ( ๐ต โm 1o ) |
77 |
|
f1of |
โข ( ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) : ๐ต โ1-1-ontoโ ( ๐ต โm 1o ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) : ๐ต โถ ( ๐ต โm 1o ) ) |
78 |
76 77
|
mp1i |
โข ( ( ๐ โง ( ๐ โ ran ( 1o eval ๐
) โง ๐ โ ran ( 1o eval ๐
) ) ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) : ๐ต โถ ( ๐ต โm 1o ) ) |
79 |
|
ovexd |
โข ( ( ๐ โง ( ๐ โ ran ( 1o eval ๐
) โง ๐ โ ran ( 1o eval ๐
) ) ) โ ( ๐ต โm 1o ) โ V ) |
80 |
19
|
a1i |
โข ( ( ๐ โง ( ๐ โ ran ( 1o eval ๐
) โง ๐ โ ran ( 1o eval ๐
) ) ) โ ๐ต โ V ) |
81 |
|
inidm |
โข ( ( ๐ต โm 1o ) โฉ ( ๐ต โm 1o ) ) = ( ๐ต โm 1o ) |
82 |
71 74 78 79 79 80 81
|
ofco |
โข ( ( ๐ โง ( ๐ โ ran ( 1o eval ๐
) โง ๐ โ ran ( 1o eval ๐
) ) ) โ ( ( ๐ โf + ๐ ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) = ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โf + ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) ) ) |
83 |
82
|
eleq1d |
โข ( ( ๐ โง ( ๐ โ ran ( 1o eval ๐
) โง ๐ โ ran ( 1o eval ๐
) ) ) โ ( ( ( ๐ โf + ๐ ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โ ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โf + ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) ) โ { ๐ฅ โฃ ๐ } ) ) |
84 |
68 83
|
sylibrd |
โข ( ( ๐ โง ( ๐ โ ran ( 1o eval ๐
) โง ๐ โ ran ( 1o eval ๐
) ) ) โ ( ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โง ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) โ ( ( ๐ โf + ๐ ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) ) |
85 |
84
|
expimpd |
โข ( ๐ โ ( ( ( ๐ โ ran ( 1o eval ๐
) โง ๐ โ ran ( 1o eval ๐
) ) โง ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โง ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) ) โ ( ( ๐ โf + ๐ ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) ) |
86 |
37 85
|
biimtrid |
โข ( ๐ โ ( ( ( ๐ โ ran ( 1o eval ๐
) โง ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) โง ( ๐ โ ran ( 1o eval ๐
) โง ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) ) โ ( ( ๐ โf + ๐ ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) ) |
87 |
86
|
imp |
โข ( ( ๐ โง ( ( ๐ โ ran ( 1o eval ๐
) โง ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) โง ( ๐ โ ran ( 1o eval ๐
) โง ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) ) ) โ ( ( ๐ โf + ๐ ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) |
88 |
|
ovex |
โข ( ๐ โf ยท ๐ ) โ V |
89 |
88 12
|
elab |
โข ( ( ๐ โf ยท ๐ ) โ { ๐ฅ โฃ ๐ } โ ๐ ) |
90 |
|
oveq1 |
โข ( ๐ = ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ ( ๐ โf ยท ๐ ) = ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โf ยท ๐ ) ) |
91 |
90
|
eleq1d |
โข ( ๐ = ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ ( ( ๐ โf ยท ๐ ) โ { ๐ฅ โฃ ๐ } โ ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โf ยท ๐ ) โ { ๐ฅ โฃ ๐ } ) ) |
92 |
89 91
|
bitr3id |
โข ( ๐ = ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ ( ๐ โ ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โf ยท ๐ ) โ { ๐ฅ โฃ ๐ } ) ) |
93 |
46 92
|
imbi12d |
โข ( ๐ = ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ ( ( ( ( ๐ โง ๐ ) โง ๐ ) โ ๐ ) โ ( ( ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โง ๐ ) โง ๐ ) โ ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โf ยท ๐ ) โ { ๐ฅ โฃ ๐ } ) ) ) |
94 |
|
oveq2 |
โข ( ๐ = ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โf ยท ๐ ) = ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โf ยท ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) ) ) |
95 |
94
|
eleq1d |
โข ( ๐ = ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ ( ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โf ยท ๐ ) โ { ๐ฅ โฃ ๐ } โ ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โf ยท ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) ) โ { ๐ฅ โฃ ๐ } ) ) |
96 |
58 95
|
imbi12d |
โข ( ๐ = ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ ( ( ( ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โง ๐ ) โง ๐ ) โ ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โf ยท ๐ ) โ { ๐ฅ โฃ ๐ } ) โ ( ( ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โง ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) โง ๐ ) โ ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โf ยท ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) ) โ { ๐ฅ โฃ ๐ } ) ) ) |
97 |
6
|
expcom |
โข ( ( ( ๐ โ ๐ โง ๐ ) โง ( ๐ โ ๐ โง ๐ ) ) โ ( ๐ โ ๐ ) ) |
98 |
97
|
an4s |
โข ( ( ( ๐ โ ๐ โง ๐ โ ๐ ) โง ( ๐ โง ๐ ) ) โ ( ๐ โ ๐ ) ) |
99 |
98
|
expimpd |
โข ( ( ๐ โ ๐ โง ๐ โ ๐ ) โ ( ( ( ๐ โง ๐ ) โง ๐ ) โ ๐ ) ) |
100 |
93 96 99
|
vtocl2ga |
โข ( ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ ๐ โง ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ ๐ ) โ ( ( ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โง ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) โง ๐ ) โ ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โf ยท ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) ) โ { ๐ฅ โฃ ๐ } ) ) |
101 |
39 40 100
|
syl2an |
โข ( ( ๐ โ ran ( 1o eval ๐
) โง ๐ โ ran ( 1o eval ๐
) ) โ ( ( ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โง ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) โง ๐ ) โ ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โf ยท ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) ) โ { ๐ฅ โฃ ๐ } ) ) |
102 |
101
|
expcomd |
โข ( ( ๐ โ ran ( 1o eval ๐
) โง ๐ โ ran ( 1o eval ๐
) ) โ ( ๐ โ ( ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โง ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) โ ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โf ยท ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) ) โ { ๐ฅ โฃ ๐ } ) ) ) |
103 |
102
|
impcom |
โข ( ( ๐ โง ( ๐ โ ran ( 1o eval ๐
) โง ๐ โ ran ( 1o eval ๐
) ) ) โ ( ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โง ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) โ ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โf ยท ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) ) โ { ๐ฅ โฃ ๐ } ) ) |
104 |
71 74 78 79 79 80 81
|
ofco |
โข ( ( ๐ โง ( ๐ โ ran ( 1o eval ๐
) โง ๐ โ ran ( 1o eval ๐
) ) ) โ ( ( ๐ โf ยท ๐ ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) = ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โf ยท ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) ) ) |
105 |
104
|
eleq1d |
โข ( ( ๐ โง ( ๐ โ ran ( 1o eval ๐
) โง ๐ โ ran ( 1o eval ๐
) ) ) โ ( ( ( ๐ โf ยท ๐ ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โ ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โf ยท ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) ) โ { ๐ฅ โฃ ๐ } ) ) |
106 |
103 105
|
sylibrd |
โข ( ( ๐ โง ( ๐ โ ran ( 1o eval ๐
) โง ๐ โ ran ( 1o eval ๐
) ) ) โ ( ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โง ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) โ ( ( ๐ โf ยท ๐ ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) ) |
107 |
106
|
expimpd |
โข ( ๐ โ ( ( ( ๐ โ ran ( 1o eval ๐
) โง ๐ โ ran ( 1o eval ๐
) ) โง ( ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โง ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) ) โ ( ( ๐ โf ยท ๐ ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) ) |
108 |
37 107
|
biimtrid |
โข ( ๐ โ ( ( ( ๐ โ ran ( 1o eval ๐
) โง ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) โง ( ๐ โ ran ( 1o eval ๐
) โง ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) ) โ ( ( ๐ โf ยท ๐ ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) ) |
109 |
108
|
imp |
โข ( ( ๐ โง ( ( ๐ โ ran ( 1o eval ๐
) โง ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) โง ( ๐ โ ran ( 1o eval ๐
) โง ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) ) ) โ ( ( ๐ โf ยท ๐ ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) |
110 |
|
coeq1 |
โข ( ๐ฆ = ( ( ๐ต โm 1o ) ร { ๐ } ) โ ( ๐ฆ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) = ( ( ( ๐ต โm 1o ) ร { ๐ } ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) ) |
111 |
110
|
eleq1d |
โข ( ๐ฆ = ( ( ๐ต โm 1o ) ร { ๐ } ) โ ( ( ๐ฆ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โ ( ( ( ๐ต โm 1o ) ร { ๐ } ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) ) |
112 |
|
coeq1 |
โข ( ๐ฆ = ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ ๐ ) ) โ ( ๐ฆ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) = ( ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ ๐ ) ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) ) |
113 |
112
|
eleq1d |
โข ( ๐ฆ = ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ ๐ ) ) โ ( ( ๐ฆ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โ ( ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ ๐ ) ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) ) |
114 |
|
coeq1 |
โข ( ๐ฆ = ๐ โ ( ๐ฆ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) = ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) ) |
115 |
114
|
eleq1d |
โข ( ๐ฆ = ๐ โ ( ( ๐ฆ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โ ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) ) |
116 |
|
coeq1 |
โข ( ๐ฆ = ๐ โ ( ๐ฆ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) = ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) ) |
117 |
116
|
eleq1d |
โข ( ๐ฆ = ๐ โ ( ( ๐ฆ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โ ( ๐ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) ) |
118 |
|
coeq1 |
โข ( ๐ฆ = ( ๐ โf + ๐ ) โ ( ๐ฆ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) = ( ( ๐ โf + ๐ ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) ) |
119 |
118
|
eleq1d |
โข ( ๐ฆ = ( ๐ โf + ๐ ) โ ( ( ๐ฆ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โ ( ( ๐ โf + ๐ ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) ) |
120 |
|
coeq1 |
โข ( ๐ฆ = ( ๐ โf ยท ๐ ) โ ( ๐ฆ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) = ( ( ๐ โf ยท ๐ ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) ) |
121 |
120
|
eleq1d |
โข ( ๐ฆ = ( ๐ โf ยท ๐ ) โ ( ( ๐ฆ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โ ( ( ๐ โf ยท ๐ ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) ) |
122 |
|
coeq1 |
โข ( ๐ฆ = ( ๐ด โ ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ โ
) ) ) โ ( ๐ฆ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) = ( ( ๐ด โ ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ โ
) ) ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) ) |
123 |
122
|
eleq1d |
โข ( ๐ฆ = ( ๐ด โ ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ โ
) ) ) โ ( ( ๐ฆ โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โ ( ( ๐ด โ ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ โ
) ) ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) ) |
124 |
4
|
pf1rcl |
โข ( ๐ด โ ๐ โ ๐
โ CRing ) |
125 |
16 124
|
syl |
โข ( ๐ โ ๐
โ CRing ) |
126 |
125
|
adantr |
โข ( ( ๐ โง ๐ โ ๐ต ) โ ๐
โ CRing ) |
127 |
|
1on |
โข 1o โ On |
128 |
|
eqid |
โข ( 1o mPoly ๐
) = ( 1o mPoly ๐
) |
129 |
128
|
mplassa |
โข ( ( 1o โ On โง ๐
โ CRing ) โ ( 1o mPoly ๐
) โ AssAlg ) |
130 |
127 125 129
|
sylancr |
โข ( ๐ โ ( 1o mPoly ๐
) โ AssAlg ) |
131 |
|
eqid |
โข ( Poly1 โ ๐
) = ( Poly1 โ ๐
) |
132 |
|
eqid |
โข ( algSc โ ( Poly1 โ ๐
) ) = ( algSc โ ( Poly1 โ ๐
) ) |
133 |
131 132
|
ply1ascl |
โข ( algSc โ ( Poly1 โ ๐
) ) = ( algSc โ ( 1o mPoly ๐
) ) |
134 |
|
eqid |
โข ( Scalar โ ( 1o mPoly ๐
) ) = ( Scalar โ ( 1o mPoly ๐
) ) |
135 |
133 134
|
asclrhm |
โข ( ( 1o mPoly ๐
) โ AssAlg โ ( algSc โ ( Poly1 โ ๐
) ) โ ( ( Scalar โ ( 1o mPoly ๐
) ) RingHom ( 1o mPoly ๐
) ) ) |
136 |
130 135
|
syl |
โข ( ๐ โ ( algSc โ ( Poly1 โ ๐
) ) โ ( ( Scalar โ ( 1o mPoly ๐
) ) RingHom ( 1o mPoly ๐
) ) ) |
137 |
127
|
a1i |
โข ( ๐ โ 1o โ On ) |
138 |
128 137 125
|
mplsca |
โข ( ๐ โ ๐
= ( Scalar โ ( 1o mPoly ๐
) ) ) |
139 |
138
|
oveq1d |
โข ( ๐ โ ( ๐
RingHom ( 1o mPoly ๐
) ) = ( ( Scalar โ ( 1o mPoly ๐
) ) RingHom ( 1o mPoly ๐
) ) ) |
140 |
136 139
|
eleqtrrd |
โข ( ๐ โ ( algSc โ ( Poly1 โ ๐
) ) โ ( ๐
RingHom ( 1o mPoly ๐
) ) ) |
141 |
|
eqid |
โข ( Base โ ( 1o mPoly ๐
) ) = ( Base โ ( 1o mPoly ๐
) ) |
142 |
1 141
|
rhmf |
โข ( ( algSc โ ( Poly1 โ ๐
) ) โ ( ๐
RingHom ( 1o mPoly ๐
) ) โ ( algSc โ ( Poly1 โ ๐
) ) : ๐ต โถ ( Base โ ( 1o mPoly ๐
) ) ) |
143 |
140 142
|
syl |
โข ( ๐ โ ( algSc โ ( Poly1 โ ๐
) ) : ๐ต โถ ( Base โ ( 1o mPoly ๐
) ) ) |
144 |
143
|
ffvelcdmda |
โข ( ( ๐ โง ๐ โ ๐ต ) โ ( ( algSc โ ( Poly1 โ ๐
) ) โ ๐ ) โ ( Base โ ( 1o mPoly ๐
) ) ) |
145 |
|
eqid |
โข ( eval1 โ ๐
) = ( eval1 โ ๐
) |
146 |
145 34 1 128 141
|
evl1val |
โข ( ( ๐
โ CRing โง ( ( algSc โ ( Poly1 โ ๐
) ) โ ๐ ) โ ( Base โ ( 1o mPoly ๐
) ) ) โ ( ( eval1 โ ๐
) โ ( ( algSc โ ( Poly1 โ ๐
) ) โ ๐ ) ) = ( ( ( 1o eval ๐
) โ ( ( algSc โ ( Poly1 โ ๐
) ) โ ๐ ) ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) ) |
147 |
126 144 146
|
syl2anc |
โข ( ( ๐ โง ๐ โ ๐ต ) โ ( ( eval1 โ ๐
) โ ( ( algSc โ ( Poly1 โ ๐
) ) โ ๐ ) ) = ( ( ( 1o eval ๐
) โ ( ( algSc โ ( Poly1 โ ๐
) ) โ ๐ ) ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) ) |
148 |
145 131 1 132
|
evl1sca |
โข ( ( ๐
โ CRing โง ๐ โ ๐ต ) โ ( ( eval1 โ ๐
) โ ( ( algSc โ ( Poly1 โ ๐
) ) โ ๐ ) ) = ( ๐ต ร { ๐ } ) ) |
149 |
125 148
|
sylan |
โข ( ( ๐ โง ๐ โ ๐ต ) โ ( ( eval1 โ ๐
) โ ( ( algSc โ ( Poly1 โ ๐
) ) โ ๐ ) ) = ( ๐ต ร { ๐ } ) ) |
150 |
1
|
ressid |
โข ( ๐
โ CRing โ ( ๐
โพs ๐ต ) = ๐
) |
151 |
126 150
|
syl |
โข ( ( ๐ โง ๐ โ ๐ต ) โ ( ๐
โพs ๐ต ) = ๐
) |
152 |
151
|
oveq2d |
โข ( ( ๐ โง ๐ โ ๐ต ) โ ( 1o mPoly ( ๐
โพs ๐ต ) ) = ( 1o mPoly ๐
) ) |
153 |
152
|
fveq2d |
โข ( ( ๐ โง ๐ โ ๐ต ) โ ( algSc โ ( 1o mPoly ( ๐
โพs ๐ต ) ) ) = ( algSc โ ( 1o mPoly ๐
) ) ) |
154 |
153 133
|
eqtr4di |
โข ( ( ๐ โง ๐ โ ๐ต ) โ ( algSc โ ( 1o mPoly ( ๐
โพs ๐ต ) ) ) = ( algSc โ ( Poly1 โ ๐
) ) ) |
155 |
154
|
fveq1d |
โข ( ( ๐ โง ๐ โ ๐ต ) โ ( ( algSc โ ( 1o mPoly ( ๐
โพs ๐ต ) ) ) โ ๐ ) = ( ( algSc โ ( Poly1 โ ๐
) ) โ ๐ ) ) |
156 |
155
|
fveq2d |
โข ( ( ๐ โง ๐ โ ๐ต ) โ ( ( 1o eval ๐
) โ ( ( algSc โ ( 1o mPoly ( ๐
โพs ๐ต ) ) ) โ ๐ ) ) = ( ( 1o eval ๐
) โ ( ( algSc โ ( Poly1 โ ๐
) ) โ ๐ ) ) ) |
157 |
|
eqid |
โข ( 1o mPoly ( ๐
โพs ๐ต ) ) = ( 1o mPoly ( ๐
โพs ๐ต ) ) |
158 |
|
eqid |
โข ( ๐
โพs ๐ต ) = ( ๐
โพs ๐ต ) |
159 |
|
eqid |
โข ( algSc โ ( 1o mPoly ( ๐
โพs ๐ต ) ) ) = ( algSc โ ( 1o mPoly ( ๐
โพs ๐ต ) ) ) |
160 |
127
|
a1i |
โข ( ( ๐ โง ๐ โ ๐ต ) โ 1o โ On ) |
161 |
|
crngring |
โข ( ๐
โ CRing โ ๐
โ Ring ) |
162 |
1
|
subrgid |
โข ( ๐
โ Ring โ ๐ต โ ( SubRing โ ๐
) ) |
163 |
125 161 162
|
3syl |
โข ( ๐ โ ๐ต โ ( SubRing โ ๐
) ) |
164 |
163
|
adantr |
โข ( ( ๐ โง ๐ โ ๐ต ) โ ๐ต โ ( SubRing โ ๐
) ) |
165 |
|
simpr |
โข ( ( ๐ โง ๐ โ ๐ต ) โ ๐ โ ๐ต ) |
166 |
35 157 158 1 159 160 126 164 165
|
evlssca |
โข ( ( ๐ โง ๐ โ ๐ต ) โ ( ( 1o eval ๐
) โ ( ( algSc โ ( 1o mPoly ( ๐
โพs ๐ต ) ) ) โ ๐ ) ) = ( ( ๐ต โm 1o ) ร { ๐ } ) ) |
167 |
156 166
|
eqtr3d |
โข ( ( ๐ โง ๐ โ ๐ต ) โ ( ( 1o eval ๐
) โ ( ( algSc โ ( Poly1 โ ๐
) ) โ ๐ ) ) = ( ( ๐ต โm 1o ) ร { ๐ } ) ) |
168 |
167
|
coeq1d |
โข ( ( ๐ โง ๐ โ ๐ต ) โ ( ( ( 1o eval ๐
) โ ( ( algSc โ ( Poly1 โ ๐
) ) โ ๐ ) ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) = ( ( ( ๐ต โm 1o ) ร { ๐ } ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) ) |
169 |
147 149 168
|
3eqtr3d |
โข ( ( ๐ โง ๐ โ ๐ต ) โ ( ๐ต ร { ๐ } ) = ( ( ( ๐ต โm 1o ) ร { ๐ } ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) ) |
170 |
|
vsnex |
โข { ๐ } โ V |
171 |
19 170
|
xpex |
โข ( ๐ต ร { ๐ } ) โ V |
172 |
171 7
|
elab |
โข ( ( ๐ต ร { ๐ } ) โ { ๐ฅ โฃ ๐ } โ ๐ ) |
173 |
14 172
|
sylibr |
โข ( ( ๐ โง ๐ โ ๐ต ) โ ( ๐ต ร { ๐ } ) โ { ๐ฅ โฃ ๐ } ) |
174 |
173
|
ralrimiva |
โข ( ๐ โ โ ๐ โ ๐ต ( ๐ต ร { ๐ } ) โ { ๐ฅ โฃ ๐ } ) |
175 |
|
sneq |
โข ( ๐ = ๐ โ { ๐ } = { ๐ } ) |
176 |
175
|
xpeq2d |
โข ( ๐ = ๐ โ ( ๐ต ร { ๐ } ) = ( ๐ต ร { ๐ } ) ) |
177 |
176
|
eleq1d |
โข ( ๐ = ๐ โ ( ( ๐ต ร { ๐ } ) โ { ๐ฅ โฃ ๐ } โ ( ๐ต ร { ๐ } ) โ { ๐ฅ โฃ ๐ } ) ) |
178 |
177
|
rspccva |
โข ( ( โ ๐ โ ๐ต ( ๐ต ร { ๐ } ) โ { ๐ฅ โฃ ๐ } โง ๐ โ ๐ต ) โ ( ๐ต ร { ๐ } ) โ { ๐ฅ โฃ ๐ } ) |
179 |
174 178
|
sylan |
โข ( ( ๐ โง ๐ โ ๐ต ) โ ( ๐ต ร { ๐ } ) โ { ๐ฅ โฃ ๐ } ) |
180 |
169 179
|
eqeltrrd |
โข ( ( ๐ โง ๐ โ ๐ต ) โ ( ( ( ๐ต โm 1o ) ร { ๐ } ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) |
181 |
|
resiexg |
โข ( ๐ต โ V โ ( I โพ ๐ต ) โ V ) |
182 |
19 181
|
ax-mp |
โข ( I โพ ๐ต ) โ V |
183 |
182 8
|
elab |
โข ( ( I โพ ๐ต ) โ { ๐ฅ โฃ ๐ } โ ๐ ) |
184 |
15 183
|
sylibr |
โข ( ๐ โ ( I โพ ๐ต ) โ { ๐ฅ โฃ ๐ } ) |
185 |
27 184
|
eqeltrd |
โข ( ๐ โ ( ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ โ
) ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) |
186 |
|
el1o |
โข ( ๐ โ 1o โ ๐ = โ
) |
187 |
|
fveq2 |
โข ( ๐ = โ
โ ( ๐ โ ๐ ) = ( ๐ โ โ
) ) |
188 |
186 187
|
sylbi |
โข ( ๐ โ 1o โ ( ๐ โ ๐ ) = ( ๐ โ โ
) ) |
189 |
188
|
mpteq2dv |
โข ( ๐ โ 1o โ ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ ๐ ) ) = ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ โ
) ) ) |
190 |
189
|
coeq1d |
โข ( ๐ โ 1o โ ( ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ ๐ ) ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) = ( ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ โ
) ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) ) |
191 |
190
|
eleq1d |
โข ( ๐ โ 1o โ ( ( ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ ๐ ) ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } โ ( ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ โ
) ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) ) |
192 |
185 191
|
syl5ibrcom |
โข ( ๐ โ ( ๐ โ 1o โ ( ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ ๐ ) ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) ) |
193 |
192
|
imp |
โข ( ( ๐ โง ๐ โ 1o ) โ ( ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ ๐ ) ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) |
194 |
4 1 38
|
pf1mpf |
โข ( ๐ด โ ๐ โ ( ๐ด โ ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ โ
) ) ) โ ran ( 1o eval ๐
) ) |
195 |
16 194
|
syl |
โข ( ๐ โ ( ๐ด โ ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ โ
) ) ) โ ran ( 1o eval ๐
) ) |
196 |
1 2 3 36 87 109 111 113 115 117 119 121 123 180 193 195
|
mpfind |
โข ( ๐ โ ( ( ๐ด โ ( ๐ โ ( ๐ต โm 1o ) โฆ ( ๐ โ โ
) ) ) โ ( ๐ค โ ๐ต โฆ ( 1o ร { ๐ค } ) ) ) โ { ๐ฅ โฃ ๐ } ) |
197 |
33 196
|
eqeltrrd |
โข ( ๐ โ ๐ด โ { ๐ฅ โฃ ๐ } ) |
198 |
13
|
elabg |
โข ( ๐ด โ ๐ โ ( ๐ด โ { ๐ฅ โฃ ๐ } โ ๐ ) ) |
199 |
16 198
|
syl |
โข ( ๐ โ ( ๐ด โ { ๐ฅ โฃ ๐ } โ ๐ ) ) |
200 |
197 199
|
mpbid |
โข ( ๐ โ ๐ ) |