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

Theorem pf1ind 21604
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 6191 . . . . 5 ((𝐴 ∘ (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅))) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) = (𝐴 ∘ ((𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅)) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))))
2 df1o2 8353 . . . . . . . . 9 1o = {∅}
3 pf1ind.cb . . . . . . . . . 10 𝐵 = (Base‘𝑅)
43fvexi 6826 . . . . . . . . 9 𝐵 ∈ V
5 0ex 5246 . . . . . . . . 9 ∅ ∈ V
6 eqid 2737 . . . . . . . . 9 (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅)) = (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅))
72, 4, 5, 6mapsncnv 8731 . . . . . . . 8 (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅)) = (𝑤𝐵 ↦ (1o × {𝑤}))
87coeq2i 5790 . . . . . . 7 ((𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅)) ∘ (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅))) = ((𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅)) ∘ (𝑤𝐵 ↦ (1o × {𝑤})))
92, 4, 5, 6mapsnf1o2 8732 . . . . . . . 8 (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅)):(𝐵m 1o)–1-1-onto𝐵
10 f1ococnv2 6781 . . . . . . . 8 ((𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅)):(𝐵m 1o)–1-1-onto𝐵 → ((𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅)) ∘ (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅))) = ( I ↾ 𝐵))
119, 10mp1i 13 . . . . . . 7 (𝜑 → ((𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅)) ∘ (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅))) = ( I ↾ 𝐵))
128, 11eqtr3id 2791 . . . . . 6 (𝜑 → ((𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅)) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) = ( I ↾ 𝐵))
1312coeq2d 5792 . . . . 5 (𝜑 → (𝐴 ∘ ((𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅)) ∘ (𝑤𝐵 ↦ (1o × {𝑤})))) = (𝐴 ∘ ( I ↾ 𝐵)))
141, 13eqtrid 2789 . . . 4 (𝜑 → ((𝐴 ∘ (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅))) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) = (𝐴 ∘ ( I ↾ 𝐵)))
15 pf1ind.a . . . . 5 (𝜑𝐴𝑄)
16 pf1ind.cq . . . . . 6 𝑄 = ran (eval1𝑅)
1716, 3pf1f 21599 . . . . 5 (𝐴𝑄𝐴:𝐵𝐵)
18 fcoi1 6686 . . . . 5 (𝐴:𝐵𝐵 → (𝐴 ∘ ( I ↾ 𝐵)) = 𝐴)
1915, 17, 183syl 18 . . . 4 (𝜑 → (𝐴 ∘ ( I ↾ 𝐵)) = 𝐴)
2014, 19eqtrd 2777 . . 3 (𝜑 → ((𝐴 ∘ (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅))) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) = 𝐴)
21 pf1ind.cp . . . 4 + = (+g𝑅)
22 pf1ind.ct . . . 4 · = (.r𝑅)
23 eqid 2737 . . . . . 6 (1o eval 𝑅) = (1o eval 𝑅)
2423, 3evlval 21388 . . . . 5 (1o eval 𝑅) = ((1o evalSub 𝑅)‘𝐵)
2524rneqi 5866 . . . 4 ran (1o eval 𝑅) = ran ((1o evalSub 𝑅)‘𝐵)
26 an4 653 . . . . . 6 (((𝑎 ∈ ran (1o eval 𝑅) ∧ (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) ∧ (𝑏 ∈ ran (1o eval 𝑅) ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓})) ↔ ((𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅)) ∧ ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓})))
27 eqid 2737 . . . . . . . . . . . 12 ran (1o eval 𝑅) = ran (1o eval 𝑅)
2816, 3, 27mpfpf1 21600 . . . . . . . . . . 11 (𝑎 ∈ ran (1o eval 𝑅) → (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ 𝑄)
2916, 3, 27mpfpf1 21600 . . . . . . . . . . 11 (𝑏 ∈ ran (1o eval 𝑅) → (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ 𝑄)
30 vex 3445 . . . . . . . . . . . . . . . . 17 𝑓 ∈ V
31 pf1ind.wc . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑓 → (𝜓𝜏))
3230, 31elab 3619 . . . . . . . . . . . . . . . 16 (𝑓 ∈ {𝑥𝜓} ↔ 𝜏)
33 eleq1 2825 . . . . . . . . . . . . . . . 16 (𝑓 = (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → (𝑓 ∈ {𝑥𝜓} ↔ (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
3432, 33bitr3id 284 . . . . . . . . . . . . . . 15 (𝑓 = (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → (𝜏 ↔ (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
3534anbi1d 630 . . . . . . . . . . . . . 14 (𝑓 = (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → ((𝜏𝜂) ↔ ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ 𝜂)))
3635anbi1d 630 . . . . . . . . . . . . 13 (𝑓 = (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → (((𝜏𝜂) ∧ 𝜑) ↔ (((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ 𝜂) ∧ 𝜑)))
37 ovex 7350 . . . . . . . . . . . . . . 15 (𝑓f + 𝑔) ∈ V
38 pf1ind.we . . . . . . . . . . . . . . 15 (𝑥 = (𝑓f + 𝑔) → (𝜓𝜁))
3937, 38elab 3619 . . . . . . . . . . . . . 14 ((𝑓f + 𝑔) ∈ {𝑥𝜓} ↔ 𝜁)
40 oveq1 7324 . . . . . . . . . . . . . . 15 (𝑓 = (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → (𝑓f + 𝑔) = ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f + 𝑔))
4140eleq1d 2822 . . . . . . . . . . . . . 14 (𝑓 = (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → ((𝑓f + 𝑔) ∈ {𝑥𝜓} ↔ ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f + 𝑔) ∈ {𝑥𝜓}))
4239, 41bitr3id 284 . . . . . . . . . . . . 13 (𝑓 = (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → (𝜁 ↔ ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f + 𝑔) ∈ {𝑥𝜓}))
4336, 42imbi12d 344 . . . . . . . . . . . 12 (𝑓 = (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → ((((𝜏𝜂) ∧ 𝜑) → 𝜁) ↔ ((((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ 𝜂) ∧ 𝜑) → ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f + 𝑔) ∈ {𝑥𝜓})))
44 vex 3445 . . . . . . . . . . . . . . . . 17 𝑔 ∈ V
45 pf1ind.wd . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑔 → (𝜓𝜂))
4644, 45elab 3619 . . . . . . . . . . . . . . . 16 (𝑔 ∈ {𝑥𝜓} ↔ 𝜂)
47 eleq1 2825 . . . . . . . . . . . . . . . 16 (𝑔 = (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → (𝑔 ∈ {𝑥𝜓} ↔ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
4846, 47bitr3id 284 . . . . . . . . . . . . . . 15 (𝑔 = (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → (𝜂 ↔ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
4948anbi2d 629 . . . . . . . . . . . . . 14 (𝑔 = (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → (((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ 𝜂) ↔ ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓})))
5049anbi1d 630 . . . . . . . . . . . . 13 (𝑔 = (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → ((((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ 𝜂) ∧ 𝜑) ↔ (((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) ∧ 𝜑)))
51 oveq2 7325 . . . . . . . . . . . . . 14 (𝑔 = (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f + 𝑔) = ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f + (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))))
5251eleq1d 2822 . . . . . . . . . . . . 13 (𝑔 = (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → (((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f + 𝑔) ∈ {𝑥𝜓} ↔ ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f + (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥𝜓}))
5350, 52imbi12d 344 . . . . . . . . . . . 12 (𝑔 = (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → (((((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ 𝜂) ∧ 𝜑) → ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f + 𝑔) ∈ {𝑥𝜓}) ↔ ((((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) ∧ 𝜑) → ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f + (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥𝜓})))
54 pf1ind.ad . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑓𝑄𝜏) ∧ (𝑔𝑄𝜂))) → 𝜁)
5554expcom 414 . . . . . . . . . . . . . 14 (((𝑓𝑄𝜏) ∧ (𝑔𝑄𝜂)) → (𝜑𝜁))
5655an4s 657 . . . . . . . . . . . . 13 (((𝑓𝑄𝑔𝑄) ∧ (𝜏𝜂)) → (𝜑𝜁))
5756expimpd 454 . . . . . . . . . . . 12 ((𝑓𝑄𝑔𝑄) → (((𝜏𝜂) ∧ 𝜑) → 𝜁))
5843, 53, 57vtocl2ga 3523 . . . . . . . . . . 11 (((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ 𝑄 ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ 𝑄) → ((((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) ∧ 𝜑) → ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f + (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥𝜓}))
5928, 29, 58syl2an 596 . . . . . . . . . 10 ((𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅)) → ((((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) ∧ 𝜑) → ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f + (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥𝜓}))
6059expcomd 417 . . . . . . . . 9 ((𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅)) → (𝜑 → (((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) → ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f + (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥𝜓})))
6160impcom 408 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → (((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) → ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f + (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥𝜓}))
6225, 3mpff 21397 . . . . . . . . . . . 12 (𝑎 ∈ ran (1o eval 𝑅) → 𝑎:(𝐵m 1o)⟶𝐵)
6362ad2antrl 725 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → 𝑎:(𝐵m 1o)⟶𝐵)
6463ffnd 6639 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → 𝑎 Fn (𝐵m 1o))
6525, 3mpff 21397 . . . . . . . . . . . 12 (𝑏 ∈ ran (1o eval 𝑅) → 𝑏:(𝐵m 1o)⟶𝐵)
6665ad2antll 726 . . . . . . . . . . 11 ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → 𝑏:(𝐵m 1o)⟶𝐵)
6766ffnd 6639 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → 𝑏 Fn (𝐵m 1o))
68 eqid 2737 . . . . . . . . . . . 12 (𝑤𝐵 ↦ (1o × {𝑤})) = (𝑤𝐵 ↦ (1o × {𝑤}))
692, 4, 5, 68mapsnf1o3 8733 . . . . . . . . . . 11 (𝑤𝐵 ↦ (1o × {𝑤})):𝐵1-1-onto→(𝐵m 1o)
70 f1of 6754 . . . . . . . . . . 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 7352 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → (𝐵m 1o) ∈ V)
734a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → 𝐵 ∈ V)
74 inidm 4163 . . . . . . . . . 10 ((𝐵m 1o) ∩ (𝐵m 1o)) = (𝐵m 1o)
7564, 67, 71, 72, 72, 73, 74ofco 7598 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → ((𝑎f + 𝑏) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) = ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f + (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))))
7675eleq1d 2822 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → (((𝑎f + 𝑏) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ↔ ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f + (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥𝜓}))
7761, 76sylibrd 258 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → (((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) → ((𝑎f + 𝑏) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
7877expimpd 454 . . . . . 6 (𝜑 → (((𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅)) ∧ ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓})) → ((𝑎f + 𝑏) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
7926, 78biimtrid 241 . . . . 5 (𝜑 → (((𝑎 ∈ ran (1o eval 𝑅) ∧ (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) ∧ (𝑏 ∈ ran (1o eval 𝑅) ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓})) → ((𝑎f + 𝑏) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
8079imp 407 . . . 4 ((𝜑 ∧ ((𝑎 ∈ ran (1o eval 𝑅) ∧ (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) ∧ (𝑏 ∈ ran (1o eval 𝑅) ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))) → ((𝑎f + 𝑏) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓})
81 ovex 7350 . . . . . . . . . . . . . . 15 (𝑓f · 𝑔) ∈ V
82 pf1ind.wf . . . . . . . . . . . . . . 15 (𝑥 = (𝑓f · 𝑔) → (𝜓𝜎))
8381, 82elab 3619 . . . . . . . . . . . . . 14 ((𝑓f · 𝑔) ∈ {𝑥𝜓} ↔ 𝜎)
84 oveq1 7324 . . . . . . . . . . . . . . 15 (𝑓 = (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → (𝑓f · 𝑔) = ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f · 𝑔))
8584eleq1d 2822 . . . . . . . . . . . . . 14 (𝑓 = (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → ((𝑓f · 𝑔) ∈ {𝑥𝜓} ↔ ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f · 𝑔) ∈ {𝑥𝜓}))
8683, 85bitr3id 284 . . . . . . . . . . . . 13 (𝑓 = (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → (𝜎 ↔ ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f · 𝑔) ∈ {𝑥𝜓}))
8736, 86imbi12d 344 . . . . . . . . . . . 12 (𝑓 = (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → ((((𝜏𝜂) ∧ 𝜑) → 𝜎) ↔ ((((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ 𝜂) ∧ 𝜑) → ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f · 𝑔) ∈ {𝑥𝜓})))
88 oveq2 7325 . . . . . . . . . . . . . 14 (𝑔 = (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f · 𝑔) = ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f · (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))))
8988eleq1d 2822 . . . . . . . . . . . . 13 (𝑔 = (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → (((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f · 𝑔) ∈ {𝑥𝜓} ↔ ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f · (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥𝜓}))
9050, 89imbi12d 344 . . . . . . . . . . . 12 (𝑔 = (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) → (((((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ 𝜂) ∧ 𝜑) → ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f · 𝑔) ∈ {𝑥𝜓}) ↔ ((((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) ∧ 𝜑) → ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f · (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥𝜓})))
91 pf1ind.mu . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑓𝑄𝜏) ∧ (𝑔𝑄𝜂))) → 𝜎)
9291expcom 414 . . . . . . . . . . . . . 14 (((𝑓𝑄𝜏) ∧ (𝑔𝑄𝜂)) → (𝜑𝜎))
9392an4s 657 . . . . . . . . . . . . 13 (((𝑓𝑄𝑔𝑄) ∧ (𝜏𝜂)) → (𝜑𝜎))
9493expimpd 454 . . . . . . . . . . . 12 ((𝑓𝑄𝑔𝑄) → (((𝜏𝜂) ∧ 𝜑) → 𝜎))
9587, 90, 94vtocl2ga 3523 . . . . . . . . . . 11 (((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ 𝑄 ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ 𝑄) → ((((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) ∧ 𝜑) → ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f · (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥𝜓}))
9628, 29, 95syl2an 596 . . . . . . . . . 10 ((𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅)) → ((((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) ∧ 𝜑) → ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f · (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥𝜓}))
9796expcomd 417 . . . . . . . . 9 ((𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅)) → (𝜑 → (((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) → ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f · (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥𝜓})))
9897impcom 408 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → (((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) → ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f · (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥𝜓}))
9964, 67, 71, 72, 72, 73, 74ofco 7598 . . . . . . . . 9 ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → ((𝑎f · 𝑏) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) = ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f · (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))))
10099eleq1d 2822 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → (((𝑎f · 𝑏) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ↔ ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∘f · (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤})))) ∈ {𝑥𝜓}))
10198, 100sylibrd 258 . . . . . . 7 ((𝜑 ∧ (𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅))) → (((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) → ((𝑎f · 𝑏) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
102101expimpd 454 . . . . . 6 (𝜑 → (((𝑎 ∈ ran (1o eval 𝑅) ∧ 𝑏 ∈ ran (1o eval 𝑅)) ∧ ((𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓})) → ((𝑎f · 𝑏) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
10326, 102biimtrid 241 . . . . 5 (𝜑 → (((𝑎 ∈ ran (1o eval 𝑅) ∧ (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) ∧ (𝑏 ∈ ran (1o eval 𝑅) ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓})) → ((𝑎f · 𝑏) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
104103imp 407 . . . 4 ((𝜑 ∧ ((𝑎 ∈ ran (1o eval 𝑅) ∧ (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}) ∧ (𝑏 ∈ ran (1o eval 𝑅) ∧ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))) → ((𝑎f · 𝑏) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓})
105 coeq1 5787 . . . . 5 (𝑦 = ((𝐵m 1o) × {𝑎}) → (𝑦 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) = (((𝐵m 1o) × {𝑎}) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))))
106105eleq1d 2822 . . . 4 (𝑦 = ((𝐵m 1o) × {𝑎}) → ((𝑦 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ↔ (((𝐵m 1o) × {𝑎}) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
107 coeq1 5787 . . . . 5 (𝑦 = (𝑏 ∈ (𝐵m 1o) ↦ (𝑏𝑎)) → (𝑦 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) = ((𝑏 ∈ (𝐵m 1o) ↦ (𝑏𝑎)) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))))
108107eleq1d 2822 . . . 4 (𝑦 = (𝑏 ∈ (𝐵m 1o) ↦ (𝑏𝑎)) → ((𝑦 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ↔ ((𝑏 ∈ (𝐵m 1o) ↦ (𝑏𝑎)) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
109 coeq1 5787 . . . . 5 (𝑦 = 𝑎 → (𝑦 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) = (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))))
110109eleq1d 2822 . . . 4 (𝑦 = 𝑎 → ((𝑦 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ↔ (𝑎 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
111 coeq1 5787 . . . . 5 (𝑦 = 𝑏 → (𝑦 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) = (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))))
112111eleq1d 2822 . . . 4 (𝑦 = 𝑏 → ((𝑦 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ↔ (𝑏 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
113 coeq1 5787 . . . . 5 (𝑦 = (𝑎f + 𝑏) → (𝑦 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) = ((𝑎f + 𝑏) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))))
114113eleq1d 2822 . . . 4 (𝑦 = (𝑎f + 𝑏) → ((𝑦 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ↔ ((𝑎f + 𝑏) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
115 coeq1 5787 . . . . 5 (𝑦 = (𝑎f · 𝑏) → (𝑦 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) = ((𝑎f · 𝑏) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))))
116115eleq1d 2822 . . . 4 (𝑦 = (𝑎f · 𝑏) → ((𝑦 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ↔ ((𝑎f · 𝑏) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
117 coeq1 5787 . . . . 5 (𝑦 = (𝐴 ∘ (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅))) → (𝑦 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) = ((𝐴 ∘ (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅))) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))))
118117eleq1d 2822 . . . 4 (𝑦 = (𝐴 ∘ (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅))) → ((𝑦 ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ↔ ((𝐴 ∘ (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅))) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
11916pf1rcl 21598 . . . . . . . . 9 (𝐴𝑄𝑅 ∈ CRing)
12015, 119syl 17 . . . . . . . 8 (𝜑𝑅 ∈ CRing)
121120adantr 481 . . . . . . 7 ((𝜑𝑎𝐵) → 𝑅 ∈ CRing)
122 1on 8358 . . . . . . . . . . . 12 1o ∈ On
123 eqid 2737 . . . . . . . . . . . . 13 (1o mPoly 𝑅) = (1o mPoly 𝑅)
124123mplassa 21310 . . . . . . . . . . . 12 ((1o ∈ On ∧ 𝑅 ∈ CRing) → (1o mPoly 𝑅) ∈ AssAlg)
125122, 120, 124sylancr 587 . . . . . . . . . . 11 (𝜑 → (1o mPoly 𝑅) ∈ AssAlg)
126 eqid 2737 . . . . . . . . . . . . 13 (Poly1𝑅) = (Poly1𝑅)
127 eqid 2737 . . . . . . . . . . . . 13 (algSc‘(Poly1𝑅)) = (algSc‘(Poly1𝑅))
128126, 127ply1ascl 21512 . . . . . . . . . . . 12 (algSc‘(Poly1𝑅)) = (algSc‘(1o mPoly 𝑅))
129 eqid 2737 . . . . . . . . . . . 12 (Scalar‘(1o mPoly 𝑅)) = (Scalar‘(1o mPoly 𝑅))
130128, 129asclrhm 21177 . . . . . . . . . . 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 21300 . . . . . . . . . . 11 (𝜑𝑅 = (Scalar‘(1o mPoly 𝑅)))
134133oveq1d 7332 . . . . . . . . . 10 (𝜑 → (𝑅 RingHom (1o mPoly 𝑅)) = ((Scalar‘(1o mPoly 𝑅)) RingHom (1o mPoly 𝑅)))
135131, 134eleqtrrd 2841 . . . . . . . . 9 (𝜑 → (algSc‘(Poly1𝑅)) ∈ (𝑅 RingHom (1o mPoly 𝑅)))
136 eqid 2737 . . . . . . . . . 10 (Base‘(1o mPoly 𝑅)) = (Base‘(1o mPoly 𝑅))
1373, 136rhmf 20045 . . . . . . . . 9 ((algSc‘(Poly1𝑅)) ∈ (𝑅 RingHom (1o mPoly 𝑅)) → (algSc‘(Poly1𝑅)):𝐵⟶(Base‘(1o mPoly 𝑅)))
138135, 137syl 17 . . . . . . . 8 (𝜑 → (algSc‘(Poly1𝑅)):𝐵⟶(Base‘(1o mPoly 𝑅)))
139138ffvelcdmda 7001 . . . . . . 7 ((𝜑𝑎𝐵) → ((algSc‘(Poly1𝑅))‘𝑎) ∈ (Base‘(1o mPoly 𝑅)))
140 eqid 2737 . . . . . . . 8 (eval1𝑅) = (eval1𝑅)
141140, 23, 3, 123, 136evl1val 21578 . . . . . . 7 ((𝑅 ∈ CRing ∧ ((algSc‘(Poly1𝑅))‘𝑎) ∈ (Base‘(1o mPoly 𝑅))) → ((eval1𝑅)‘((algSc‘(Poly1𝑅))‘𝑎)) = (((1o eval 𝑅)‘((algSc‘(Poly1𝑅))‘𝑎)) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))))
142121, 139, 141syl2anc 584 . . . . . 6 ((𝜑𝑎𝐵) → ((eval1𝑅)‘((algSc‘(Poly1𝑅))‘𝑎)) = (((1o eval 𝑅)‘((algSc‘(Poly1𝑅))‘𝑎)) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))))
143140, 126, 3, 127evl1sca 21583 . . . . . . 7 ((𝑅 ∈ CRing ∧ 𝑎𝐵) → ((eval1𝑅)‘((algSc‘(Poly1𝑅))‘𝑎)) = (𝐵 × {𝑎}))
144120, 143sylan 580 . . . . . 6 ((𝜑𝑎𝐵) → ((eval1𝑅)‘((algSc‘(Poly1𝑅))‘𝑎)) = (𝐵 × {𝑎}))
1453ressid 17031 . . . . . . . . . . . . . 14 (𝑅 ∈ CRing → (𝑅s 𝐵) = 𝑅)
146121, 145syl 17 . . . . . . . . . . . . 13 ((𝜑𝑎𝐵) → (𝑅s 𝐵) = 𝑅)
147146oveq2d 7333 . . . . . . . . . . . 12 ((𝜑𝑎𝐵) → (1o mPoly (𝑅s 𝐵)) = (1o mPoly 𝑅))
148147fveq2d 6816 . . . . . . . . . . 11 ((𝜑𝑎𝐵) → (algSc‘(1o mPoly (𝑅s 𝐵))) = (algSc‘(1o mPoly 𝑅)))
149148, 128eqtr4di 2795 . . . . . . . . . 10 ((𝜑𝑎𝐵) → (algSc‘(1o mPoly (𝑅s 𝐵))) = (algSc‘(Poly1𝑅)))
150149fveq1d 6814 . . . . . . . . 9 ((𝜑𝑎𝐵) → ((algSc‘(1o mPoly (𝑅s 𝐵)))‘𝑎) = ((algSc‘(Poly1𝑅))‘𝑎))
151150fveq2d 6816 . . . . . . . 8 ((𝜑𝑎𝐵) → ((1o eval 𝑅)‘((algSc‘(1o mPoly (𝑅s 𝐵)))‘𝑎)) = ((1o eval 𝑅)‘((algSc‘(Poly1𝑅))‘𝑎)))
152 eqid 2737 . . . . . . . . 9 (1o mPoly (𝑅s 𝐵)) = (1o mPoly (𝑅s 𝐵))
153 eqid 2737 . . . . . . . . 9 (𝑅s 𝐵) = (𝑅s 𝐵)
154 eqid 2737 . . . . . . . . 9 (algSc‘(1o mPoly (𝑅s 𝐵))) = (algSc‘(1o mPoly (𝑅s 𝐵)))
155122a1i 11 . . . . . . . . 9 ((𝜑𝑎𝐵) → 1o ∈ On)
156 crngring 19870 . . . . . . . . . . 11 (𝑅 ∈ CRing → 𝑅 ∈ Ring)
1573subrgid 20108 . . . . . . . . . . 11 (𝑅 ∈ Ring → 𝐵 ∈ (SubRing‘𝑅))
158120, 156, 1573syl 18 . . . . . . . . . 10 (𝜑𝐵 ∈ (SubRing‘𝑅))
159158adantr 481 . . . . . . . . 9 ((𝜑𝑎𝐵) → 𝐵 ∈ (SubRing‘𝑅))
160 simpr 485 . . . . . . . . 9 ((𝜑𝑎𝐵) → 𝑎𝐵)
16124, 152, 153, 3, 154, 155, 121, 159, 160evlssca 21382 . . . . . . . 8 ((𝜑𝑎𝐵) → ((1o eval 𝑅)‘((algSc‘(1o mPoly (𝑅s 𝐵)))‘𝑎)) = ((𝐵m 1o) × {𝑎}))
162151, 161eqtr3d 2779 . . . . . . 7 ((𝜑𝑎𝐵) → ((1o eval 𝑅)‘((algSc‘(Poly1𝑅))‘𝑎)) = ((𝐵m 1o) × {𝑎}))
163162coeq1d 5791 . . . . . 6 ((𝜑𝑎𝐵) → (((1o eval 𝑅)‘((algSc‘(Poly1𝑅))‘𝑎)) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) = (((𝐵m 1o) × {𝑎}) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))))
164142, 144, 1633eqtr3d 2785 . . . . 5 ((𝜑𝑎𝐵) → (𝐵 × {𝑎}) = (((𝐵m 1o) × {𝑎}) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))))
165 pf1ind.co . . . . . . . 8 ((𝜑𝑓𝐵) → 𝜒)
166 snex 5369 . . . . . . . . . 10 {𝑓} ∈ V
1674, 166xpex 7645 . . . . . . . . 9 (𝐵 × {𝑓}) ∈ V
168 pf1ind.wa . . . . . . . . 9 (𝑥 = (𝐵 × {𝑓}) → (𝜓𝜒))
169167, 168elab 3619 . . . . . . . 8 ((𝐵 × {𝑓}) ∈ {𝑥𝜓} ↔ 𝜒)
170165, 169sylibr 233 . . . . . . 7 ((𝜑𝑓𝐵) → (𝐵 × {𝑓}) ∈ {𝑥𝜓})
171170ralrimiva 3140 . . . . . 6 (𝜑 → ∀𝑓𝐵 (𝐵 × {𝑓}) ∈ {𝑥𝜓})
172 sneq 4581 . . . . . . . . 9 (𝑓 = 𝑎 → {𝑓} = {𝑎})
173172xpeq2d 5638 . . . . . . . 8 (𝑓 = 𝑎 → (𝐵 × {𝑓}) = (𝐵 × {𝑎}))
174173eleq1d 2822 . . . . . . 7 (𝑓 = 𝑎 → ((𝐵 × {𝑓}) ∈ {𝑥𝜓} ↔ (𝐵 × {𝑎}) ∈ {𝑥𝜓}))
175174rspccva 3569 . . . . . 6 ((∀𝑓𝐵 (𝐵 × {𝑓}) ∈ {𝑥𝜓} ∧ 𝑎𝐵) → (𝐵 × {𝑎}) ∈ {𝑥𝜓})
176171, 175sylan 580 . . . . 5 ((𝜑𝑎𝐵) → (𝐵 × {𝑎}) ∈ {𝑥𝜓})
177164, 176eqeltrrd 2839 . . . 4 ((𝜑𝑎𝐵) → (((𝐵m 1o) × {𝑎}) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓})
178 pf1ind.pr . . . . . . . 8 (𝜑𝜃)
179 resiexg 7808 . . . . . . . . . 10 (𝐵 ∈ V → ( I ↾ 𝐵) ∈ V)
1804, 179ax-mp 5 . . . . . . . . 9 ( I ↾ 𝐵) ∈ V
181 pf1ind.wb . . . . . . . . 9 (𝑥 = ( I ↾ 𝐵) → (𝜓𝜃))
182180, 181elab 3619 . . . . . . . 8 (( I ↾ 𝐵) ∈ {𝑥𝜓} ↔ 𝜃)
183178, 182sylibr 233 . . . . . . 7 (𝜑 → ( I ↾ 𝐵) ∈ {𝑥𝜓})
18412, 183eqeltrd 2838 . . . . . 6 (𝜑 → ((𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅)) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓})
185 el1o 8375 . . . . . . . . . 10 (𝑎 ∈ 1o𝑎 = ∅)
186 fveq2 6812 . . . . . . . . . 10 (𝑎 = ∅ → (𝑏𝑎) = (𝑏‘∅))
187185, 186sylbi 216 . . . . . . . . 9 (𝑎 ∈ 1o → (𝑏𝑎) = (𝑏‘∅))
188187mpteq2dv 5189 . . . . . . . 8 (𝑎 ∈ 1o → (𝑏 ∈ (𝐵m 1o) ↦ (𝑏𝑎)) = (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅)))
189188coeq1d 5791 . . . . . . 7 (𝑎 ∈ 1o → ((𝑏 ∈ (𝐵m 1o) ↦ (𝑏𝑎)) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) = ((𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅)) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))))
190189eleq1d 2822 . . . . . 6 (𝑎 ∈ 1o → (((𝑏 ∈ (𝐵m 1o) ↦ (𝑏𝑎)) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓} ↔ ((𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅)) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
191184, 190syl5ibrcom 246 . . . . 5 (𝜑 → (𝑎 ∈ 1o → ((𝑏 ∈ (𝐵m 1o) ↦ (𝑏𝑎)) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓}))
192191imp 407 . . . 4 ((𝜑𝑎 ∈ 1o) → ((𝑏 ∈ (𝐵m 1o) ↦ (𝑏𝑎)) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓})
19316, 3, 27pf1mpf 21601 . . . . 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 21400 . . 3 (𝜑 → ((𝐴 ∘ (𝑏 ∈ (𝐵m 1o) ↦ (𝑏‘∅))) ∘ (𝑤𝐵 ↦ (1o × {𝑤}))) ∈ {𝑥𝜓})
19620, 195eqeltrrd 2839 . 2 (𝜑𝐴 ∈ {𝑥𝜓})
197 pf1ind.wg . . . 4 (𝑥 = 𝐴 → (𝜓𝜌))
198197elabg 3617 . . 3 (𝐴𝑄 → (𝐴 ∈ {𝑥𝜓} ↔ 𝜌))
19915, 198syl 17 . 2 (𝜑 → (𝐴 ∈ {𝑥𝜓} ↔ 𝜌))
200196, 199mpbid 231 1 (𝜑𝜌)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1540  wcel 2105  {cab 2714  wral 3062  Vcvv 3441  c0 4267  {csn 4571  cmpt 5170   I cid 5506   × cxp 5606  ccnv 5607  ran crn 5609  cres 5610  ccom 5612  Oncon0 6289  wf 6462  1-1-ontowf1o 6465  cfv 6466  (class class class)co 7317  f cof 7573  1oc1o 8339  m cmap 8665  Basecbs 16989  s cress 17018  +gcplusg 17039  .rcmulr 17040  Scalarcsca 17042  Ringcrg 19858  CRingccrg 19859   RingHom crh 20031  SubRingcsubrg 20102  AssAlgcasa 21140  algSccascl 21142   mPoly cmpl 21192   evalSub ces 21363   eval cevl 21364  Poly1cpl1 21431  eval1ce1 21563
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-rep 5224  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7630  ax-cnex 11007  ax-resscn 11008  ax-1cn 11009  ax-icn 11010  ax-addcl 11011  ax-addrcl 11012  ax-mulcl 11013  ax-mulrcl 11014  ax-mulcom 11015  ax-addass 11016  ax-mulass 11017  ax-distr 11018  ax-i2m1 11019  ax-1ne0 11020  ax-1rid 11021  ax-rnegex 11022  ax-rrecex 11023  ax-cnre 11024  ax-pre-lttri 11025  ax-pre-lttrn 11026  ax-pre-ltadd 11027  ax-pre-mulgt0 11028
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-tp 4576  df-op 4578  df-uni 4851  df-int 4893  df-iun 4939  df-iin 4940  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5563  df-se 5564  df-we 5565  df-xp 5614  df-rel 5615  df-cnv 5616  df-co 5617  df-dm 5618  df-rn 5619  df-res 5620  df-ima 5621  df-pred 6225  df-ord 6292  df-on 6293  df-lim 6294  df-suc 6295  df-iota 6418  df-fun 6468  df-fn 6469  df-f 6470  df-f1 6471  df-fo 6472  df-f1o 6473  df-fv 6474  df-isom 6475  df-riota 7274  df-ov 7320  df-oprab 7321  df-mpo 7322  df-of 7575  df-ofr 7576  df-om 7760  df-1st 7878  df-2nd 7879  df-supp 8027  df-frecs 8146  df-wrecs 8177  df-recs 8251  df-rdg 8290  df-1o 8346  df-er 8548  df-map 8667  df-pm 8668  df-ixp 8736  df-en 8784  df-dom 8785  df-sdom 8786  df-fin 8787  df-fsupp 9206  df-sup 9278  df-oi 9346  df-card 9775  df-pnf 11091  df-mnf 11092  df-xr 11093  df-ltxr 11094  df-le 11095  df-sub 11287  df-neg 11288  df-nn 12054  df-2 12116  df-3 12117  df-4 12118  df-5 12119  df-6 12120  df-7 12121  df-8 12122  df-9 12123  df-n0 12314  df-z 12400  df-dec 12518  df-uz 12663  df-fz 13320  df-fzo 13463  df-seq 13802  df-hash 14125  df-struct 16925  df-sets 16942  df-slot 16960  df-ndx 16972  df-base 16990  df-ress 17019  df-plusg 17052  df-mulr 17053  df-sca 17055  df-vsca 17056  df-ip 17057  df-tset 17058  df-ple 17059  df-ds 17061  df-hom 17063  df-cco 17064  df-0g 17229  df-gsum 17230  df-prds 17235  df-pws 17237  df-mre 17372  df-mrc 17373  df-acs 17375  df-mgm 18403  df-sgrp 18452  df-mnd 18463  df-mhm 18507  df-submnd 18508  df-grp 18656  df-minusg 18657  df-sbg 18658  df-mulg 18777  df-subg 18828  df-ghm 18908  df-cntz 18999  df-cmn 19463  df-abl 19464  df-mgp 19796  df-ur 19813  df-srg 19817  df-ring 19860  df-cring 19861  df-rnghom 20034  df-subrg 20104  df-lmod 20208  df-lss 20277  df-lsp 20317  df-assa 21143  df-asp 21144  df-ascl 21145  df-psr 21195  df-mvr 21196  df-mpl 21197  df-opsr 21199  df-evls 21365  df-evl 21366  df-psr1 21434  df-ply1 21436  df-evl1 21565
This theorem is referenced by:  pl1cn  32045
  Copyright terms: Public domain W3C validator