mpfind - Metamath Proof Explorer

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

Theorem mpfind 21891

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.

Step	Hyp	Ref	Expression
1		mpfind.a	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝑄)
2		mpfind.cq	. . . . 5 ⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅)
3	1, 2	eleqtrdi 2841	. . . 4 ⊢ (𝜑 → 𝐴 ∈ ran ((𝐼 evalSub 𝑆)‘𝑅))
4	2	mpfrcl 21869	. . . . . . . 8 ⊢ (𝐴 ∈ 𝑄 → (𝐼 ∈ V ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)))
5	1, 4	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝐼 ∈ V ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)))
6		eqid 2730	. . . . . . . 8 ⊢ ((𝐼 evalSub 𝑆)‘𝑅) = ((𝐼 evalSub 𝑆)‘𝑅)
7		eqid 2730	. . . . . . . 8 ⊢ (𝐼 mPoly (𝑆 ↾_s 𝑅)) = (𝐼 mPoly (𝑆 ↾_s 𝑅))
8		eqid 2730	. . . . . . . 8 ⊢ (𝑆 ↾_s 𝑅) = (𝑆 ↾_s 𝑅)
9		eqid 2730	. . . . . . . 8 ⊢ (𝑆 ↑_s (𝐵 ↑_m 𝐼)) = (𝑆 ↑_s (𝐵 ↑_m 𝐼))
10		mpfind.cb	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝑆)
11	6, 7, 8, 9, 10	evlsrhm 21872	. . . . . . 7 ⊢ ((𝐼 ∈ V ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → ((𝐼 evalSub 𝑆)‘𝑅) ∈ ((𝐼 mPoly (𝑆 ↾_s 𝑅)) RingHom (𝑆 ↑_s (𝐵 ↑_m 𝐼))))
12		eqid 2730	. . . . . . . 8 ⊢ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) = (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))
13		eqid 2730	. . . . . . . 8 ⊢ (Base‘(𝑆 ↑_s (𝐵 ↑_m 𝐼))) = (Base‘(𝑆 ↑_s (𝐵 ↑_m 𝐼)))
14	12, 13	rhmf 20378	. . . . . . 7 ⊢ (((𝐼 evalSub 𝑆)‘𝑅) ∈ ((𝐼 mPoly (𝑆 ↾_s 𝑅)) RingHom (𝑆 ↑_s (𝐵 ↑_m 𝐼))) → ((𝐼 evalSub 𝑆)‘𝑅):(Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))⟶(Base‘(𝑆 ↑_s (𝐵 ↑_m 𝐼))))
15	5, 11, 14	3syl 18	. . . . . 6 ⊢ (𝜑 → ((𝐼 evalSub 𝑆)‘𝑅):(Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))⟶(Base‘(𝑆 ↑_s (𝐵 ↑_m 𝐼))))
16	15	ffnd 6719	. . . . 5 ⊢ (𝜑 → ((𝐼 evalSub 𝑆)‘𝑅) Fn (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))))
17		fvelrnb 6953	. . . . 5 ⊢ (((𝐼 evalSub 𝑆)‘𝑅) Fn (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) → (𝐴 ∈ ran ((𝐼 evalSub 𝑆)‘𝑅) ↔ ∃𝑦 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))(((𝐼 evalSub 𝑆)‘𝑅)‘𝑦) = 𝐴))
18	16, 17	syl 17	. . . 4 ⊢ (𝜑 → (𝐴 ∈ ran ((𝐼 evalSub 𝑆)‘𝑅) ↔ ∃𝑦 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))(((𝐼 evalSub 𝑆)‘𝑅)‘𝑦) = 𝐴))
19	3, 18	mpbid 231	. . 3 ⊢ (𝜑 → ∃𝑦 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))(((𝐼 evalSub 𝑆)‘𝑅)‘𝑦) = 𝐴)
20	15	ffund 6722	. . . . . 6 ⊢ (𝜑 → Fun ((𝐼 evalSub 𝑆)‘𝑅))
21		eqid 2730	. . . . . . 7 ⊢ (Base‘(𝑆 ↾_s 𝑅)) = (Base‘(𝑆 ↾_s 𝑅))
22		eqid 2730	. . . . . . 7 ⊢ (𝐼 mVar (𝑆 ↾_s 𝑅)) = (𝐼 mVar (𝑆 ↾_s 𝑅))
23		eqid 2730	. . . . . . 7 ⊢ (+_g‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) = (+_g‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))
24		eqid 2730	. . . . . . 7 ⊢ (._r‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) = (._r‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))
25		eqid 2730	. . . . . . 7 ⊢ (algSc‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) = (algSc‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))
26	5	simp1d 1140	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐼 ∈ V)
27	5	simp2d 1141	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑆 ∈ CRing)
28	5	simp3d 1142	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆))
29	8	subrgcrng 20467	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → (𝑆 ↾_s 𝑅) ∈ CRing)
30	27, 28, 29	syl2anc 582	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆 ↾_s 𝑅) ∈ CRing)
31		crngring 20141	. . . . . . . . . . . . 13 ⊢ ((𝑆 ↾_s 𝑅) ∈ CRing → (𝑆 ↾_s 𝑅) ∈ Ring)
32	30, 31	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 ↾_s 𝑅) ∈ Ring)
33	7	mplring 21799	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ V ∧ (𝑆 ↾_s 𝑅) ∈ Ring) → (𝐼 mPoly (𝑆 ↾_s 𝑅)) ∈ Ring)
34	26, 32, 33	syl2anc 582	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐼 mPoly (𝑆 ↾_s 𝑅)) ∈ Ring)
35	34	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (𝐼 mPoly (𝑆 ↾_s 𝑅)) ∈ Ring)
36		simprl 767	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → 𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))
37		elpreima 7060	. . . . . . . . . . . . . 14 ⊢ (((𝐼 evalSub 𝑆)‘𝑅) Fn (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) → (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ (𝑖 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥 ∣ 𝜓})))
38	16, 37	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ (𝑖 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥 ∣ 𝜓})))
39	38	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ (𝑖 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥 ∣ 𝜓})))
40	36, 39	mpbid 231	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (𝑖 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥 ∣ 𝜓}))
41	40	simpld 493	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → 𝑖 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))))
42		simprr 769	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))
43		elpreima 7060	. . . . . . . . . . . . . 14 ⊢ (((𝐼 evalSub 𝑆)‘𝑅) Fn (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) → (𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ (𝑗 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥 ∣ 𝜓})))
44	16, 43	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ (𝑗 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥 ∣ 𝜓})))
45	44	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ (𝑗 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥 ∣ 𝜓})))
46	42, 45	mpbid 231	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (𝑗 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥 ∣ 𝜓}))
47	46	simpld 493	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → 𝑗 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))))
48	12, 23	ringacl 20168	. . . . . . . . . 10 ⊢ (((𝐼 mPoly (𝑆 ↾_s 𝑅)) ∈ Ring ∧ 𝑖 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) ∧ 𝑗 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))) → (𝑖(+_g‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗) ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))))
49	35, 41, 47, 48	syl3anc 1369	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (𝑖(+_g‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗) ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))))
50		rhmghm 20377	. . . . . . . . . . . . . 14 ⊢ (((𝐼 evalSub 𝑆)‘𝑅) ∈ ((𝐼 mPoly (𝑆 ↾_s 𝑅)) RingHom (𝑆 ↑_s (𝐵 ↑_m 𝐼))) → ((𝐼 evalSub 𝑆)‘𝑅) ∈ ((𝐼 mPoly (𝑆 ↾_s 𝑅)) GrpHom (𝑆 ↑_s (𝐵 ↑_m 𝐼))))
51	5, 11, 50	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐼 evalSub 𝑆)‘𝑅) ∈ ((𝐼 mPoly (𝑆 ↾_s 𝑅)) GrpHom (𝑆 ↑_s (𝐵 ↑_m 𝐼))))
52	51	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → ((𝐼 evalSub 𝑆)‘𝑅) ∈ ((𝐼 mPoly (𝑆 ↾_s 𝑅)) GrpHom (𝑆 ↑_s (𝐵 ↑_m 𝐼))))
53		eqid 2730	. . . . . . . . . . . . 13 ⊢ (+_g‘(𝑆 ↑_s (𝐵 ↑_m 𝐼))) = (+_g‘(𝑆 ↑_s (𝐵 ↑_m 𝐼)))
54	12, 23, 53	ghmlin 19137	. . . . . . . . . . . 12 ⊢ ((((𝐼 evalSub 𝑆)‘𝑅) ∈ ((𝐼 mPoly (𝑆 ↾_s 𝑅)) GrpHom (𝑆 ↑_s (𝐵 ↑_m 𝐼))) ∧ 𝑖 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) ∧ 𝑗 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))) → (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(+_g‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗)) = ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖)(+_g‘(𝑆 ↑_s (𝐵 ↑_m 𝐼)))(((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)))
55	52, 41, 47, 54	syl3anc 1369	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(+_g‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗)) = ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖)(+_g‘(𝑆 ↑_s (𝐵 ↑_m 𝐼)))(((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)))
56	27	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → 𝑆 ∈ CRing)
57		ovexd 7448	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (𝐵 ↑_m 𝐼) ∈ V)
58	15	adantr 479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → ((𝐼 evalSub 𝑆)‘𝑅):(Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))⟶(Base‘(𝑆 ↑_s (𝐵 ↑_m 𝐼))))
59	58, 41	ffvelcdmd 7088	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ (Base‘(𝑆 ↑_s (𝐵 ↑_m 𝐼))))
60	58, 47	ffvelcdmd 7088	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ (Base‘(𝑆 ↑_s (𝐵 ↑_m 𝐼))))
61		mpfind.cp	. . . . . . . . . . . 12 ⊢ + = (+_g‘𝑆)
62	9, 13, 56, 57, 59, 60, 61, 53	pwsplusgval 17442	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖)(+_g‘(𝑆 ↑_s (𝐵 ↑_m 𝐼)))(((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) = ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘_f + (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)))
63	55, 62	eqtrd 2770	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(+_g‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗)) = ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘_f + (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)))
64		simpl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → 𝜑)
65		fnfvelrn 7083	. . . . . . . . . . . . . 14 ⊢ ((((𝐼 evalSub 𝑆)‘𝑅) Fn (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) ∧ 𝑖 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ ran ((𝐼 evalSub 𝑆)‘𝑅))
66	16, 41, 65	syl2an2r 681	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ ran ((𝐼 evalSub 𝑆)‘𝑅))
67	66, 2	eleqtrrdi 2842	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ 𝑄)
68		fvimacnvi 7054	. . . . . . . . . . . . 13 ⊢ ((Fun ((𝐼 evalSub 𝑆)‘𝑅) ∧ 𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓})) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥 ∣ 𝜓})
69	20, 36, 68	syl2an2r 681	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥 ∣ 𝜓})
70	67, 69	jca 510	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥 ∣ 𝜓}))
71		fnfvelrn 7083	. . . . . . . . . . . . . 14 ⊢ ((((𝐼 evalSub 𝑆)‘𝑅) Fn (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) ∧ 𝑗 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ ran ((𝐼 evalSub 𝑆)‘𝑅))
72	16, 47, 71	syl2an2r 681	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ ran ((𝐼 evalSub 𝑆)‘𝑅))
73	72, 2	eleqtrrdi 2842	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ 𝑄)
74		fvimacnvi 7054	. . . . . . . . . . . . 13 ⊢ ((Fun ((𝐼 evalSub 𝑆)‘𝑅) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓})) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥 ∣ 𝜓})
75	20, 42, 74	syl2an2r 681	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥 ∣ 𝜓})
76	73, 75	jca 510	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥 ∣ 𝜓}))
77		fvex 6905	. . . . . . . . . . . 12 ⊢ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ V
78		fvex 6905	. . . . . . . . . . . 12 ⊢ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ V
79		eleq1 2819	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) → (𝑓 ∈ 𝑄 ↔ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ 𝑄))
80		vex 3476	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑓 ∈ V
81		mpfind.wc	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑓 → (𝜓 ↔ 𝜏))
82	80, 81	elab 3669	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ {𝑥 ∣ 𝜓} ↔ 𝜏)
83		eleq1 2819	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) → (𝑓 ∈ {𝑥 ∣ 𝜓} ↔ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥 ∣ 𝜓}))
84	82, 83	bitr3id 284	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) → (𝜏 ↔ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥 ∣ 𝜓}))
85	79, 84	anbi12d 629	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) → ((𝑓 ∈ 𝑄 ∧ 𝜏) ↔ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥 ∣ 𝜓})))
86		eleq1 2819	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) → (𝑔 ∈ 𝑄 ↔ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ 𝑄))
87		vex 3476	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑔 ∈ V
88		mpfind.wd	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = 𝑔 → (𝜓 ↔ 𝜂))
89	87, 88	elab 3669	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ∈ {𝑥 ∣ 𝜓} ↔ 𝜂)
90		eleq1 2819	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) → (𝑔 ∈ {𝑥 ∣ 𝜓} ↔ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥 ∣ 𝜓}))
91	89, 90	bitr3id 284	. . . . . . . . . . . . . . . 16 ⊢ (𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) → (𝜂 ↔ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥 ∣ 𝜓}))
92	86, 91	anbi12d 629	. . . . . . . . . . . . . . 15 ⊢ (𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) → ((𝑔 ∈ 𝑄 ∧ 𝜂) ↔ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥 ∣ 𝜓})))
93	85, 92	bi2anan9 635	. . . . . . . . . . . . . 14 ⊢ ((𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∧ 𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) → (((𝑓 ∈ 𝑄 ∧ 𝜏) ∧ (𝑔 ∈ 𝑄 ∧ 𝜂)) ↔ (((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥 ∣ 𝜓}) ∧ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥 ∣ 𝜓}))))
94	93	anbi2d 627	. . . . . . . . . . . . 13 ⊢ ((𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∧ 𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) → ((𝜑 ∧ ((𝑓 ∈ 𝑄 ∧ 𝜏) ∧ (𝑔 ∈ 𝑄 ∧ 𝜂))) ↔ (𝜑 ∧ (((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥 ∣ 𝜓}) ∧ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥 ∣ 𝜓})))))
95		ovex 7446	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∘_f + 𝑔) ∈ V
96		mpfind.we	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑓 ∘_f + 𝑔) → (𝜓 ↔ 𝜁))
97	95, 96	elab 3669	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∘_f + 𝑔) ∈ {𝑥 ∣ 𝜓} ↔ 𝜁)
98		oveq12 7422	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∧ 𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) → (𝑓 ∘_f + 𝑔) = ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘_f + (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)))
99	98	eleq1d 2816	. . . . . . . . . . . . . 14 ⊢ ((𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∧ 𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) → ((𝑓 ∘_f + 𝑔) ∈ {𝑥 ∣ 𝜓} ↔ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘_f + (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) ∈ {𝑥 ∣ 𝜓}))
100	97, 99	bitr3id 284	. . . . . . . . . . . . 13 ⊢ ((𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∧ 𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) → (𝜁 ↔ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘_f + (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) ∈ {𝑥 ∣ 𝜓}))
101	94, 100	imbi12d 343	. . . . . . . . . . . 12 ⊢ ((𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∧ 𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) → (((𝜑 ∧ ((𝑓 ∈ 𝑄 ∧ 𝜏) ∧ (𝑔 ∈ 𝑄 ∧ 𝜂))) → 𝜁) ↔ ((𝜑 ∧ (((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥 ∣ 𝜓}) ∧ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥 ∣ 𝜓}))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘_f + (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) ∈ {𝑥 ∣ 𝜓})))
102		mpfind.ad	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑄 ∧ 𝜏) ∧ (𝑔 ∈ 𝑄 ∧ 𝜂))) → 𝜁)
103	77, 78, 101, 102	vtocl2 3553	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥 ∣ 𝜓}) ∧ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥 ∣ 𝜓}))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘_f + (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) ∈ {𝑥 ∣ 𝜓})
104	64, 70, 76, 103	syl12anc 833	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘_f + (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) ∈ {𝑥 ∣ 𝜓})
105	63, 104	eqeltrd 2831	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(+_g‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗)) ∈ {𝑥 ∣ 𝜓})
106		elpreima 7060	. . . . . . . . . . 11 ⊢ (((𝐼 evalSub 𝑆)‘𝑅) Fn (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) → ((𝑖(+_g‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗) ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ ((𝑖(+_g‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗) ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(+_g‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗)) ∈ {𝑥 ∣ 𝜓})))
107	16, 106	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑖(+_g‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗) ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ ((𝑖(+_g‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗) ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(+_g‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗)) ∈ {𝑥 ∣ 𝜓})))
108	107	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → ((𝑖(+_g‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗) ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ ((𝑖(+_g‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗) ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(+_g‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗)) ∈ {𝑥 ∣ 𝜓})))
109	49, 105, 108	mpbir2and 709	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (𝑖(+_g‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗) ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))
110	109	adantlr 711	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))) ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (𝑖(+_g‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗) ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))
111	12, 24	ringcl 20146	. . . . . . . . . 10 ⊢ (((𝐼 mPoly (𝑆 ↾_s 𝑅)) ∈ Ring ∧ 𝑖 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) ∧ 𝑗 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))) → (𝑖(._r‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗) ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))))
112	35, 41, 47, 111	syl3anc 1369	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (𝑖(._r‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗) ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))))
113		eqid 2730	. . . . . . . . . . . . . . 15 ⊢ (mulGrp‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) = (mulGrp‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))
114		eqid 2730	. . . . . . . . . . . . . . 15 ⊢ (mulGrp‘(𝑆 ↑_s (𝐵 ↑_m 𝐼))) = (mulGrp‘(𝑆 ↑_s (𝐵 ↑_m 𝐼)))
115	113, 114	rhmmhm 20372	. . . . . . . . . . . . . 14 ⊢ (((𝐼 evalSub 𝑆)‘𝑅) ∈ ((𝐼 mPoly (𝑆 ↾_s 𝑅)) RingHom (𝑆 ↑_s (𝐵 ↑_m 𝐼))) → ((𝐼 evalSub 𝑆)‘𝑅) ∈ ((mulGrp‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) MndHom (mulGrp‘(𝑆 ↑_s (𝐵 ↑_m 𝐼)))))
116	5, 11, 115	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐼 evalSub 𝑆)‘𝑅) ∈ ((mulGrp‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) MndHom (mulGrp‘(𝑆 ↑_s (𝐵 ↑_m 𝐼)))))
117	116	adantr 479	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → ((𝐼 evalSub 𝑆)‘𝑅) ∈ ((mulGrp‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) MndHom (mulGrp‘(𝑆 ↑_s (𝐵 ↑_m 𝐼)))))
118	113, 12	mgpbas 20036	. . . . . . . . . . . . 13 ⊢ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) = (Base‘(mulGrp‘(𝐼 mPoly (𝑆 ↾_s 𝑅))))
119	113, 24	mgpplusg 20034	. . . . . . . . . . . . 13 ⊢ (._r‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) = (+_g‘(mulGrp‘(𝐼 mPoly (𝑆 ↾_s 𝑅))))
120		eqid 2730	. . . . . . . . . . . . . 14 ⊢ (._r‘(𝑆 ↑_s (𝐵 ↑_m 𝐼))) = (._r‘(𝑆 ↑_s (𝐵 ↑_m 𝐼)))
121	114, 120	mgpplusg 20034	. . . . . . . . . . . . 13 ⊢ (._r‘(𝑆 ↑_s (𝐵 ↑_m 𝐼))) = (+_g‘(mulGrp‘(𝑆 ↑_s (𝐵 ↑_m 𝐼))))
122	118, 119, 121	mhmlin 18717	. . . . . . . . . . . 12 ⊢ ((((𝐼 evalSub 𝑆)‘𝑅) ∈ ((mulGrp‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) MndHom (mulGrp‘(𝑆 ↑_s (𝐵 ↑_m 𝐼)))) ∧ 𝑖 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) ∧ 𝑗 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))) → (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(._r‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗)) = ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖)(._r‘(𝑆 ↑_s (𝐵 ↑_m 𝐼)))(((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)))
123	117, 41, 47, 122	syl3anc 1369	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(._r‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗)) = ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖)(._r‘(𝑆 ↑_s (𝐵 ↑_m 𝐼)))(((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)))
124		mpfind.ct	. . . . . . . . . . . 12 ⊢ · = (._r‘𝑆)
125	9, 13, 56, 57, 59, 60, 124, 120	pwsmulrval 17443	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖)(._r‘(𝑆 ↑_s (𝐵 ↑_m 𝐼)))(((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) = ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘_f · (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)))
126	123, 125	eqtrd 2770	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(._r‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗)) = ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘_f · (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)))
127		ovex 7446	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∘_f · 𝑔) ∈ V
128		mpfind.wf	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑓 ∘_f · 𝑔) → (𝜓 ↔ 𝜎))
129	127, 128	elab 3669	. . . . . . . . . . . . . 14 ⊢ ((𝑓 ∘_f · 𝑔) ∈ {𝑥 ∣ 𝜓} ↔ 𝜎)
130		oveq12 7422	. . . . . . . . . . . . . . 15 ⊢ ((𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∧ 𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) → (𝑓 ∘_f · 𝑔) = ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘_f · (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)))
131	130	eleq1d 2816	. . . . . . . . . . . . . 14 ⊢ ((𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∧ 𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) → ((𝑓 ∘_f · 𝑔) ∈ {𝑥 ∣ 𝜓} ↔ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘_f · (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) ∈ {𝑥 ∣ 𝜓}))
132	129, 131	bitr3id 284	. . . . . . . . . . . . 13 ⊢ ((𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∧ 𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) → (𝜎 ↔ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘_f · (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) ∈ {𝑥 ∣ 𝜓}))
133	94, 132	imbi12d 343	. . . . . . . . . . . 12 ⊢ ((𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∧ 𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) → (((𝜑 ∧ ((𝑓 ∈ 𝑄 ∧ 𝜏) ∧ (𝑔 ∈ 𝑄 ∧ 𝜂))) → 𝜎) ↔ ((𝜑 ∧ (((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥 ∣ 𝜓}) ∧ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥 ∣ 𝜓}))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘_f · (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) ∈ {𝑥 ∣ 𝜓})))
134		mpfind.mu	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑄 ∧ 𝜏) ∧ (𝑔 ∈ 𝑄 ∧ 𝜂))) → 𝜎)
135	77, 78, 133, 134	vtocl2 3553	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥 ∣ 𝜓}) ∧ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥 ∣ 𝜓}))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘_f · (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) ∈ {𝑥 ∣ 𝜓})
136	64, 70, 76, 135	syl12anc 833	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘_f · (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) ∈ {𝑥 ∣ 𝜓})
137	126, 136	eqeltrd 2831	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(._r‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗)) ∈ {𝑥 ∣ 𝜓})
138		elpreima 7060	. . . . . . . . . . 11 ⊢ (((𝐼 evalSub 𝑆)‘𝑅) Fn (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) → ((𝑖(._r‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗) ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ ((𝑖(._r‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗) ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(._r‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗)) ∈ {𝑥 ∣ 𝜓})))
139	16, 138	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑖(._r‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗) ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ ((𝑖(._r‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗) ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(._r‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗)) ∈ {𝑥 ∣ 𝜓})))
140	139	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → ((𝑖(._r‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗) ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ ((𝑖(._r‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗) ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(._r‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗)) ∈ {𝑥 ∣ 𝜓})))
141	112, 137, 140	mpbir2and 709	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (𝑖(._r‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗) ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))
142	141	adantlr 711	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))) ∧ (𝑖 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (𝑖(._r‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))𝑗) ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))
143	7	mplassa 21802	. . . . . . . . . . . . 13 ⊢ ((𝐼 ∈ V ∧ (𝑆 ↾_s 𝑅) ∈ CRing) → (𝐼 mPoly (𝑆 ↾_s 𝑅)) ∈ AssAlg)
144	26, 30, 143	syl2anc 582	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐼 mPoly (𝑆 ↾_s 𝑅)) ∈ AssAlg)
145		eqid 2730	. . . . . . . . . . . . 13 ⊢ (Scalar‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) = (Scalar‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))
146	25, 145	asclrhm 21665	. . . . . . . . . . . 12 ⊢ ((𝐼 mPoly (𝑆 ↾_s 𝑅)) ∈ AssAlg → (algSc‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) ∈ ((Scalar‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) RingHom (𝐼 mPoly (𝑆 ↾_s 𝑅))))
147		eqid 2730	. . . . . . . . . . . . 13 ⊢ (Base‘(Scalar‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))) = (Base‘(Scalar‘(𝐼 mPoly (𝑆 ↾_s 𝑅))))
148	147, 12	rhmf 20378	. . . . . . . . . . . 12 ⊢ ((algSc‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) ∈ ((Scalar‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) RingHom (𝐼 mPoly (𝑆 ↾_s 𝑅))) → (algSc‘(𝐼 mPoly (𝑆 ↾_s 𝑅))):(Base‘(Scalar‘(𝐼 mPoly (𝑆 ↾_s 𝑅))))⟶(Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))))
149	144, 146, 148	3syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → (algSc‘(𝐼 mPoly (𝑆 ↾_s 𝑅))):(Base‘(Scalar‘(𝐼 mPoly (𝑆 ↾_s 𝑅))))⟶(Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))))
150	149	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (Base‘(𝑆 ↾_s 𝑅))) → (algSc‘(𝐼 mPoly (𝑆 ↾_s 𝑅))):(Base‘(Scalar‘(𝐼 mPoly (𝑆 ↾_s 𝑅))))⟶(Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))))
151	7, 26, 30	mplsca 21793	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆 ↾_s 𝑅) = (Scalar‘(𝐼 mPoly (𝑆 ↾_s 𝑅))))
152	151	fveq2d 6896	. . . . . . . . . . . 12 ⊢ (𝜑 → (Base‘(𝑆 ↾_s 𝑅)) = (Base‘(Scalar‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))))
153	152	eleq2d 2817	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑖 ∈ (Base‘(𝑆 ↾_s 𝑅)) ↔ 𝑖 ∈ (Base‘(Scalar‘(𝐼 mPoly (𝑆 ↾_s 𝑅))))))
154	153	biimpa 475	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (Base‘(𝑆 ↾_s 𝑅))) → 𝑖 ∈ (Base‘(Scalar‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))))
155	150, 154	ffvelcdmd 7088	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (Base‘(𝑆 ↾_s 𝑅))) → ((algSc‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))‘𝑖) ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))))
156	26	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (Base‘(𝑆 ↾_s 𝑅))) → 𝐼 ∈ V)
157	27	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (Base‘(𝑆 ↾_s 𝑅))) → 𝑆 ∈ CRing)
158	28	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (Base‘(𝑆 ↾_s 𝑅))) → 𝑅 ∈ (SubRing‘𝑆))
159	10	subrgss 20464	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑅 ⊆ 𝐵)
160	8, 10	ressbas2 17188	. . . . . . . . . . . . . 14 ⊢ (𝑅 ⊆ 𝐵 → 𝑅 = (Base‘(𝑆 ↾_s 𝑅)))
161	28, 159, 160	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑅 = (Base‘(𝑆 ↾_s 𝑅)))
162	161	eleq2d 2817	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑖 ∈ 𝑅 ↔ 𝑖 ∈ (Base‘(𝑆 ↾_s 𝑅))))
163	162	biimpar 476	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (Base‘(𝑆 ↾_s 𝑅))) → 𝑖 ∈ 𝑅)
164	6, 7, 8, 10, 25, 156, 157, 158, 163	evlssca 21873	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (Base‘(𝑆 ↾_s 𝑅))) → (((𝐼 evalSub 𝑆)‘𝑅)‘((algSc‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))‘𝑖)) = ((𝐵 ↑_m 𝐼) × {𝑖}))
165		mpfind.co	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑅) → 𝜒)
166	165	ralrimiva 3144	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑓 ∈ 𝑅 𝜒)
167		ovex 7446	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ↑_m 𝐼) ∈ V
168		vsnex 5430	. . . . . . . . . . . . . . . . 17 ⊢ {𝑓} ∈ V
169	167, 168	xpex 7744	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 ↑_m 𝐼) × {𝑓}) ∈ V
170		mpfind.wa	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = ((𝐵 ↑_m 𝐼) × {𝑓}) → (𝜓 ↔ 𝜒))
171	169, 170	elab 3669	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 ↑_m 𝐼) × {𝑓}) ∈ {𝑥 ∣ 𝜓} ↔ 𝜒)
172		sneq 4639	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝑖 → {𝑓} = {𝑖})
173	172	xpeq2d 5707	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 = 𝑖 → ((𝐵 ↑_m 𝐼) × {𝑓}) = ((𝐵 ↑_m 𝐼) × {𝑖}))
174	173	eleq1d 2816	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑖 → (((𝐵 ↑_m 𝐼) × {𝑓}) ∈ {𝑥 ∣ 𝜓} ↔ ((𝐵 ↑_m 𝐼) × {𝑖}) ∈ {𝑥 ∣ 𝜓}))
175	171, 174	bitr3id 284	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑖 → (𝜒 ↔ ((𝐵 ↑_m 𝐼) × {𝑖}) ∈ {𝑥 ∣ 𝜓}))
176	175	cbvralvw 3232	. . . . . . . . . . . . 13 ⊢ (∀𝑓 ∈ 𝑅 𝜒 ↔ ∀𝑖 ∈ 𝑅 ((𝐵 ↑_m 𝐼) × {𝑖}) ∈ {𝑥 ∣ 𝜓})
177	166, 176	sylib 217	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑖 ∈ 𝑅 ((𝐵 ↑_m 𝐼) × {𝑖}) ∈ {𝑥 ∣ 𝜓})
178	177	r19.21bi 3246	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝑅) → ((𝐵 ↑_m 𝐼) × {𝑖}) ∈ {𝑥 ∣ 𝜓})
179	163, 178	syldan 589	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ (Base‘(𝑆 ↾_s 𝑅))) → ((𝐵 ↑_m 𝐼) × {𝑖}) ∈ {𝑥 ∣ 𝜓})
180	164, 179	eqeltrd 2831	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (Base‘(𝑆 ↾_s 𝑅))) → (((𝐼 evalSub 𝑆)‘𝑅)‘((algSc‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))‘𝑖)) ∈ {𝑥 ∣ 𝜓})
181		elpreima 7060	. . . . . . . . . . 11 ⊢ (((𝐼 evalSub 𝑆)‘𝑅) Fn (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) → (((algSc‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))‘𝑖) ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ (((algSc‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))‘𝑖) ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘((algSc‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))‘𝑖)) ∈ {𝑥 ∣ 𝜓})))
182	16, 181	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (((algSc‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))‘𝑖) ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ (((algSc‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))‘𝑖) ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘((algSc‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))‘𝑖)) ∈ {𝑥 ∣ 𝜓})))
183	182	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (Base‘(𝑆 ↾_s 𝑅))) → (((algSc‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))‘𝑖) ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ (((algSc‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))‘𝑖) ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘((algSc‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))‘𝑖)) ∈ {𝑥 ∣ 𝜓})))
184	155, 180, 183	mpbir2and 709	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (Base‘(𝑆 ↾_s 𝑅))) → ((algSc‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))‘𝑖) ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))
185	184	adantlr 711	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))) ∧ 𝑖 ∈ (Base‘(𝑆 ↾_s 𝑅))) → ((algSc‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))‘𝑖) ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))
186	26	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → 𝐼 ∈ V)
187	32	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝑆 ↾_s 𝑅) ∈ Ring)
188		simpr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → 𝑖 ∈ 𝐼)
189	7, 22, 12, 186, 187, 188	mvrcl 21772	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → ((𝐼 mVar (𝑆 ↾_s 𝑅))‘𝑖) ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))))
190	27	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → 𝑆 ∈ CRing)
191	28	adantr 479	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → 𝑅 ∈ (SubRing‘𝑆))
192	6, 22, 8, 10, 186, 190, 191, 188	evlsvar 21874	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (((𝐼 evalSub 𝑆)‘𝑅)‘((𝐼 mVar (𝑆 ↾_s 𝑅))‘𝑖)) = (𝑔 ∈ (𝐵 ↑_m 𝐼) ↦ (𝑔‘𝑖)))
193		mpfind.pr	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐼) → 𝜃)
194	167	mptex 7228	. . . . . . . . . . . . . . 15 ⊢ (𝑔 ∈ (𝐵 ↑_m 𝐼) ↦ (𝑔‘𝑓)) ∈ V
195		mpfind.wb	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (𝑔 ∈ (𝐵 ↑_m 𝐼) ↦ (𝑔‘𝑓)) → (𝜓 ↔ 𝜃))
196	194, 195	elab 3669	. . . . . . . . . . . . . 14 ⊢ ((𝑔 ∈ (𝐵 ↑_m 𝐼) ↦ (𝑔‘𝑓)) ∈ {𝑥 ∣ 𝜓} ↔ 𝜃)
197	193, 196	sylibr 233	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑓 ∈ 𝐼) → (𝑔 ∈ (𝐵 ↑_m 𝐼) ↦ (𝑔‘𝑓)) ∈ {𝑥 ∣ 𝜓})
198	197	ralrimiva 3144	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑓 ∈ 𝐼 (𝑔 ∈ (𝐵 ↑_m 𝐼) ↦ (𝑔‘𝑓)) ∈ {𝑥 ∣ 𝜓})
199		fveq2 6892	. . . . . . . . . . . . . . 15 ⊢ (𝑓 = 𝑖 → (𝑔‘𝑓) = (𝑔‘𝑖))
200	199	mpteq2dv 5251	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝑖 → (𝑔 ∈ (𝐵 ↑_m 𝐼) ↦ (𝑔‘𝑓)) = (𝑔 ∈ (𝐵 ↑_m 𝐼) ↦ (𝑔‘𝑖)))
201	200	eleq1d 2816	. . . . . . . . . . . . 13 ⊢ (𝑓 = 𝑖 → ((𝑔 ∈ (𝐵 ↑_m 𝐼) ↦ (𝑔‘𝑓)) ∈ {𝑥 ∣ 𝜓} ↔ (𝑔 ∈ (𝐵 ↑_m 𝐼) ↦ (𝑔‘𝑖)) ∈ {𝑥 ∣ 𝜓}))
202	201	cbvralvw 3232	. . . . . . . . . . . 12 ⊢ (∀𝑓 ∈ 𝐼 (𝑔 ∈ (𝐵 ↑_m 𝐼) ↦ (𝑔‘𝑓)) ∈ {𝑥 ∣ 𝜓} ↔ ∀𝑖 ∈ 𝐼 (𝑔 ∈ (𝐵 ↑_m 𝐼) ↦ (𝑔‘𝑖)) ∈ {𝑥 ∣ 𝜓})
203	198, 202	sylib 217	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑖 ∈ 𝐼 (𝑔 ∈ (𝐵 ↑_m 𝐼) ↦ (𝑔‘𝑖)) ∈ {𝑥 ∣ 𝜓})
204	203	r19.21bi 3246	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝑔 ∈ (𝐵 ↑_m 𝐼) ↦ (𝑔‘𝑖)) ∈ {𝑥 ∣ 𝜓})
205	192, 204	eqeltrd 2831	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (((𝐼 evalSub 𝑆)‘𝑅)‘((𝐼 mVar (𝑆 ↾_s 𝑅))‘𝑖)) ∈ {𝑥 ∣ 𝜓})
206		elpreima 7060	. . . . . . . . . . 11 ⊢ (((𝐼 evalSub 𝑆)‘𝑅) Fn (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) → (((𝐼 mVar (𝑆 ↾_s 𝑅))‘𝑖) ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ (((𝐼 mVar (𝑆 ↾_s 𝑅))‘𝑖) ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘((𝐼 mVar (𝑆 ↾_s 𝑅))‘𝑖)) ∈ {𝑥 ∣ 𝜓})))
207	16, 206	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐼 mVar (𝑆 ↾_s 𝑅))‘𝑖) ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ (((𝐼 mVar (𝑆 ↾_s 𝑅))‘𝑖) ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘((𝐼 mVar (𝑆 ↾_s 𝑅))‘𝑖)) ∈ {𝑥 ∣ 𝜓})))
208	207	adantr 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (((𝐼 mVar (𝑆 ↾_s 𝑅))‘𝑖) ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ (((𝐼 mVar (𝑆 ↾_s 𝑅))‘𝑖) ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘((𝐼 mVar (𝑆 ↾_s 𝑅))‘𝑖)) ∈ {𝑥 ∣ 𝜓})))
209	189, 205, 208	mpbir2and 709	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → ((𝐼 mVar (𝑆 ↾_s 𝑅))‘𝑖) ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))
210	209	adantlr 711	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))) ∧ 𝑖 ∈ 𝐼) → ((𝐼 mVar (𝑆 ↾_s 𝑅))‘𝑖) ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))
211		simpr 483	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))) → 𝑦 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅))))
212	26	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))) → 𝐼 ∈ V)
213	30	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))) → (𝑆 ↾_s 𝑅) ∈ CRing)
214	21, 22, 7, 23, 24, 25, 12, 110, 142, 185, 210, 211, 212, 213	mplind 21852	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))) → 𝑦 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))
215		fvimacnvi 7054	. . . . . 6 ⊢ ((Fun ((𝐼 evalSub 𝑆)‘𝑅) ∧ 𝑦 ∈ (^◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓})) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑦) ∈ {𝑥 ∣ 𝜓})
216	20, 214, 215	syl2an2r 681	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑦) ∈ {𝑥 ∣ 𝜓})
217		eleq1 2819	. . . . 5 ⊢ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑦) = 𝐴 → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑦) ∈ {𝑥 ∣ 𝜓} ↔ 𝐴 ∈ {𝑥 ∣ 𝜓}))
218	216, 217	syl5ibcom 244	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑦) = 𝐴 → 𝐴 ∈ {𝑥 ∣ 𝜓}))
219	218	rexlimdva 3153	. . 3 ⊢ (𝜑 → (∃𝑦 ∈ (Base‘(𝐼 mPoly (𝑆 ↾_s 𝑅)))(((𝐼 evalSub 𝑆)‘𝑅)‘𝑦) = 𝐴 → 𝐴 ∈ {𝑥 ∣ 𝜓}))
220	19, 219	mpd 15	. 2 ⊢ (𝜑 → 𝐴 ∈ {𝑥 ∣ 𝜓})
221		mpfind.wg	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜌))
222	221	elabg 3667	. . 3 ⊢ (𝐴 ∈ 𝑄 → (𝐴 ∈ {𝑥 ∣ 𝜓} ↔ 𝜌))
223	1, 222	syl 17	. 2 ⊢ (𝜑 → (𝐴 ∈ {𝑥 ∣ 𝜓} ↔ 𝜌))
224	220, 223	mpbid 231	1 ⊢ (𝜑 → 𝜌)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∧ w3a 1085 = wceq 1539 ∈ wcel 2104 {cab 2707 ∀wral 3059 ∃wrex 3068 Vcvv 3472 ⊆ wss 3949 {csn 4629 ↦ cmpt 5232 × cxp 5675 ^◡ccnv 5676 ran crn 5678 “ cima 5680 Fun wfun 6538 Fn wfn 6539 ⟶wf 6540 ‘cfv 6544 (class class class)co 7413 ∘_f cof 7672 ↑_m cmap 8824 Basecbs 17150 ↾_s cress 17179 +_gcplusg 17203 ._rcmulr 17204 Scalarcsca 17206 ↑_s cpws 17398 MndHom cmhm 18705 GrpHom cghm 19129 mulGrpcmgp 20030 Ringcrg 20129 CRingccrg 20130 RingHom crh 20362 SubRingcsubrg 20459 AssAlgcasa 21626 algSccascl 21628 mVar cmvr 21679 mPoly cmpl 21680 evalSub ces 21854

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7729 ax-cnex 11170 ax-resscn 11171 ax-1cn 11172 ax-icn 11173 ax-addcl 11174 ax-addrcl 11175 ax-mulcl 11176 ax-mulrcl 11177 ax-mulcom 11178 ax-addass 11179 ax-mulass 11180 ax-distr 11181 ax-i2m1 11182 ax-1ne0 11183 ax-1rid 11184 ax-rnegex 11185 ax-rrecex 11186 ax-cnre 11187 ax-pre-lttri 11188 ax-pre-lttrn 11189 ax-pre-ltadd 11190 ax-pre-mulgt0 11191

This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3374 df-reu 3375 df-rab 3431 df-v 3474 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-tp 4634 df-op 4636 df-uni 4910 df-int 4952 df-iun 5000 df-iin 5001 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-se 5633 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-isom 6553 df-riota 7369 df-ov 7416 df-oprab 7417 df-mpo 7418 df-of 7674 df-ofr 7675 df-om 7860 df-1st 7979 df-2nd 7980 df-supp 8151 df-frecs 8270 df-wrecs 8301 df-recs 8375 df-rdg 8414 df-1o 8470 df-er 8707 df-map 8826 df-pm 8827 df-ixp 8896 df-en 8944 df-dom 8945 df-sdom 8946 df-fin 8947 df-fsupp 9366 df-sup 9441 df-oi 9509 df-card 9938 df-pnf 11256 df-mnf 11257 df-xr 11258 df-ltxr 11259 df-le 11260 df-sub 11452 df-neg 11453 df-nn 12219 df-2 12281 df-3 12282 df-4 12283 df-5 12284 df-6 12285 df-7 12286 df-8 12287 df-9 12288 df-n0 12479 df-z 12565 df-dec 12684 df-uz 12829 df-fz 13491 df-fzo 13634 df-seq 13973 df-hash 14297 df-struct 17086 df-sets 17103 df-slot 17121 df-ndx 17133 df-base 17151 df-ress 17180 df-plusg 17216 df-mulr 17217 df-sca 17219 df-vsca 17220 df-ip 17221 df-tset 17222 df-ple 17223 df-ds 17225 df-hom 17227 df-cco 17228 df-0g 17393 df-gsum 17394 df-prds 17399 df-pws 17401 df-mre 17536 df-mrc 17537 df-acs 17539 df-mgm 18567 df-sgrp 18646 df-mnd 18662 df-mhm 18707 df-submnd 18708 df-grp 18860 df-minusg 18861 df-sbg 18862 df-mulg 18989 df-subg 19041 df-ghm 19130 df-cntz 19224 df-cmn 19693 df-abl 19694 df-mgp 20031 df-rng 20049 df-ur 20078 df-srg 20083 df-ring 20131 df-cring 20132 df-rhm 20365 df-subrng 20436 df-subrg 20461 df-lmod 20618 df-lss 20689 df-lsp 20729 df-assa 21629 df-asp 21630 df-ascl 21631 df-psr 21683 df-mvr 21684 df-mpl 21685 df-evls 21856

This theorem is referenced by: pf1ind 22096 mzpmfp 41789

W3C validator