MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pf1ind Structured version   Visualization version   GIF version

Theorem pf1ind 20983
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.)
Hypotheses
Ref Expression
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
Ref Expression
pf1ind (𝜑𝜌)
Distinct variable groups:   𝑓,𝑔,𝑥, +   𝐵,𝑓,𝑔,𝑥   𝜂,𝑓,𝑥   𝜑,𝑓,𝑔   𝑥,𝐴   𝜒,𝑥   𝜓,𝑓,𝑔   𝑄,𝑓,𝑔   𝜌,𝑥   𝜎,𝑥   𝜏,𝑥   𝜃,𝑥   · ,𝑓,𝑔,𝑥   𝜁,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)   𝜒(𝑓,𝑔)   𝜃(𝑓,𝑔)   𝜏(𝑓,𝑔)   𝜂(𝑔)   𝜁(𝑓,𝑔)   𝜎(𝑓,𝑔)   𝜌(𝑓,𝑔)   𝐴(𝑓,𝑔)   𝑄(𝑥)   𝑅(𝑥,𝑓,𝑔)

Proof of Theorem pf1ind
Dummy variables 𝑎 𝑏 𝑦 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 coass 6089 . . . . 5 ((𝐴 ∘ (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅))) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) = (𝐴 ∘ ((𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅)) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))))
2 df1o2 8103 . . . . . . . . 9 1o = {∅}
3 pf1ind.cb . . . . . . . . . 10 𝐵 = (Base‘𝑅)
43fvexi 6663 . . . . . . . . 9 𝐵 ∈ V
5 0ex 5178 . . . . . . . . 9 ∅ ∈ V
6 eqid 2801 . . . . . . . . 9 (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅)) = (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅))
72, 4, 5, 6mapsncnv 8444 . . . . . . . 8 (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅)) = (𝑤𝐵 ↦ (1o × {𝑤}))
87coeq2i 5699 . . . . . . 7 ((𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅)) ∘ (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅))) = ((𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅)) ∘ (𝑤𝐵 ↦ (1o × {𝑤})))
92, 4, 5, 6mapsnf1o2 8445 . . . . . . . 8 (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅)):(𝐵m 1o)–1-1-onto𝐵
10 f1ococnv2 6620 . . . . . . . 8 ((𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅)):(𝐵m 1o)–1-1-onto𝐵 → ((𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅)) ∘ (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅))) = ( I ↾ 𝐵))
119, 10mp1i 13 . . . . . . 7 (𝜑 → ((𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅)) ∘ (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅))) = ( I ↾ 𝐵))
128, 11syl5eqr 2850 . . . . . 6 (𝜑 → ((𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅)) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) = ( I ↾ 𝐵))
1312coeq2d 5701 . . . . 5 (𝜑 → (𝐴 ∘ ((𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅)) ∘ (𝑤𝐵 ↦ (1o × {𝑤})))) = (𝐴 ∘ ( I ↾ 𝐵)))
141, 13syl5eq 2848 . . . 4 (𝜑 → ((𝐴 ∘ (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅))) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) = (𝐴 ∘ ( I ↾ 𝐵)))
15 pf1ind.a . . . . 5 (𝜑𝐴𝑄)
16 pf1ind.cq . . . . . 6 𝑄 = ran (eval1𝑅)
1716, 3pf1f 20978 . . . . 5 (𝐴𝑄𝐴:𝐵𝐵)
18 fcoi1 6530 . . . . 5 (𝐴:𝐵𝐵 → (𝐴 ∘ ( I ↾ 𝐵)) = 𝐴)
1915, 17, 183syl 18 . . . 4 (𝜑 → (𝐴 ∘ ( I ↾ 𝐵)) = 𝐴)
2014, 19eqtrd 2836 . . 3 (𝜑 → ((𝐴 ∘ (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅))) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) = 𝐴)
21 pf1ind.cp . . . 4 + = (+g𝑅)
22 pf1ind.ct . . . 4 · = (.r𝑅)
23 eqid 2801 . . . . . 6 (1o eval 𝑅) = (1o eval 𝑅)
2423, 3evlval 20771 . . . . 5 (1o eval 𝑅) = ((1o evalSub 𝑅)‘𝐵)
2524rneqi 5775 . . . 4 ran (1o eval 𝑅) = ran ((1o evalSub 𝑅)‘𝐵)
26 an4 655 . . . . . 6 (((𝑎 ∈ ran (1o eval 𝑅) ∧ (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) ∧ (𝑏 ∈ ran (1o eval 𝑅) ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓})) ↔ ((𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅)) ∧ ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓})))
27 eqid 2801 . . . . . . . . . . . 12 ran (1o eval 𝑅) = ran (1o eval 𝑅)
2816, 3, 27mpfpf1 20979 . . . . . . . . . . 11 (𝑎 ∈ ran (1o eval 𝑅) → (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ 𝑄)
2916, 3, 27mpfpf1 20979 . . . . . . . . . . 11 (𝑏 ∈ ran (1o eval 𝑅) → (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ 𝑄)
30 vex 3447 . . . . . . . . . . . . . . . . 17 𝑓 ∈ V
31 pf1ind.wc . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑓 → (𝜓𝜏))
3230, 31elab 3618 . . . . . . . . . . . . . . . 16 (𝑓 ∈ {𝑥𝜓} ↔ 𝜏)
33 eleq1 2880 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → (𝑓 ∈ {𝑥𝜓} ↔ (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
3432, 33bitr3id 288 . . . . . . . . . . . . . . 15 (𝑓 = (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → (𝜏 ↔ (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
3534anbi1d 632 . . . . . . . . . . . . . 14 (𝑓 = (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → ((𝜏𝜂) ↔ ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ 𝜂)))
3635anbi1d 632 . . . . . . . . . . . . 13 (𝑓 = (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → (((𝜏𝜂) ∧ 𝜑) ↔ (((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ 𝜂) ∧ 𝜑)))
37 ovex 7172 . . . . . . . . . . . . . . 15 (𝑓f + 𝑔) ∈ V
38 pf1ind.we . . . . . . . . . . . . . . 15 (𝑥 = (𝑓f + 𝑔) → (𝜓𝜁))
3937, 38elab 3618 . . . . . . . . . . . . . 14 ((𝑓f + 𝑔) ∈ {𝑥𝜓} ↔ 𝜁)
40 oveq1 7146 . . . . . . . . . . . . . . 15 (𝑓 = (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → (𝑓f + 𝑔) = ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f + 𝑔))
4140eleq1d 2877 . . . . . . . . . . . . . 14 (𝑓 = (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → ((𝑓f + 𝑔) ∈ {𝑥𝜓} ↔ ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f + 𝑔) ∈ {𝑥𝜓}))
4239, 41bitr3id 288 . . . . . . . . . . . . 13 (𝑓 = (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → (𝜁 ↔ ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f + 𝑔) ∈ {𝑥𝜓}))
4336, 42imbi12d 348 . . . . . . . . . . . 12 (𝑓 = (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → ((((𝜏𝜂) ∧ 𝜑) → 𝜁) ↔ ((((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ 𝜂) ∧ 𝜑) → ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f + 𝑔) ∈ {𝑥𝜓})))
44 vex 3447 . . . . . . . . . . . . . . . . 17 𝑔 ∈ V
45 pf1ind.wd . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑔 → (𝜓𝜂))
4644, 45elab 3618 . . . . . . . . . . . . . . . 16 (𝑔 ∈ {𝑥𝜓} ↔ 𝜂)
47 eleq1 2880 . . . . . . . . . . . . . . . 16 (𝑔 = (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → (𝑔 ∈ {𝑥𝜓} ↔ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
4846, 47bitr3id 288 . . . . . . . . . . . . . . 15 (𝑔 = (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → (𝜂 ↔ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
4948anbi2d 631 . . . . . . . . . . . . . 14 (𝑔 = (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → (((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ 𝜂) ↔ ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓})))
5049anbi1d 632 . . . . . . . . . . . . 13 (𝑔 = (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → ((((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ 𝜂) ∧ 𝜑) ↔ (((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) ∧ 𝜑)))
51 oveq2 7147 . . . . . . . . . . . . . 14 (𝑔 = (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f + 𝑔) = ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f + (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))))
5251eleq1d 2877 . . . . . . . . . . . . 13 (𝑔 = (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → (((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f + 𝑔) ∈ {𝑥𝜓} ↔ ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f + (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥𝜓}))
5350, 52imbi12d 348 . . . . . . . . . . . 12 (𝑔 = (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → (((((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ 𝜂) ∧ 𝜑) → ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f + 𝑔) ∈ {𝑥𝜓}) ↔ ((((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) ∧ 𝜑) → ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f + (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥𝜓})))
54 pf1ind.ad . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑓𝑄𝜏) ∧ (𝑔𝑄𝜂))) → 𝜁)
5554expcom 417 . . . . . . . . . . . . . 14 (((𝑓𝑄𝜏) ∧ (𝑔𝑄𝜂)) → (𝜑𝜁))
5655an4s 659 . . . . . . . . . . . . 13 (((𝑓𝑄𝑔𝑄) ∧ (𝜏𝜂)) → (𝜑𝜁))
5756expimpd 457 . . . . . . . . . . . 12 ((𝑓𝑄𝑔𝑄) → (((𝜏𝜂) ∧ 𝜑) → 𝜁))
5843, 53, 57vtocl2ga 3526 . . . . . . . . . . 11 (((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ 𝑄 ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ 𝑄) → ((((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) ∧ 𝜑) → ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f + (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥𝜓}))
5928, 29, 58syl2an 598 . . . . . . . . . 10 ((𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅)) → ((((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) ∧ 𝜑) → ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f + (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥𝜓}))
6059expcomd 420 . . . . . . . . 9 ((𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅)) → (𝜑 → (((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) → ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f + (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥𝜓})))
6160impcom 411 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → (((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) → ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f + (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥𝜓}))
6225, 3mpff 20780 . . . . . . . . . . . 12 (𝑎 ∈ ran (1o eval 𝑅) → 𝑎:(𝐵m 1o)⟶𝐵)
6362ad2antrl 727 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → 𝑎:(𝐵m 1o)⟶𝐵)
6463ffnd 6492 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → 𝑎 Fn (𝐵m 1o))
6525, 3mpff 20780 . . . . . . . . . . . 12 (𝑏 ∈ ran (1o eval 𝑅) → 𝑏:(𝐵m 1o)⟶𝐵)
6665ad2antll 728 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → 𝑏:(𝐵m 1o)⟶𝐵)
6766ffnd 6492 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → 𝑏 Fn (𝐵m 1o))
68 eqid 2801 . . . . . . . . . . . 12 (𝑤𝐵 ↦ (1o × {𝑤})) = (𝑤𝐵 ↦ (1o × {𝑤}))
692, 4, 5, 68mapsnf1o3 8446 . . . . . . . . . . 11 (𝑤𝐵 ↦ (1o × {𝑤})):𝐵1-1-onto→(𝐵m 1o)
70 f1of 6594 . . . . . . . . . . 11 ((𝑤𝐵 ↦ (1o × {𝑤})):𝐵1-1-onto→(𝐵m 1o) → (𝑤𝐵 ↦ (1o × {𝑤})):𝐵⟶(𝐵m 1o))
7169, 70mp1i 13 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → (𝑤𝐵 ↦ (1o × {𝑤})):𝐵⟶(𝐵m 1o))
72 ovexd 7174 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → (𝐵m 1o) ∈ V)
734a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → 𝐵 ∈ V)
74 inidm 4148 . . . . . . . . . 10 ((𝐵m 1o) ∩ (𝐵m 1o)) = (𝐵m 1o)
7564, 67, 71, 72, 72, 73, 74ofco 7413 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → ((𝑎f + 𝑏) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) = ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f + (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))))
7675eleq1d 2877 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → (((𝑎f + 𝑏) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ↔ ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f + (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥𝜓}))
7761, 76sylibrd 262 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → (((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) → ((𝑎f + 𝑏) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
7877expimpd 457 . . . . . 6 (𝜑 → (((𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅)) ∧ ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓})) → ((𝑎f + 𝑏) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
7926, 78syl5bi 245 . . . . 5 (𝜑 → (((𝑎 ∈ ran (1o eval 𝑅) ∧ (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) ∧ (𝑏 ∈ ran (1o eval 𝑅) ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓})) → ((𝑎f + 𝑏) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
8079imp 410 . . . 4 ((𝜑 ∧ ((𝑎 ∈ ran (1o eval 𝑅) ∧ (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) ∧ (𝑏 ∈ ran (1o eval 𝑅) ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))) → ((𝑎f + 𝑏) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓})
81 ovex 7172 . . . . . . . . . . . . . . 15 (𝑓f · 𝑔) ∈ V
82 pf1ind.wf . . . . . . . . . . . . . . 15 (𝑥 = (𝑓f · 𝑔) → (𝜓𝜎))
8381, 82elab 3618 . . . . . . . . . . . . . 14 ((𝑓f · 𝑔) ∈ {𝑥𝜓} ↔ 𝜎)
84 oveq1 7146 . . . . . . . . . . . . . . 15 (𝑓 = (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → (𝑓f · 𝑔) = ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f · 𝑔))
8584eleq1d 2877 . . . . . . . . . . . . . 14 (𝑓 = (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → ((𝑓f · 𝑔) ∈ {𝑥𝜓} ↔ ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f · 𝑔) ∈ {𝑥𝜓}))
8683, 85bitr3id 288 . . . . . . . . . . . . 13 (𝑓 = (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → (𝜎 ↔ ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f · 𝑔) ∈ {𝑥𝜓}))
8736, 86imbi12d 348 . . . . . . . . . . . 12 (𝑓 = (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → ((((𝜏𝜂) ∧ 𝜑) → 𝜎) ↔ ((((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ 𝜂) ∧ 𝜑) → ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f · 𝑔) ∈ {𝑥𝜓})))
88 oveq2 7147 . . . . . . . . . . . . . 14 (𝑔 = (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f · 𝑔) = ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f · (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))))
8988eleq1d 2877 . . . . . . . . . . . . 13 (𝑔 = (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → (((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f · 𝑔) ∈ {𝑥𝜓} ↔ ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f · (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥𝜓}))
9050, 89imbi12d 348 . . . . . . . . . . . 12 (𝑔 = (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → (((((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ 𝜂) ∧ 𝜑) → ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f · 𝑔) ∈ {𝑥𝜓}) ↔ ((((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) ∧ 𝜑) → ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f · (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥𝜓})))
91 pf1ind.mu . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑓𝑄𝜏) ∧ (𝑔𝑄𝜂))) → 𝜎)
9291expcom 417 . . . . . . . . . . . . . 14 (((𝑓𝑄𝜏) ∧ (𝑔𝑄𝜂)) → (𝜑𝜎))
9392an4s 659 . . . . . . . . . . . . 13 (((𝑓𝑄𝑔𝑄) ∧ (𝜏𝜂)) → (𝜑𝜎))
9493expimpd 457 . . . . . . . . . . . 12 ((𝑓𝑄𝑔𝑄) → (((𝜏𝜂) ∧ 𝜑) → 𝜎))
9587, 90, 94vtocl2ga 3526 . . . . . . . . . . 11 (((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ 𝑄 ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ 𝑄) → ((((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) ∧ 𝜑) → ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f · (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥𝜓}))
9628, 29, 95syl2an 598 . . . . . . . . . 10 ((𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅)) → ((((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) ∧ 𝜑) → ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f · (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥𝜓}))
9796expcomd 420 . . . . . . . . 9 ((𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅)) → (𝜑 → (((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) → ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f · (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥𝜓})))
9897impcom 411 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → (((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) → ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f · (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥𝜓}))
9964, 67, 71, 72, 72, 73, 74ofco 7413 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → ((𝑎f · 𝑏) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) = ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f · (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))))
10099eleq1d 2877 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → (((𝑎f · 𝑏) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ↔ ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f · (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥𝜓}))
10198, 100sylibrd 262 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → (((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) → ((𝑎f · 𝑏) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
102101expimpd 457 . . . . . 6 (𝜑 → (((𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅)) ∧ ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓})) → ((𝑎f · 𝑏) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
10326, 102syl5bi 245 . . . . 5 (𝜑 → (((𝑎 ∈ ran (1o eval 𝑅) ∧ (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) ∧ (𝑏 ∈ ran (1o eval 𝑅) ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓})) → ((𝑎f · 𝑏) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
104103imp 410 . . . 4 ((𝜑 ∧ ((𝑎 ∈ ran (1o eval 𝑅) ∧ (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) ∧ (𝑏 ∈ ran (1o eval 𝑅) ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))) → ((𝑎f · 𝑏) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓})
105 coeq1 5696 . . . . 5 (𝑦 = ((𝐵m 1o) × {𝑎}) → (𝑦 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) = (((𝐵m 1o) × {𝑎}) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))))
106105eleq1d 2877 . . . 4 (𝑦 = ((𝐵m 1o) × {𝑎}) → ((𝑦 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ↔ (((𝐵m 1o) × {𝑎}) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
107 coeq1 5696 . . . . 5 (𝑦 = (𝑏 ∈ (𝐵m 1o) ↦ (𝑏𝑎)) → (𝑦 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) = ((𝑏 ∈ (𝐵m 1o) ↦ (𝑏𝑎)) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))))
108107eleq1d 2877 . . . 4 (𝑦 = (𝑏 ∈ (𝐵m 1o) ↦ (𝑏𝑎)) → ((𝑦 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ↔ ((𝑏 ∈ (𝐵m 1o) ↦ (𝑏𝑎)) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
109 coeq1 5696 . . . . 5 (𝑦 = 𝑎 → (𝑦 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) = (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))))
110109eleq1d 2877 . . . 4 (𝑦 = 𝑎 → ((𝑦 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ↔ (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
111 coeq1 5696 . . . . 5 (𝑦 = 𝑏 → (𝑦 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) = (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))))
112111eleq1d 2877 . . . 4 (𝑦 = 𝑏 → ((𝑦 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ↔ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
113 coeq1 5696 . . . . 5 (𝑦 = (𝑎f + 𝑏) → (𝑦 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) = ((𝑎f + 𝑏) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))))
114113eleq1d 2877 . . . 4 (𝑦 = (𝑎f + 𝑏) → ((𝑦 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ↔ ((𝑎f + 𝑏) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
115 coeq1 5696 . . . . 5 (𝑦 = (𝑎f · 𝑏) → (𝑦 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) = ((𝑎f · 𝑏) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))))
116115eleq1d 2877 . . . 4 (𝑦 = (𝑎f · 𝑏) → ((𝑦 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ↔ ((𝑎f · 𝑏) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
117 coeq1 5696 . . . . 5 (𝑦 = (𝐴 ∘ (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅))) → (𝑦 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) = ((𝐴 ∘ (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅))) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))))
118117eleq1d 2877 . . . 4 (𝑦 = (𝐴 ∘ (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅))) → ((𝑦 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ↔ ((𝐴 ∘ (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅))) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
11916pf1rcl 20977 . . . . . . . . 9 (𝐴𝑄𝑅 ∈ CRing)
12015, 119syl 17 . . . . . . . 8 (𝜑𝑅 ∈ CRing)
121120adantr 484 . . . . . . 7 ((𝜑𝑎𝐵) → 𝑅 ∈ CRing)
122 1on 8096 . . . . . . . . . . . 12 1o ∈ On
123 eqid 2801 . . . . . . . . . . . . 13 (1o mPoly 𝑅) = (1o mPoly 𝑅)
124123mplassa 20698 . . . . . . . . . . . 12 ((1o ∈ On ∧ 𝑅 ∈ CRing) → (1o mPoly 𝑅) ∈ AssAlg)
125122, 120, 124sylancr 590 . . . . . . . . . . 11 (𝜑 → (1o mPoly 𝑅) ∈ AssAlg)
126 eqid 2801 . . . . . . . . . . . . 13 (Poly1𝑅) = (Poly1𝑅)
127 eqid 2801 . . . . . . . . . . . . 13 (algSc‘(Poly1𝑅)) = (algSc‘(Poly1𝑅))
128126, 127ply1ascl 20891 . . . . . . . . . . . 12 (algSc‘(Poly1𝑅)) = (algSc‘(1o mPoly 𝑅))
129 eqid 2801 . . . . . . . . . . . 12 (Scalar‘(1o mPoly 𝑅)) = (Scalar‘(1o mPoly 𝑅))
130128, 129asclrhm 20580 . . . . . . . . . . 11 ((1o mPoly 𝑅) ∈ AssAlg → (algSc‘(Poly1𝑅)) ∈ ((Scalar‘(1o mPoly 𝑅)) RingHom (1o mPoly 𝑅)))
131125, 130syl 17 . . . . . . . . . 10 (𝜑 → (algSc‘(Poly1𝑅)) ∈ ((Scalar‘(1o mPoly 𝑅)) RingHom (1o mPoly 𝑅)))
132122a1i 11 . . . . . . . . . . . 12 (𝜑 → 1o ∈ On)
133123, 132, 120mplsca 20688 . . . . . . . . . . 11 (𝜑𝑅 = (Scalar‘(1o mPoly 𝑅)))
134133oveq1d 7154 . . . . . . . . . 10 (𝜑 → (𝑅 RingHom (1o mPoly 𝑅)) = ((Scalar‘(1o mPoly 𝑅)) RingHom (1o mPoly 𝑅)))
135131, 134eleqtrrd 2896 . . . . . . . . 9 (𝜑 → (algSc‘(Poly1𝑅)) ∈ (𝑅 RingHom (1o mPoly 𝑅)))
136 eqid 2801 . . . . . . . . . 10 (Base‘(1o mPoly 𝑅)) = (Base‘(1o mPoly 𝑅))
1373, 136rhmf 19478 . . . . . . . . 9 ((algSc‘(Poly1𝑅)) ∈ (𝑅 RingHom (1o mPoly 𝑅)) → (algSc‘(Poly1𝑅)):𝐵⟶(Base‘(1o mPoly 𝑅)))
138135, 137syl 17 . . . . . . . 8 (𝜑 → (algSc‘(Poly1𝑅)):𝐵⟶(Base‘(1o mPoly 𝑅)))
139138ffvelrnda 6832 . . . . . . 7 ((𝜑𝑎𝐵) → ((algSc‘(Poly1𝑅))‘𝑎) ∈ (Base‘(1o mPoly 𝑅)))
140 eqid 2801 . . . . . . . 8 (eval1𝑅) = (eval1𝑅)
141140, 23, 3, 123, 136evl1val 20957 . . . . . . 7 ((𝑅 ∈ CRing ∧ ((algSc‘(Poly1𝑅))‘𝑎) ∈ (Base‘(1o mPoly 𝑅))) → ((eval1𝑅)‘((algSc‘(Poly1𝑅))‘𝑎)) = (((1o eval 𝑅)‘((algSc‘(Poly1𝑅))‘𝑎)) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))))
142121, 139, 141syl2anc 587 . . . . . 6 ((𝜑𝑎𝐵) → ((eval1𝑅)‘((algSc‘(Poly1𝑅))‘𝑎)) = (((1o eval 𝑅)‘((algSc‘(Poly1𝑅))‘𝑎)) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))))
143140, 126, 3, 127evl1sca 20962 . . . . . . 7 ((𝑅 ∈ CRing ∧ 𝑎𝐵) → ((eval1𝑅)‘((algSc‘(Poly1𝑅))‘𝑎)) = (𝐵 × {𝑎}))
144120, 143sylan 583 . . . . . 6 ((𝜑𝑎𝐵) → ((eval1𝑅)‘((algSc‘(Poly1𝑅))‘𝑎)) = (𝐵 × {𝑎}))
1453ressid 16555 . . . . . . . . . . . . . 14 (𝑅 ∈ CRing → (𝑅s 𝐵) = 𝑅)
146121, 145syl 17 . . . . . . . . . . . . 13 ((𝜑𝑎𝐵) → (𝑅s 𝐵) = 𝑅)
147146oveq2d 7155 . . . . . . . . . . . 12 ((𝜑𝑎𝐵) → (1o mPoly (𝑅s 𝐵)) = (1o mPoly 𝑅))
148147fveq2d 6653 . . . . . . . . . . 11 ((𝜑𝑎𝐵) → (algSc‘(1o mPoly (𝑅s 𝐵))) = (algSc‘(1o mPoly 𝑅)))
149148, 128eqtr4di 2854 . . . . . . . . . 10 ((𝜑𝑎𝐵) → (algSc‘(1o mPoly (𝑅s 𝐵))) = (algSc‘(Poly1𝑅)))
150149fveq1d 6651 . . . . . . . . 9 ((𝜑𝑎𝐵) → ((algSc‘(1o mPoly (𝑅s 𝐵)))‘𝑎) = ((algSc‘(Poly1𝑅))‘𝑎))
151150fveq2d 6653 . . . . . . . 8 ((𝜑𝑎𝐵) → ((1o eval 𝑅)‘((algSc‘(1o mPoly (𝑅s 𝐵)))‘𝑎)) = ((1o eval 𝑅)‘((algSc‘(Poly1𝑅))‘𝑎)))
152 eqid 2801 . . . . . . . . 9 (1o mPoly (𝑅s 𝐵)) = (1o mPoly (𝑅s 𝐵))
153 eqid 2801 . . . . . . . . 9 (𝑅s 𝐵) = (𝑅s 𝐵)
154 eqid 2801 . . . . . . . . 9 (algSc‘(1o mPoly (𝑅s 𝐵))) = (algSc‘(1o mPoly (𝑅s 𝐵)))
155122a1i 11 . . . . . . . . 9 ((𝜑𝑎𝐵) → 1o ∈ On)
156 crngring 19306 . . . . . . . . . . 11 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
1573subrgid 19534 . . . . . . . . . . 11 (𝑅 ∈ Ring → 𝐵 ∈ (SubRing‘𝑅))
158120, 156, 1573syl 18 . . . . . . . . . 10 (𝜑𝐵 ∈ (SubRing‘𝑅))
159158adantr 484 . . . . . . . . 9 ((𝜑𝑎𝐵) → 𝐵 ∈ (SubRing‘𝑅))
160 simpr 488 . . . . . . . . 9 ((𝜑𝑎𝐵) → 𝑎𝐵)
16124, 152, 153, 3, 154, 155, 121, 159, 160evlssca 20765 . . . . . . . 8 ((𝜑𝑎𝐵) → ((1o eval 𝑅)‘((algSc‘(1o mPoly (𝑅s 𝐵)))‘𝑎)) = ((𝐵m 1o) × {𝑎}))
162151, 161eqtr3d 2838 . . . . . . 7 ((𝜑𝑎𝐵) → ((1o eval 𝑅)‘((algSc‘(Poly1𝑅))‘𝑎)) = ((𝐵m 1o) × {𝑎}))
163162coeq1d 5700 . . . . . 6 ((𝜑𝑎𝐵) → (((1o eval 𝑅)‘((algSc‘(Poly1𝑅))‘𝑎)) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) = (((𝐵m 1o) × {𝑎}) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))))
164142, 144, 1633eqtr3d 2844 . . . . 5 ((𝜑𝑎𝐵) → (𝐵 × {𝑎}) = (((𝐵m 1o) × {𝑎}) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))))
165 pf1ind.co . . . . . . . 8 ((𝜑𝑓𝐵) → 𝜒)
166 snex 5300 . . . . . . . . . 10 {𝑓} ∈ V
1674, 166xpex 7460 . . . . . . . . 9 (𝐵 × {𝑓}) ∈ V
168 pf1ind.wa . . . . . . . . 9 (𝑥 = (𝐵 × {𝑓}) → (𝜓𝜒))
169167, 168elab 3618 . . . . . . . 8 ((𝐵 × {𝑓}) ∈ {𝑥𝜓} ↔ 𝜒)
170165, 169sylibr 237 . . . . . . 7 ((𝜑𝑓𝐵) → (𝐵 × {𝑓}) ∈ {𝑥𝜓})
171170ralrimiva 3152 . . . . . 6 (𝜑 → ∀𝑓𝐵 (𝐵 × {𝑓}) ∈ {𝑥𝜓})
172 sneq 4538 . . . . . . . . 9 (𝑓 = 𝑎 → {𝑓} = {𝑎})
173172xpeq2d 5553 . . . . . . . 8 (𝑓 = 𝑎 → (𝐵 × {𝑓}) = (𝐵 × {𝑎}))
174173eleq1d 2877 . . . . . . 7 (𝑓 = 𝑎 → ((𝐵 × {𝑓}) ∈ {𝑥𝜓} ↔ (𝐵 × {𝑎}) ∈ {𝑥𝜓}))
175174rspccva 3573 . . . . . 6 ((∀𝑓𝐵 (𝐵 × {𝑓}) ∈ {𝑥𝜓} ∧ 𝑎𝐵) → (𝐵 × {𝑎}) ∈ {𝑥𝜓})
176171, 175sylan 583 . . . . 5 ((𝜑𝑎𝐵) → (𝐵 × {𝑎}) ∈ {𝑥𝜓})
177164, 176eqeltrrd 2894 . . . 4 ((𝜑𝑎𝐵) → (((𝐵m 1o) × {𝑎}) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓})
178 pf1ind.pr . . . . . . . 8 (𝜑𝜃)
179 resiexg 7605 . . . . . . . . . 10 (𝐵 ∈ V → ( I ↾ 𝐵) ∈ V)
1804, 179ax-mp 5 . . . . . . . . 9 ( I ↾ 𝐵) ∈ V
181 pf1ind.wb . . . . . . . . 9 (𝑥 = ( I ↾ 𝐵) → (𝜓𝜃))
182180, 181elab 3618 . . . . . . . 8 (( I ↾ 𝐵) ∈ {𝑥𝜓} ↔ 𝜃)
183178, 182sylibr 237 . . . . . . 7 (𝜑 → ( I ↾ 𝐵) ∈ {𝑥𝜓})
18412, 183eqeltrd 2893 . . . . . 6 (𝜑 → ((𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅)) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓})
185 el1o 8111 . . . . . . . . . 10 (𝑎 ∈ 1o𝑎 = ∅)
186 fveq2 6649 . . . . . . . . . 10 (𝑎 = ∅ → (𝑏𝑎) = (𝑏‘∅))
187185, 186sylbi 220 . . . . . . . . 9 (𝑎 ∈ 1o → (𝑏𝑎) = (𝑏‘∅))
188187mpteq2dv 5129 . . . . . . . 8 (𝑎 ∈ 1o → (𝑏 ∈ (𝐵m 1o) ↦ (𝑏𝑎)) = (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅)))
189188coeq1d 5700 . . . . . . 7 (𝑎 ∈ 1o → ((𝑏 ∈ (𝐵m 1o) ↦ (𝑏𝑎)) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) = ((𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅)) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))))
190189eleq1d 2877 . . . . . 6 (𝑎 ∈ 1o → (((𝑏 ∈ (𝐵m 1o) ↦ (𝑏𝑎)) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ↔ ((𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅)) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
191184, 190syl5ibrcom 250 . . . . 5 (𝜑 → (𝑎 ∈ 1o → ((𝑏 ∈ (𝐵m 1o) ↦ (𝑏𝑎)) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
192191imp 410 . . . 4 ((𝜑𝑎 ∈ 1o) → ((𝑏 ∈ (𝐵m 1o) ↦ (𝑏𝑎)) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓})
19316, 3, 27pf1mpf 20980 . . . . 5 (𝐴𝑄 → (𝐴 ∘ (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅))) ∈ ran (1o eval 𝑅))
19415, 193syl 17 . . . 4 (𝜑 → (𝐴 ∘ (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅))) ∈ ran (1o eval 𝑅))
1953, 21, 22, 25, 80, 104, 106, 108, 110, 112, 114, 116, 118, 177, 192, 194mpfind 20783 . . 3 (𝜑 → ((𝐴 ∘ (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅))) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓})
19620, 195eqeltrrd 2894 . 2 (𝜑𝐴 ∈ {𝑥𝜓})
197 pf1ind.wg . . . 4 (𝑥 = 𝐴 → (𝜓𝜌))
198197elabg 3617 . . 3 (𝐴𝑄 → (𝐴 ∈ {𝑥𝜓} ↔ 𝜌))
19915, 198syl 17 . 2 (𝜑 → (𝐴 ∈ {𝑥𝜓} ↔ 𝜌))
200196, 199mpbid 235 1 (𝜑𝜌)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wcel 2112  {cab 2779  wral 3109  Vcvv 3444  c0 4246  {csn 4528  cmpt 5113   I cid 5427   × cxp 5521  ccnv 5522  ran crn 5524  cres 5525  ccom 5527  Oncon0 6163  wf 6324  1-1-ontowf1o 6327  cfv 6328  (class class class)co 7139  f cof 7391  1oc1o 8082  m cmap 8393  Basecbs 16479  s cress 16480  +gcplusg 16561  .rcmulr 16562  Scalarcsca 16564  Ringcrg 19294  CRingccrg 19295   RingHom crh 19464  SubRingcsubrg 19528  AssAlgcasa 20543  algSccascl 20545   mPoly cmpl 20595   evalSub ces 20747   eval cevl 20748  Poly1cpl1 20810  eval1ce1 20942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-of 7393  df-ofr 7394  df-om 7565  df-1st 7675  df-2nd 7676  df-supp 7818  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-2o 8090  df-oadd 8093  df-er 8276  df-map 8395  df-pm 8396  df-ixp 8449  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-fsupp 8822  df-sup 8894  df-oi 8962  df-card 9356  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-nn 11630  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-z 11974  df-dec 12091  df-uz 12236  df-fz 12890  df-fzo 13033  df-seq 13369  df-hash 13691  df-struct 16481  df-ndx 16482  df-slot 16483  df-base 16485  df-sets 16486  df-ress 16487  df-plusg 16574  df-mulr 16575  df-sca 16577  df-vsca 16578  df-ip 16579  df-tset 16580  df-ple 16581  df-ds 16583  df-hom 16585  df-cco 16586  df-0g 16711  df-gsum 16712  df-prds 16717  df-pws 16719  df-mre 16853  df-mrc 16854  df-acs 16856  df-mgm 17848  df-sgrp 17897  df-mnd 17908  df-mhm 17952  df-submnd 17953  df-grp 18102  df-minusg 18103  df-sbg 18104  df-mulg 18221  df-subg 18272  df-ghm 18352  df-cntz 18443  df-cmn 18904  df-abl 18905  df-mgp 19237  df-ur 19249  df-srg 19253  df-ring 19296  df-cring 19297  df-rnghom 19467  df-subrg 19530  df-lmod 19633  df-lss 19701  df-lsp 19741  df-assa 20546  df-asp 20547  df-ascl 20548  df-psr 20598  df-mvr 20599  df-mpl 20600  df-opsr 20602  df-evls 20749  df-evl 20750  df-psr1 20813  df-ply1 20815  df-evl1 20944
This theorem is referenced by:  pl1cn  31312
  Copyright terms: Public domain W3C validator