Metamath Proof Explorer


Theorem pf1ind

Description: Prove a property of polynomials by "structural" induction, under a simplified model of structure which loses the sum of products structure. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses pf1ind.cb โŠข ๐ต = ( Base โ€˜ ๐‘… )
pf1ind.cp โŠข + = ( +g โ€˜ ๐‘… )
pf1ind.ct โŠข ยท = ( .r โ€˜ ๐‘… )
pf1ind.cq โŠข ๐‘„ = ran ( eval1 โ€˜ ๐‘… )
pf1ind.ad โŠข ( ( ๐œ‘ โˆง ( ( ๐‘“ โˆˆ ๐‘„ โˆง ๐œ ) โˆง ( ๐‘” โˆˆ ๐‘„ โˆง ๐œ‚ ) ) ) โ†’ ๐œ )
pf1ind.mu โŠข ( ( ๐œ‘ โˆง ( ( ๐‘“ โˆˆ ๐‘„ โˆง ๐œ ) โˆง ( ๐‘” โˆˆ ๐‘„ โˆง ๐œ‚ ) ) ) โ†’ ๐œŽ )
pf1ind.wa โŠข ( ๐‘ฅ = ( ๐ต ร— { ๐‘“ } ) โ†’ ( ๐œ“ โ†” ๐œ’ ) )
pf1ind.wb โŠข ( ๐‘ฅ = ( I โ†พ ๐ต ) โ†’ ( ๐œ“ โ†” ๐œƒ ) )
pf1ind.wc โŠข ( ๐‘ฅ = ๐‘“ โ†’ ( ๐œ“ โ†” ๐œ ) )
pf1ind.wd โŠข ( ๐‘ฅ = ๐‘” โ†’ ( ๐œ“ โ†” ๐œ‚ ) )
pf1ind.we โŠข ( ๐‘ฅ = ( ๐‘“ โˆ˜f + ๐‘” ) โ†’ ( ๐œ“ โ†” ๐œ ) )
pf1ind.wf โŠข ( ๐‘ฅ = ( ๐‘“ โˆ˜f ยท ๐‘” ) โ†’ ( ๐œ“ โ†” ๐œŽ ) )
pf1ind.wg โŠข ( ๐‘ฅ = ๐ด โ†’ ( ๐œ“ โ†” ๐œŒ ) )
pf1ind.co โŠข ( ( ๐œ‘ โˆง ๐‘“ โˆˆ ๐ต ) โ†’ ๐œ’ )
pf1ind.pr โŠข ( ๐œ‘ โ†’ ๐œƒ )
pf1ind.a โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ ๐‘„ )
Assertion pf1ind ( ๐œ‘ โ†’ ๐œŒ )

Proof

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 โŠข ( ๐œ‘ โ†’ ๐œŒ )