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

Theorem mpfind 22114
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, 19-Mar-2015.)
Hypotheses
Ref Expression
mpfind.cb 𝐵 = (Base‘𝑆)
mpfind.cp + = (+g𝑆)
mpfind.ct · = (.r𝑆)
mpfind.cq 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)
mpfind.ad ((𝜑 ∧ ((𝑓𝑄𝜏) ∧ (𝑔𝑄𝜂))) → 𝜁)
mpfind.mu ((𝜑 ∧ ((𝑓𝑄𝜏) ∧ (𝑔𝑄𝜂))) → 𝜎)
mpfind.wa (𝑥 = ((𝐵m 𝐼) × {𝑓}) → (𝜓𝜒))
mpfind.wb (𝑥 = (𝑔 ∈ (𝐵m 𝐼) ↦ (𝑔𝑓)) → (𝜓𝜃))
mpfind.wc (𝑥 = 𝑓 → (𝜓𝜏))
mpfind.wd (𝑥 = 𝑔 → (𝜓𝜂))
mpfind.we (𝑥 = (𝑓f + 𝑔) → (𝜓𝜁))
mpfind.wf (𝑥 = (𝑓f · 𝑔) → (𝜓𝜎))
mpfind.wg (𝑥 = 𝐴 → (𝜓𝜌))
mpfind.co ((𝜑𝑓𝑅) → 𝜒)
mpfind.pr ((𝜑𝑓𝐼) → 𝜃)
mpfind.a (𝜑𝐴𝑄)
Assertion
Ref Expression
mpfind (𝜑𝜌)
Distinct variable groups:   𝜒,𝑥   𝜂,𝑥   𝜑,𝑓,𝑔   𝜓,𝑓,𝑔   𝜌,𝑥   𝜎,𝑥   𝜏,𝑥   𝜃,𝑥   𝜁,𝑥   𝑥,𝐴   𝐵,𝑓,𝑔,𝑥   𝑓,𝐼,𝑔,𝑥   + ,𝑓,𝑔,𝑥   𝑄,𝑓,𝑔   𝑅,𝑓,𝑔   𝑆,𝑓,𝑔   · ,𝑓,𝑔,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)   𝜒(𝑓,𝑔)   𝜃(𝑓,𝑔)   𝜏(𝑓,𝑔)   𝜂(𝑓,𝑔)   𝜁(𝑓,𝑔)   𝜎(𝑓,𝑔)   𝜌(𝑓,𝑔)   𝐴(𝑓,𝑔)   𝑄(𝑥)   𝑅(𝑥)   𝑆(𝑥)

Proof of Theorem mpfind
Dummy variables 𝑖 𝑗 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mpfind.a . . . . 5 (𝜑𝐴𝑄)
2 mpfind.cq . . . . 5 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)
31, 2eleqtrdi 2835 . . . 4 (𝜑𝐴 ∈ ran ((𝐼 evalSub 𝑆)‘𝑅))
42mpfrcl 22092 . . . . . . . 8 (𝐴𝑄 → (𝐼 ∈ V ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)))
51, 4syl 17 . . . . . . 7 (𝜑 → (𝐼 ∈ V ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)))
6 eqid 2725 . . . . . . . 8 ((𝐼 evalSub 𝑆)‘𝑅) = ((𝐼 evalSub 𝑆)‘𝑅)
7 eqid 2725 . . . . . . . 8 (𝐼 mPoly (𝑆s 𝑅)) = (𝐼 mPoly (𝑆s 𝑅))
8 eqid 2725 . . . . . . . 8 (𝑆s 𝑅) = (𝑆s 𝑅)
9 eqid 2725 . . . . . . . 8 (𝑆s (𝐵m 𝐼)) = (𝑆s (𝐵m 𝐼))
10 mpfind.cb . . . . . . . 8 𝐵 = (Base‘𝑆)
116, 7, 8, 9, 10evlsrhm 22095 . . . . . . 7 ((𝐼 ∈ V ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → ((𝐼 evalSub 𝑆)‘𝑅) ∈ ((𝐼 mPoly (𝑆s 𝑅)) RingHom (𝑆s (𝐵m 𝐼))))
12 eqid 2725 . . . . . . . 8 (Base‘(𝐼 mPoly (𝑆s 𝑅))) = (Base‘(𝐼 mPoly (𝑆s 𝑅)))
13 eqid 2725 . . . . . . . 8 (Base‘(𝑆s (𝐵m 𝐼))) = (Base‘(𝑆s (𝐵m 𝐼)))
1412, 13rhmf 20462 . . . . . . 7 (((𝐼 evalSub 𝑆)‘𝑅) ∈ ((𝐼 mPoly (𝑆s 𝑅)) RingHom (𝑆s (𝐵m 𝐼))) → ((𝐼 evalSub 𝑆)‘𝑅):(Base‘(𝐼 mPoly (𝑆s 𝑅)))⟶(Base‘(𝑆s (𝐵m 𝐼))))
155, 11, 143syl 18 . . . . . 6 (𝜑 → ((𝐼 evalSub 𝑆)‘𝑅):(Base‘(𝐼 mPoly (𝑆s 𝑅)))⟶(Base‘(𝑆s (𝐵m 𝐼))))
1615ffnd 6728 . . . . 5 (𝜑 → ((𝐼 evalSub 𝑆)‘𝑅) Fn (Base‘(𝐼 mPoly (𝑆s 𝑅))))
17 fvelrnb 6962 . . . . 5 (((𝐼 evalSub 𝑆)‘𝑅) Fn (Base‘(𝐼 mPoly (𝑆s 𝑅))) → (𝐴 ∈ ran ((𝐼 evalSub 𝑆)‘𝑅) ↔ ∃𝑦 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅)))(((𝐼 evalSub 𝑆)‘𝑅)‘𝑦) = 𝐴))
1816, 17syl 17 . . . 4 (𝜑 → (𝐴 ∈ ran ((𝐼 evalSub 𝑆)‘𝑅) ↔ ∃𝑦 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅)))(((𝐼 evalSub 𝑆)‘𝑅)‘𝑦) = 𝐴))
193, 18mpbid 231 . . 3 (𝜑 → ∃𝑦 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅)))(((𝐼 evalSub 𝑆)‘𝑅)‘𝑦) = 𝐴)
2015ffund 6731 . . . . . 6 (𝜑 → Fun ((𝐼 evalSub 𝑆)‘𝑅))
21 eqid 2725 . . . . . . 7 (Base‘(𝑆s 𝑅)) = (Base‘(𝑆s 𝑅))
22 eqid 2725 . . . . . . 7 (𝐼 mVar (𝑆s 𝑅)) = (𝐼 mVar (𝑆s 𝑅))
23 eqid 2725 . . . . . . 7 (+g‘(𝐼 mPoly (𝑆s 𝑅))) = (+g‘(𝐼 mPoly (𝑆s 𝑅)))
24 eqid 2725 . . . . . . 7 (.r‘(𝐼 mPoly (𝑆s 𝑅))) = (.r‘(𝐼 mPoly (𝑆s 𝑅)))
25 eqid 2725 . . . . . . 7 (algSc‘(𝐼 mPoly (𝑆s 𝑅))) = (algSc‘(𝐼 mPoly (𝑆s 𝑅)))
265simp1d 1139 . . . . . . . . . . . 12 (𝜑𝐼 ∈ V)
275simp2d 1140 . . . . . . . . . . . . . 14 (𝜑𝑆 ∈ CRing)
285simp3d 1141 . . . . . . . . . . . . . 14 (𝜑𝑅 ∈ (SubRing‘𝑆))
298subrgcrng 20554 . . . . . . . . . . . . . 14 ((𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → (𝑆s 𝑅) ∈ CRing)
3027, 28, 29syl2anc 582 . . . . . . . . . . . . 13 (𝜑 → (𝑆s 𝑅) ∈ CRing)
31 crngring 20223 . . . . . . . . . . . . 13 ((𝑆s 𝑅) ∈ CRing → (𝑆s 𝑅) ∈ Ring)
3230, 31syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑆s 𝑅) ∈ Ring)
337, 26, 32mplringd 22024 . . . . . . . . . . 11 (𝜑 → (𝐼 mPoly (𝑆s 𝑅)) ∈ Ring)
3433adantr 479 . . . . . . . . . 10 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → (𝐼 mPoly (𝑆s 𝑅)) ∈ Ring)
35 simprl 769 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → 𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))
36 elpreima 7070 . . . . . . . . . . . . . 14 (((𝐼 evalSub 𝑆)‘𝑅) Fn (Base‘(𝐼 mPoly (𝑆s 𝑅))) → (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ↔ (𝑖 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥𝜓})))
3716, 36syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ↔ (𝑖 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥𝜓})))
3837adantr 479 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ↔ (𝑖 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥𝜓})))
3935, 38mpbid 231 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → (𝑖 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥𝜓}))
4039simpld 493 . . . . . . . . . 10 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → 𝑖 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))))
41 simprr 771 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))
42 elpreima 7070 . . . . . . . . . . . . . 14 (((𝐼 evalSub 𝑆)‘𝑅) Fn (Base‘(𝐼 mPoly (𝑆s 𝑅))) → (𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ↔ (𝑗 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥𝜓})))
4316, 42syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ↔ (𝑗 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥𝜓})))
4443adantr 479 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → (𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ↔ (𝑗 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥𝜓})))
4541, 44mpbid 231 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → (𝑗 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥𝜓}))
4645simpld 493 . . . . . . . . . 10 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → 𝑗 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))))
4712, 23ringacl 20252 . . . . . . . . . 10 (((𝐼 mPoly (𝑆s 𝑅)) ∈ Ring ∧ 𝑖 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))) ∧ 𝑗 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅)))) → (𝑖(+g‘(𝐼 mPoly (𝑆s 𝑅)))𝑗) ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))))
4834, 40, 46, 47syl3anc 1368 . . . . . . . . 9 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → (𝑖(+g‘(𝐼 mPoly (𝑆s 𝑅)))𝑗) ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))))
49 rhmghm 20461 . . . . . . . . . . . . . 14 (((𝐼 evalSub 𝑆)‘𝑅) ∈ ((𝐼 mPoly (𝑆s 𝑅)) RingHom (𝑆s (𝐵m 𝐼))) → ((𝐼 evalSub 𝑆)‘𝑅) ∈ ((𝐼 mPoly (𝑆s 𝑅)) GrpHom (𝑆s (𝐵m 𝐼))))
505, 11, 493syl 18 . . . . . . . . . . . . 13 (𝜑 → ((𝐼 evalSub 𝑆)‘𝑅) ∈ ((𝐼 mPoly (𝑆s 𝑅)) GrpHom (𝑆s (𝐵m 𝐼))))
5150adantr 479 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → ((𝐼 evalSub 𝑆)‘𝑅) ∈ ((𝐼 mPoly (𝑆s 𝑅)) GrpHom (𝑆s (𝐵m 𝐼))))
52 eqid 2725 . . . . . . . . . . . . 13 (+g‘(𝑆s (𝐵m 𝐼))) = (+g‘(𝑆s (𝐵m 𝐼)))
5312, 23, 52ghmlin 19210 . . . . . . . . . . . 12 ((((𝐼 evalSub 𝑆)‘𝑅) ∈ ((𝐼 mPoly (𝑆s 𝑅)) GrpHom (𝑆s (𝐵m 𝐼))) ∧ 𝑖 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))) ∧ 𝑗 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅)))) → (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(+g‘(𝐼 mPoly (𝑆s 𝑅)))𝑗)) = ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖)(+g‘(𝑆s (𝐵m 𝐼)))(((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)))
5451, 40, 46, 53syl3anc 1368 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(+g‘(𝐼 mPoly (𝑆s 𝑅)))𝑗)) = ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖)(+g‘(𝑆s (𝐵m 𝐼)))(((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)))
5527adantr 479 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → 𝑆 ∈ CRing)
56 ovexd 7458 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → (𝐵m 𝐼) ∈ V)
5715adantr 479 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → ((𝐼 evalSub 𝑆)‘𝑅):(Base‘(𝐼 mPoly (𝑆s 𝑅)))⟶(Base‘(𝑆s (𝐵m 𝐼))))
5857, 40ffvelcdmd 7098 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ (Base‘(𝑆s (𝐵m 𝐼))))
5957, 46ffvelcdmd 7098 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ (Base‘(𝑆s (𝐵m 𝐼))))
60 mpfind.cp . . . . . . . . . . . 12 + = (+g𝑆)
619, 13, 55, 56, 58, 59, 60, 52pwsplusgval 17500 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖)(+g‘(𝑆s (𝐵m 𝐼)))(((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) = ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘f + (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)))
6254, 61eqtrd 2765 . . . . . . . . . 10 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(+g‘(𝐼 mPoly (𝑆s 𝑅)))𝑗)) = ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘f + (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)))
63 simpl 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → 𝜑)
64 fnfvelrn 7093 . . . . . . . . . . . . . 14 ((((𝐼 evalSub 𝑆)‘𝑅) Fn (Base‘(𝐼 mPoly (𝑆s 𝑅))) ∧ 𝑖 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅)))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ ran ((𝐼 evalSub 𝑆)‘𝑅))
6516, 40, 64syl2an2r 683 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ ran ((𝐼 evalSub 𝑆)‘𝑅))
6665, 2eleqtrrdi 2836 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ 𝑄)
67 fvimacnvi 7064 . . . . . . . . . . . . 13 ((Fun ((𝐼 evalSub 𝑆)‘𝑅) ∧ 𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓})) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥𝜓})
6820, 35, 67syl2an2r 683 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥𝜓})
6966, 68jca 510 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥𝜓}))
70 fnfvelrn 7093 . . . . . . . . . . . . . 14 ((((𝐼 evalSub 𝑆)‘𝑅) Fn (Base‘(𝐼 mPoly (𝑆s 𝑅))) ∧ 𝑗 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅)))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ ran ((𝐼 evalSub 𝑆)‘𝑅))
7116, 46, 70syl2an2r 683 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ ran ((𝐼 evalSub 𝑆)‘𝑅))
7271, 2eleqtrrdi 2836 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ 𝑄)
73 fvimacnvi 7064 . . . . . . . . . . . . 13 ((Fun ((𝐼 evalSub 𝑆)‘𝑅) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓})) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥𝜓})
7420, 41, 73syl2an2r 683 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥𝜓})
7572, 74jca 510 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥𝜓}))
76 fvex 6913 . . . . . . . . . . . 12 (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ V
77 fvex 6913 . . . . . . . . . . . 12 (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ V
78 eleq1 2813 . . . . . . . . . . . . . . . 16 (𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) → (𝑓𝑄 ↔ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ 𝑄))
79 vex 3465 . . . . . . . . . . . . . . . . . 18 𝑓 ∈ V
80 mpfind.wc . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑓 → (𝜓𝜏))
8179, 80elab 3665 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ {𝑥𝜓} ↔ 𝜏)
82 eleq1 2813 . . . . . . . . . . . . . . . . 17 (𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) → (𝑓 ∈ {𝑥𝜓} ↔ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥𝜓}))
8381, 82bitr3id 284 . . . . . . . . . . . . . . . 16 (𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) → (𝜏 ↔ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥𝜓}))
8478, 83anbi12d 630 . . . . . . . . . . . . . . 15 (𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) → ((𝑓𝑄𝜏) ↔ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥𝜓})))
85 eleq1 2813 . . . . . . . . . . . . . . . 16 (𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) → (𝑔𝑄 ↔ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ 𝑄))
86 vex 3465 . . . . . . . . . . . . . . . . . 18 𝑔 ∈ V
87 mpfind.wd . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑔 → (𝜓𝜂))
8886, 87elab 3665 . . . . . . . . . . . . . . . . 17 (𝑔 ∈ {𝑥𝜓} ↔ 𝜂)
89 eleq1 2813 . . . . . . . . . . . . . . . . 17 (𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) → (𝑔 ∈ {𝑥𝜓} ↔ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥𝜓}))
9088, 89bitr3id 284 . . . . . . . . . . . . . . . 16 (𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) → (𝜂 ↔ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥𝜓}))
9185, 90anbi12d 630 . . . . . . . . . . . . . . 15 (𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) → ((𝑔𝑄𝜂) ↔ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥𝜓})))
9284, 91bi2anan9 636 . . . . . . . . . . . . . 14 ((𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∧ 𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) → (((𝑓𝑄𝜏) ∧ (𝑔𝑄𝜂)) ↔ (((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥𝜓}) ∧ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥𝜓}))))
9392anbi2d 628 . . . . . . . . . . . . 13 ((𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∧ 𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) → ((𝜑 ∧ ((𝑓𝑄𝜏) ∧ (𝑔𝑄𝜂))) ↔ (𝜑 ∧ (((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥𝜓}) ∧ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥𝜓})))))
94 ovex 7456 . . . . . . . . . . . . . . 15 (𝑓f + 𝑔) ∈ V
95 mpfind.we . . . . . . . . . . . . . . 15 (𝑥 = (𝑓f + 𝑔) → (𝜓𝜁))
9694, 95elab 3665 . . . . . . . . . . . . . 14 ((𝑓f + 𝑔) ∈ {𝑥𝜓} ↔ 𝜁)
97 oveq12 7432 . . . . . . . . . . . . . . 15 ((𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∧ 𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) → (𝑓f + 𝑔) = ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘f + (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)))
9897eleq1d 2810 . . . . . . . . . . . . . 14 ((𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∧ 𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) → ((𝑓f + 𝑔) ∈ {𝑥𝜓} ↔ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘f + (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) ∈ {𝑥𝜓}))
9996, 98bitr3id 284 . . . . . . . . . . . . 13 ((𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∧ 𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) → (𝜁 ↔ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘f + (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) ∈ {𝑥𝜓}))
10093, 99imbi12d 343 . . . . . . . . . . . 12 ((𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∧ 𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) → (((𝜑 ∧ ((𝑓𝑄𝜏) ∧ (𝑔𝑄𝜂))) → 𝜁) ↔ ((𝜑 ∧ (((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥𝜓}) ∧ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥𝜓}))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘f + (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) ∈ {𝑥𝜓})))
101 mpfind.ad . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑓𝑄𝜏) ∧ (𝑔𝑄𝜂))) → 𝜁)
10276, 77, 100, 101vtocl2 3546 . . . . . . . . . . 11 ((𝜑 ∧ (((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥𝜓}) ∧ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥𝜓}))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘f + (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) ∈ {𝑥𝜓})
10363, 69, 75, 102syl12anc 835 . . . . . . . . . 10 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘f + (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) ∈ {𝑥𝜓})
10462, 103eqeltrd 2825 . . . . . . . . 9 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(+g‘(𝐼 mPoly (𝑆s 𝑅)))𝑗)) ∈ {𝑥𝜓})
105 elpreima 7070 . . . . . . . . . . 11 (((𝐼 evalSub 𝑆)‘𝑅) Fn (Base‘(𝐼 mPoly (𝑆s 𝑅))) → ((𝑖(+g‘(𝐼 mPoly (𝑆s 𝑅)))𝑗) ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ↔ ((𝑖(+g‘(𝐼 mPoly (𝑆s 𝑅)))𝑗) ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(+g‘(𝐼 mPoly (𝑆s 𝑅)))𝑗)) ∈ {𝑥𝜓})))
10616, 105syl 17 . . . . . . . . . 10 (𝜑 → ((𝑖(+g‘(𝐼 mPoly (𝑆s 𝑅)))𝑗) ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ↔ ((𝑖(+g‘(𝐼 mPoly (𝑆s 𝑅)))𝑗) ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(+g‘(𝐼 mPoly (𝑆s 𝑅)))𝑗)) ∈ {𝑥𝜓})))
107106adantr 479 . . . . . . . . 9 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → ((𝑖(+g‘(𝐼 mPoly (𝑆s 𝑅)))𝑗) ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ↔ ((𝑖(+g‘(𝐼 mPoly (𝑆s 𝑅)))𝑗) ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(+g‘(𝐼 mPoly (𝑆s 𝑅)))𝑗)) ∈ {𝑥𝜓})))
10848, 104, 107mpbir2and 711 . . . . . . . 8 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → (𝑖(+g‘(𝐼 mPoly (𝑆s 𝑅)))𝑗) ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))
109108adantlr 713 . . . . . . 7 (((𝜑𝑦 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅)))) ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → (𝑖(+g‘(𝐼 mPoly (𝑆s 𝑅)))𝑗) ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))
11012, 24ringcl 20228 . . . . . . . . . 10 (((𝐼 mPoly (𝑆s 𝑅)) ∈ Ring ∧ 𝑖 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))) ∧ 𝑗 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅)))) → (𝑖(.r‘(𝐼 mPoly (𝑆s 𝑅)))𝑗) ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))))
11134, 40, 46, 110syl3anc 1368 . . . . . . . . 9 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → (𝑖(.r‘(𝐼 mPoly (𝑆s 𝑅)))𝑗) ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))))
112 eqid 2725 . . . . . . . . . . . . . . 15 (mulGrp‘(𝐼 mPoly (𝑆s 𝑅))) = (mulGrp‘(𝐼 mPoly (𝑆s 𝑅)))
113 eqid 2725 . . . . . . . . . . . . . . 15 (mulGrp‘(𝑆s (𝐵m 𝐼))) = (mulGrp‘(𝑆s (𝐵m 𝐼)))
114112, 113rhmmhm 20456 . . . . . . . . . . . . . 14 (((𝐼 evalSub 𝑆)‘𝑅) ∈ ((𝐼 mPoly (𝑆s 𝑅)) RingHom (𝑆s (𝐵m 𝐼))) → ((𝐼 evalSub 𝑆)‘𝑅) ∈ ((mulGrp‘(𝐼 mPoly (𝑆s 𝑅))) MndHom (mulGrp‘(𝑆s (𝐵m 𝐼)))))
1155, 11, 1143syl 18 . . . . . . . . . . . . 13 (𝜑 → ((𝐼 evalSub 𝑆)‘𝑅) ∈ ((mulGrp‘(𝐼 mPoly (𝑆s 𝑅))) MndHom (mulGrp‘(𝑆s (𝐵m 𝐼)))))
116115adantr 479 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → ((𝐼 evalSub 𝑆)‘𝑅) ∈ ((mulGrp‘(𝐼 mPoly (𝑆s 𝑅))) MndHom (mulGrp‘(𝑆s (𝐵m 𝐼)))))
117112, 12mgpbas 20118 . . . . . . . . . . . . 13 (Base‘(𝐼 mPoly (𝑆s 𝑅))) = (Base‘(mulGrp‘(𝐼 mPoly (𝑆s 𝑅))))
118112, 24mgpplusg 20116 . . . . . . . . . . . . 13 (.r‘(𝐼 mPoly (𝑆s 𝑅))) = (+g‘(mulGrp‘(𝐼 mPoly (𝑆s 𝑅))))
119 eqid 2725 . . . . . . . . . . . . . 14 (.r‘(𝑆s (𝐵m 𝐼))) = (.r‘(𝑆s (𝐵m 𝐼)))
120113, 119mgpplusg 20116 . . . . . . . . . . . . 13 (.r‘(𝑆s (𝐵m 𝐼))) = (+g‘(mulGrp‘(𝑆s (𝐵m 𝐼))))
121117, 118, 120mhmlin 18778 . . . . . . . . . . . 12 ((((𝐼 evalSub 𝑆)‘𝑅) ∈ ((mulGrp‘(𝐼 mPoly (𝑆s 𝑅))) MndHom (mulGrp‘(𝑆s (𝐵m 𝐼)))) ∧ 𝑖 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))) ∧ 𝑗 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅)))) → (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(.r‘(𝐼 mPoly (𝑆s 𝑅)))𝑗)) = ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖)(.r‘(𝑆s (𝐵m 𝐼)))(((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)))
122116, 40, 46, 121syl3anc 1368 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(.r‘(𝐼 mPoly (𝑆s 𝑅)))𝑗)) = ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖)(.r‘(𝑆s (𝐵m 𝐼)))(((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)))
123 mpfind.ct . . . . . . . . . . . 12 · = (.r𝑆)
1249, 13, 55, 56, 58, 59, 123, 119pwsmulrval 17501 . . . . . . . . . . 11 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖)(.r‘(𝑆s (𝐵m 𝐼)))(((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) = ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘f · (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)))
125122, 124eqtrd 2765 . . . . . . . . . 10 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(.r‘(𝐼 mPoly (𝑆s 𝑅)))𝑗)) = ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘f · (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)))
126 ovex 7456 . . . . . . . . . . . . . . 15 (𝑓f · 𝑔) ∈ V
127 mpfind.wf . . . . . . . . . . . . . . 15 (𝑥 = (𝑓f · 𝑔) → (𝜓𝜎))
128126, 127elab 3665 . . . . . . . . . . . . . 14 ((𝑓f · 𝑔) ∈ {𝑥𝜓} ↔ 𝜎)
129 oveq12 7432 . . . . . . . . . . . . . . 15 ((𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∧ 𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) → (𝑓f · 𝑔) = ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘f · (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)))
130129eleq1d 2810 . . . . . . . . . . . . . 14 ((𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∧ 𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) → ((𝑓f · 𝑔) ∈ {𝑥𝜓} ↔ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘f · (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) ∈ {𝑥𝜓}))
131128, 130bitr3id 284 . . . . . . . . . . . . 13 ((𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∧ 𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) → (𝜎 ↔ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘f · (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) ∈ {𝑥𝜓}))
13293, 131imbi12d 343 . . . . . . . . . . . 12 ((𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∧ 𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) → (((𝜑 ∧ ((𝑓𝑄𝜏) ∧ (𝑔𝑄𝜂))) → 𝜎) ↔ ((𝜑 ∧ (((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥𝜓}) ∧ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥𝜓}))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘f · (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) ∈ {𝑥𝜓})))
133 mpfind.mu . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑓𝑄𝜏) ∧ (𝑔𝑄𝜂))) → 𝜎)
13476, 77, 132, 133vtocl2 3546 . . . . . . . . . . 11 ((𝜑 ∧ (((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥𝜓}) ∧ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥𝜓}))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘f · (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) ∈ {𝑥𝜓})
13563, 69, 75, 134syl12anc 835 . . . . . . . . . 10 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘f · (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) ∈ {𝑥𝜓})
136125, 135eqeltrd 2825 . . . . . . . . 9 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(.r‘(𝐼 mPoly (𝑆s 𝑅)))𝑗)) ∈ {𝑥𝜓})
137 elpreima 7070 . . . . . . . . . . 11 (((𝐼 evalSub 𝑆)‘𝑅) Fn (Base‘(𝐼 mPoly (𝑆s 𝑅))) → ((𝑖(.r‘(𝐼 mPoly (𝑆s 𝑅)))𝑗) ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ↔ ((𝑖(.r‘(𝐼 mPoly (𝑆s 𝑅)))𝑗) ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(.r‘(𝐼 mPoly (𝑆s 𝑅)))𝑗)) ∈ {𝑥𝜓})))
13816, 137syl 17 . . . . . . . . . 10 (𝜑 → ((𝑖(.r‘(𝐼 mPoly (𝑆s 𝑅)))𝑗) ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ↔ ((𝑖(.r‘(𝐼 mPoly (𝑆s 𝑅)))𝑗) ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(.r‘(𝐼 mPoly (𝑆s 𝑅)))𝑗)) ∈ {𝑥𝜓})))
139138adantr 479 . . . . . . . . 9 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → ((𝑖(.r‘(𝐼 mPoly (𝑆s 𝑅)))𝑗) ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ↔ ((𝑖(.r‘(𝐼 mPoly (𝑆s 𝑅)))𝑗) ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(.r‘(𝐼 mPoly (𝑆s 𝑅)))𝑗)) ∈ {𝑥𝜓})))
140111, 136, 139mpbir2and 711 . . . . . . . 8 ((𝜑 ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → (𝑖(.r‘(𝐼 mPoly (𝑆s 𝑅)))𝑗) ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))
141140adantlr 713 . . . . . . 7 (((𝜑𝑦 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅)))) ∧ (𝑖 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ∧ 𝑗 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))) → (𝑖(.r‘(𝐼 mPoly (𝑆s 𝑅)))𝑗) ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))
1427mplassa 22023 . . . . . . . . . . . . 13 ((𝐼 ∈ V ∧ (𝑆s 𝑅) ∈ CRing) → (𝐼 mPoly (𝑆s 𝑅)) ∈ AssAlg)
14326, 30, 142syl2anc 582 . . . . . . . . . . . 12 (𝜑 → (𝐼 mPoly (𝑆s 𝑅)) ∈ AssAlg)
144 eqid 2725 . . . . . . . . . . . . 13 (Scalar‘(𝐼 mPoly (𝑆s 𝑅))) = (Scalar‘(𝐼 mPoly (𝑆s 𝑅)))
14525, 144asclrhm 21879 . . . . . . . . . . . 12 ((𝐼 mPoly (𝑆s 𝑅)) ∈ AssAlg → (algSc‘(𝐼 mPoly (𝑆s 𝑅))) ∈ ((Scalar‘(𝐼 mPoly (𝑆s 𝑅))) RingHom (𝐼 mPoly (𝑆s 𝑅))))
146 eqid 2725 . . . . . . . . . . . . 13 (Base‘(Scalar‘(𝐼 mPoly (𝑆s 𝑅)))) = (Base‘(Scalar‘(𝐼 mPoly (𝑆s 𝑅))))
147146, 12rhmf 20462 . . . . . . . . . . . 12 ((algSc‘(𝐼 mPoly (𝑆s 𝑅))) ∈ ((Scalar‘(𝐼 mPoly (𝑆s 𝑅))) RingHom (𝐼 mPoly (𝑆s 𝑅))) → (algSc‘(𝐼 mPoly (𝑆s 𝑅))):(Base‘(Scalar‘(𝐼 mPoly (𝑆s 𝑅))))⟶(Base‘(𝐼 mPoly (𝑆s 𝑅))))
148143, 145, 1473syl 18 . . . . . . . . . . 11 (𝜑 → (algSc‘(𝐼 mPoly (𝑆s 𝑅))):(Base‘(Scalar‘(𝐼 mPoly (𝑆s 𝑅))))⟶(Base‘(𝐼 mPoly (𝑆s 𝑅))))
149148adantr 479 . . . . . . . . . 10 ((𝜑𝑖 ∈ (Base‘(𝑆s 𝑅))) → (algSc‘(𝐼 mPoly (𝑆s 𝑅))):(Base‘(Scalar‘(𝐼 mPoly (𝑆s 𝑅))))⟶(Base‘(𝐼 mPoly (𝑆s 𝑅))))
1507, 26, 30mplsca 22014 . . . . . . . . . . . . 13 (𝜑 → (𝑆s 𝑅) = (Scalar‘(𝐼 mPoly (𝑆s 𝑅))))
151150fveq2d 6904 . . . . . . . . . . . 12 (𝜑 → (Base‘(𝑆s 𝑅)) = (Base‘(Scalar‘(𝐼 mPoly (𝑆s 𝑅)))))
152151eleq2d 2811 . . . . . . . . . . 11 (𝜑 → (𝑖 ∈ (Base‘(𝑆s 𝑅)) ↔ 𝑖 ∈ (Base‘(Scalar‘(𝐼 mPoly (𝑆s 𝑅))))))
153152biimpa 475 . . . . . . . . . 10 ((𝜑𝑖 ∈ (Base‘(𝑆s 𝑅))) → 𝑖 ∈ (Base‘(Scalar‘(𝐼 mPoly (𝑆s 𝑅)))))
154149, 153ffvelcdmd 7098 . . . . . . . . 9 ((𝜑𝑖 ∈ (Base‘(𝑆s 𝑅))) → ((algSc‘(𝐼 mPoly (𝑆s 𝑅)))‘𝑖) ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))))
15526adantr 479 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (Base‘(𝑆s 𝑅))) → 𝐼 ∈ V)
15627adantr 479 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (Base‘(𝑆s 𝑅))) → 𝑆 ∈ CRing)
15728adantr 479 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (Base‘(𝑆s 𝑅))) → 𝑅 ∈ (SubRing‘𝑆))
15810subrgss 20551 . . . . . . . . . . . . . 14 (𝑅 ∈ (SubRing‘𝑆) → 𝑅𝐵)
1598, 10ressbas2 17246 . . . . . . . . . . . . . 14 (𝑅𝐵𝑅 = (Base‘(𝑆s 𝑅)))
16028, 158, 1593syl 18 . . . . . . . . . . . . 13 (𝜑𝑅 = (Base‘(𝑆s 𝑅)))
161160eleq2d 2811 . . . . . . . . . . . 12 (𝜑 → (𝑖𝑅𝑖 ∈ (Base‘(𝑆s 𝑅))))
162161biimpar 476 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (Base‘(𝑆s 𝑅))) → 𝑖𝑅)
1636, 7, 8, 10, 25, 155, 156, 157, 162evlssca 22096 . . . . . . . . . 10 ((𝜑𝑖 ∈ (Base‘(𝑆s 𝑅))) → (((𝐼 evalSub 𝑆)‘𝑅)‘((algSc‘(𝐼 mPoly (𝑆s 𝑅)))‘𝑖)) = ((𝐵m 𝐼) × {𝑖}))
164 mpfind.co . . . . . . . . . . . . . 14 ((𝜑𝑓𝑅) → 𝜒)
165164ralrimiva 3135 . . . . . . . . . . . . 13 (𝜑 → ∀𝑓𝑅 𝜒)
166 ovex 7456 . . . . . . . . . . . . . . . . 17 (𝐵m 𝐼) ∈ V
167 vsnex 5434 . . . . . . . . . . . . . . . . 17 {𝑓} ∈ V
168166, 167xpex 7760 . . . . . . . . . . . . . . . 16 ((𝐵m 𝐼) × {𝑓}) ∈ V
169 mpfind.wa . . . . . . . . . . . . . . . 16 (𝑥 = ((𝐵m 𝐼) × {𝑓}) → (𝜓𝜒))
170168, 169elab 3665 . . . . . . . . . . . . . . 15 (((𝐵m 𝐼) × {𝑓}) ∈ {𝑥𝜓} ↔ 𝜒)
171 sneq 4642 . . . . . . . . . . . . . . . . 17 (𝑓 = 𝑖 → {𝑓} = {𝑖})
172171xpeq2d 5711 . . . . . . . . . . . . . . . 16 (𝑓 = 𝑖 → ((𝐵m 𝐼) × {𝑓}) = ((𝐵m 𝐼) × {𝑖}))
173172eleq1d 2810 . . . . . . . . . . . . . . 15 (𝑓 = 𝑖 → (((𝐵m 𝐼) × {𝑓}) ∈ {𝑥𝜓} ↔ ((𝐵m 𝐼) × {𝑖}) ∈ {𝑥𝜓}))
174170, 173bitr3id 284 . . . . . . . . . . . . . 14 (𝑓 = 𝑖 → (𝜒 ↔ ((𝐵m 𝐼) × {𝑖}) ∈ {𝑥𝜓}))
175174cbvralvw 3224 . . . . . . . . . . . . 13 (∀𝑓𝑅 𝜒 ↔ ∀𝑖𝑅 ((𝐵m 𝐼) × {𝑖}) ∈ {𝑥𝜓})
176165, 175sylib 217 . . . . . . . . . . . 12 (𝜑 → ∀𝑖𝑅 ((𝐵m 𝐼) × {𝑖}) ∈ {𝑥𝜓})
177176r19.21bi 3238 . . . . . . . . . . 11 ((𝜑𝑖𝑅) → ((𝐵m 𝐼) × {𝑖}) ∈ {𝑥𝜓})
178162, 177syldan 589 . . . . . . . . . 10 ((𝜑𝑖 ∈ (Base‘(𝑆s 𝑅))) → ((𝐵m 𝐼) × {𝑖}) ∈ {𝑥𝜓})
179163, 178eqeltrd 2825 . . . . . . . . 9 ((𝜑𝑖 ∈ (Base‘(𝑆s 𝑅))) → (((𝐼 evalSub 𝑆)‘𝑅)‘((algSc‘(𝐼 mPoly (𝑆s 𝑅)))‘𝑖)) ∈ {𝑥𝜓})
180 elpreima 7070 . . . . . . . . . . 11 (((𝐼 evalSub 𝑆)‘𝑅) Fn (Base‘(𝐼 mPoly (𝑆s 𝑅))) → (((algSc‘(𝐼 mPoly (𝑆s 𝑅)))‘𝑖) ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ↔ (((algSc‘(𝐼 mPoly (𝑆s 𝑅)))‘𝑖) ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘((algSc‘(𝐼 mPoly (𝑆s 𝑅)))‘𝑖)) ∈ {𝑥𝜓})))
18116, 180syl 17 . . . . . . . . . 10 (𝜑 → (((algSc‘(𝐼 mPoly (𝑆s 𝑅)))‘𝑖) ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ↔ (((algSc‘(𝐼 mPoly (𝑆s 𝑅)))‘𝑖) ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘((algSc‘(𝐼 mPoly (𝑆s 𝑅)))‘𝑖)) ∈ {𝑥𝜓})))
182181adantr 479 . . . . . . . . 9 ((𝜑𝑖 ∈ (Base‘(𝑆s 𝑅))) → (((algSc‘(𝐼 mPoly (𝑆s 𝑅)))‘𝑖) ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ↔ (((algSc‘(𝐼 mPoly (𝑆s 𝑅)))‘𝑖) ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘((algSc‘(𝐼 mPoly (𝑆s 𝑅)))‘𝑖)) ∈ {𝑥𝜓})))
183154, 179, 182mpbir2and 711 . . . . . . . 8 ((𝜑𝑖 ∈ (Base‘(𝑆s 𝑅))) → ((algSc‘(𝐼 mPoly (𝑆s 𝑅)))‘𝑖) ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))
184183adantlr 713 . . . . . . 7 (((𝜑𝑦 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅)))) ∧ 𝑖 ∈ (Base‘(𝑆s 𝑅))) → ((algSc‘(𝐼 mPoly (𝑆s 𝑅)))‘𝑖) ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))
18526adantr 479 . . . . . . . . . 10 ((𝜑𝑖𝐼) → 𝐼 ∈ V)
18632adantr 479 . . . . . . . . . 10 ((𝜑𝑖𝐼) → (𝑆s 𝑅) ∈ Ring)
187 simpr 483 . . . . . . . . . 10 ((𝜑𝑖𝐼) → 𝑖𝐼)
1887, 22, 12, 185, 186, 187mvrcl 21993 . . . . . . . . 9 ((𝜑𝑖𝐼) → ((𝐼 mVar (𝑆s 𝑅))‘𝑖) ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))))
18927adantr 479 . . . . . . . . . . 11 ((𝜑𝑖𝐼) → 𝑆 ∈ CRing)
19028adantr 479 . . . . . . . . . . 11 ((𝜑𝑖𝐼) → 𝑅 ∈ (SubRing‘𝑆))
1916, 22, 8, 10, 185, 189, 190, 187evlsvar 22097 . . . . . . . . . 10 ((𝜑𝑖𝐼) → (((𝐼 evalSub 𝑆)‘𝑅)‘((𝐼 mVar (𝑆s 𝑅))‘𝑖)) = (𝑔 ∈ (𝐵m 𝐼) ↦ (𝑔𝑖)))
192 mpfind.pr . . . . . . . . . . . . . 14 ((𝜑𝑓𝐼) → 𝜃)
193166mptex 7239 . . . . . . . . . . . . . . 15 (𝑔 ∈ (𝐵m 𝐼) ↦ (𝑔𝑓)) ∈ V
194 mpfind.wb . . . . . . . . . . . . . . 15 (𝑥 = (𝑔 ∈ (𝐵m 𝐼) ↦ (𝑔𝑓)) → (𝜓𝜃))
195193, 194elab 3665 . . . . . . . . . . . . . 14 ((𝑔 ∈ (𝐵m 𝐼) ↦ (𝑔𝑓)) ∈ {𝑥𝜓} ↔ 𝜃)
196192, 195sylibr 233 . . . . . . . . . . . . 13 ((𝜑𝑓𝐼) → (𝑔 ∈ (𝐵m 𝐼) ↦ (𝑔𝑓)) ∈ {𝑥𝜓})
197196ralrimiva 3135 . . . . . . . . . . . 12 (𝜑 → ∀𝑓𝐼 (𝑔 ∈ (𝐵m 𝐼) ↦ (𝑔𝑓)) ∈ {𝑥𝜓})
198 fveq2 6900 . . . . . . . . . . . . . . 15 (𝑓 = 𝑖 → (𝑔𝑓) = (𝑔𝑖))
199198mpteq2dv 5254 . . . . . . . . . . . . . 14 (𝑓 = 𝑖 → (𝑔 ∈ (𝐵m 𝐼) ↦ (𝑔𝑓)) = (𝑔 ∈ (𝐵m 𝐼) ↦ (𝑔𝑖)))
200199eleq1d 2810 . . . . . . . . . . . . 13 (𝑓 = 𝑖 → ((𝑔 ∈ (𝐵m 𝐼) ↦ (𝑔𝑓)) ∈ {𝑥𝜓} ↔ (𝑔 ∈ (𝐵m 𝐼) ↦ (𝑔𝑖)) ∈ {𝑥𝜓}))
201200cbvralvw 3224 . . . . . . . . . . . 12 (∀𝑓𝐼 (𝑔 ∈ (𝐵m 𝐼) ↦ (𝑔𝑓)) ∈ {𝑥𝜓} ↔ ∀𝑖𝐼 (𝑔 ∈ (𝐵m 𝐼) ↦ (𝑔𝑖)) ∈ {𝑥𝜓})
202197, 201sylib 217 . . . . . . . . . . 11 (𝜑 → ∀𝑖𝐼 (𝑔 ∈ (𝐵m 𝐼) ↦ (𝑔𝑖)) ∈ {𝑥𝜓})
203202r19.21bi 3238 . . . . . . . . . 10 ((𝜑𝑖𝐼) → (𝑔 ∈ (𝐵m 𝐼) ↦ (𝑔𝑖)) ∈ {𝑥𝜓})
204191, 203eqeltrd 2825 . . . . . . . . 9 ((𝜑𝑖𝐼) → (((𝐼 evalSub 𝑆)‘𝑅)‘((𝐼 mVar (𝑆s 𝑅))‘𝑖)) ∈ {𝑥𝜓})
205 elpreima 7070 . . . . . . . . . . 11 (((𝐼 evalSub 𝑆)‘𝑅) Fn (Base‘(𝐼 mPoly (𝑆s 𝑅))) → (((𝐼 mVar (𝑆s 𝑅))‘𝑖) ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ↔ (((𝐼 mVar (𝑆s 𝑅))‘𝑖) ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘((𝐼 mVar (𝑆s 𝑅))‘𝑖)) ∈ {𝑥𝜓})))
20616, 205syl 17 . . . . . . . . . 10 (𝜑 → (((𝐼 mVar (𝑆s 𝑅))‘𝑖) ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ↔ (((𝐼 mVar (𝑆s 𝑅))‘𝑖) ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘((𝐼 mVar (𝑆s 𝑅))‘𝑖)) ∈ {𝑥𝜓})))
207206adantr 479 . . . . . . . . 9 ((𝜑𝑖𝐼) → (((𝐼 mVar (𝑆s 𝑅))‘𝑖) ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}) ↔ (((𝐼 mVar (𝑆s 𝑅))‘𝑖) ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘((𝐼 mVar (𝑆s 𝑅))‘𝑖)) ∈ {𝑥𝜓})))
208188, 204, 207mpbir2and 711 . . . . . . . 8 ((𝜑𝑖𝐼) → ((𝐼 mVar (𝑆s 𝑅))‘𝑖) ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))
209208adantlr 713 . . . . . . 7 (((𝜑𝑦 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅)))) ∧ 𝑖𝐼) → ((𝐼 mVar (𝑆s 𝑅))‘𝑖) ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))
210 simpr 483 . . . . . . 7 ((𝜑𝑦 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅)))) → 𝑦 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅))))
21126adantr 479 . . . . . . 7 ((𝜑𝑦 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅)))) → 𝐼 ∈ V)
21230adantr 479 . . . . . . 7 ((𝜑𝑦 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅)))) → (𝑆s 𝑅) ∈ CRing)
21321, 22, 7, 23, 24, 25, 12, 109, 141, 184, 209, 210, 211, 212mplind 22075 . . . . . 6 ((𝜑𝑦 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅)))) → 𝑦 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓}))
214 fvimacnvi 7064 . . . . . 6 ((Fun ((𝐼 evalSub 𝑆)‘𝑅) ∧ 𝑦 ∈ (((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥𝜓})) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑦) ∈ {𝑥𝜓})
21520, 213, 214syl2an2r 683 . . . . 5 ((𝜑𝑦 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅)))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑦) ∈ {𝑥𝜓})
216 eleq1 2813 . . . . 5 ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑦) = 𝐴 → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑦) ∈ {𝑥𝜓} ↔ 𝐴 ∈ {𝑥𝜓}))
217215, 216syl5ibcom 244 . . . 4 ((𝜑𝑦 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅)))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑦) = 𝐴𝐴 ∈ {𝑥𝜓}))
218217rexlimdva 3144 . . 3 (𝜑 → (∃𝑦 ∈ (Base‘(𝐼 mPoly (𝑆s 𝑅)))(((𝐼 evalSub 𝑆)‘𝑅)‘𝑦) = 𝐴𝐴 ∈ {𝑥𝜓}))
21919, 218mpd 15 . 2 (𝜑𝐴 ∈ {𝑥𝜓})
220 mpfind.wg . . . 4 (𝑥 = 𝐴 → (𝜓𝜌))
221220elabg 3663 . . 3 (𝐴𝑄 → (𝐴 ∈ {𝑥𝜓} ↔ 𝜌))
2221, 221syl 17 . 2 (𝜑 → (𝐴 ∈ {𝑥𝜓} ↔ 𝜌))
223219, 222mpbid 231 1 (𝜑𝜌)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  w3a 1084   = wceq 1533  wcel 2098  {cab 2702  wral 3050  wrex 3059  Vcvv 3461  wss 3946  {csn 4632  cmpt 5235   × cxp 5679  ccnv 5680  ran crn 5682  cima 5684  Fun wfun 6547   Fn wfn 6548  wf 6549  cfv 6553  (class class class)co 7423  f cof 7687  m cmap 8854  Basecbs 17208  s cress 17237  +gcplusg 17261  .rcmulr 17262  Scalarcsca 17264  s cpws 17456   MndHom cmhm 18766   GrpHom cghm 19201  mulGrpcmgp 20112  Ringcrg 20211  CRingccrg 20212   RingHom crh 20446  SubRingcsubrg 20546  AssAlgcasa 21840  algSccascl 21842   mVar cmvr 21894   mPoly cmpl 21895   evalSub ces 22077
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5289  ax-sep 5303  ax-nul 5310  ax-pow 5368  ax-pr 5432  ax-un 7745  ax-cnex 11210  ax-resscn 11211  ax-1cn 11212  ax-icn 11213  ax-addcl 11214  ax-addrcl 11215  ax-mulcl 11216  ax-mulrcl 11217  ax-mulcom 11218  ax-addass 11219  ax-mulass 11220  ax-distr 11221  ax-i2m1 11222  ax-1ne0 11223  ax-1rid 11224  ax-rnegex 11225  ax-rrecex 11226  ax-cnre 11227  ax-pre-lttri 11228  ax-pre-lttrn 11229  ax-pre-ltadd 11230  ax-pre-mulgt0 11231
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4325  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-tp 4637  df-op 4639  df-uni 4913  df-int 4954  df-iun 5002  df-iin 5003  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5579  df-eprel 5585  df-po 5593  df-so 5594  df-fr 5636  df-se 5637  df-we 5638  df-xp 5687  df-rel 5688  df-cnv 5689  df-co 5690  df-dm 5691  df-rn 5692  df-res 5693  df-ima 5694  df-pred 6311  df-ord 6378  df-on 6379  df-lim 6380  df-suc 6381  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-isom 6562  df-riota 7379  df-ov 7426  df-oprab 7427  df-mpo 7428  df-of 7689  df-ofr 7690  df-om 7876  df-1st 8002  df-2nd 8003  df-supp 8174  df-frecs 8295  df-wrecs 8326  df-recs 8400  df-rdg 8439  df-1o 8495  df-2o 8496  df-er 8733  df-map 8856  df-pm 8857  df-ixp 8926  df-en 8974  df-dom 8975  df-sdom 8976  df-fin 8977  df-fsupp 9402  df-sup 9481  df-oi 9549  df-card 9978  df-pnf 11296  df-mnf 11297  df-xr 11298  df-ltxr 11299  df-le 11300  df-sub 11492  df-neg 11493  df-nn 12260  df-2 12322  df-3 12323  df-4 12324  df-5 12325  df-6 12326  df-7 12327  df-8 12328  df-9 12329  df-n0 12520  df-z 12606  df-dec 12725  df-uz 12870  df-fz 13534  df-fzo 13677  df-seq 14017  df-hash 14343  df-struct 17144  df-sets 17161  df-slot 17179  df-ndx 17191  df-base 17209  df-ress 17238  df-plusg 17274  df-mulr 17275  df-sca 17277  df-vsca 17278  df-ip 17279  df-tset 17280  df-ple 17281  df-ds 17283  df-hom 17285  df-cco 17286  df-0g 17451  df-gsum 17452  df-prds 17457  df-pws 17459  df-mre 17594  df-mrc 17595  df-acs 17597  df-mgm 18628  df-sgrp 18707  df-mnd 18723  df-mhm 18768  df-submnd 18769  df-grp 18926  df-minusg 18927  df-sbg 18928  df-mulg 19057  df-subg 19112  df-ghm 19202  df-cntz 19306  df-cmn 19775  df-abl 19776  df-mgp 20113  df-rng 20131  df-ur 20160  df-srg 20165  df-ring 20213  df-cring 20214  df-rhm 20449  df-subrng 20523  df-subrg 20548  df-lmod 20785  df-lss 20856  df-lsp 20896  df-assa 21843  df-asp 21844  df-ascl 21845  df-psr 21898  df-mvr 21899  df-mpl 21900  df-evls 22079
This theorem is referenced by:  pf1ind  22338  mzpmfp  42353
  Copyright terms: Public domain W3C validator