Step | Hyp | Ref
| Expression |
1 | | mpfind.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑄) |
2 | | mpfind.cq |
. . . . 5
⊢ 𝑄 = ran ((𝐼 evalSub 𝑆)‘𝑅) |
3 | 1, 2 | syl6eleq 2698 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ ran ((𝐼 evalSub 𝑆)‘𝑅)) |
4 | 2 | mpfrcl 19339 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑄 → (𝐼 ∈ V ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆))) |
5 | 1, 4 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐼 ∈ V ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆))) |
6 | | eqid 2610 |
. . . . . . . . 9
⊢ ((𝐼 evalSub 𝑆)‘𝑅) = ((𝐼 evalSub 𝑆)‘𝑅) |
7 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝐼 mPoly (𝑆 ↾s 𝑅)) = (𝐼 mPoly (𝑆 ↾s 𝑅)) |
8 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑆 ↾s 𝑅) = (𝑆 ↾s 𝑅) |
9 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑆 ↑s
(𝐵
↑𝑚 𝐼)) = (𝑆 ↑s (𝐵 ↑𝑚
𝐼)) |
10 | | mpfind.cb |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑆) |
11 | 6, 7, 8, 9, 10 | evlsrhm 19342 |
. . . . . . . 8
⊢ ((𝐼 ∈ V ∧ 𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → ((𝐼 evalSub 𝑆)‘𝑅) ∈ ((𝐼 mPoly (𝑆 ↾s 𝑅)) RingHom (𝑆 ↑s (𝐵 ↑𝑚
𝐼)))) |
12 | 5, 11 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝐼 evalSub 𝑆)‘𝑅) ∈ ((𝐼 mPoly (𝑆 ↾s 𝑅)) RingHom (𝑆 ↑s (𝐵 ↑𝑚
𝐼)))) |
13 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘(𝐼 mPoly
(𝑆 ↾s
𝑅))) = (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) |
14 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘(𝑆
↑s (𝐵 ↑𝑚 𝐼))) = (Base‘(𝑆 ↑s
(𝐵
↑𝑚 𝐼))) |
15 | 13, 14 | rhmf 18549 |
. . . . . . 7
⊢ (((𝐼 evalSub 𝑆)‘𝑅) ∈ ((𝐼 mPoly (𝑆 ↾s 𝑅)) RingHom (𝑆 ↑s (𝐵 ↑𝑚
𝐼))) → ((𝐼 evalSub 𝑆)‘𝑅):(Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))⟶(Base‘(𝑆 ↑s (𝐵 ↑𝑚
𝐼)))) |
16 | 12, 15 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝐼 evalSub 𝑆)‘𝑅):(Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))⟶(Base‘(𝑆 ↑s (𝐵 ↑𝑚
𝐼)))) |
17 | | ffn 5958 |
. . . . . 6
⊢ (((𝐼 evalSub 𝑆)‘𝑅):(Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))⟶(Base‘(𝑆 ↑s (𝐵 ↑𝑚
𝐼))) → ((𝐼 evalSub 𝑆)‘𝑅) Fn (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) |
18 | 16, 17 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝐼 evalSub 𝑆)‘𝑅) Fn (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) |
19 | | fvelrnb 6153 |
. . . . 5
⊢ (((𝐼 evalSub 𝑆)‘𝑅) Fn (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) → (𝐴 ∈ ran ((𝐼 evalSub 𝑆)‘𝑅) ↔ ∃𝑦 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))(((𝐼 evalSub 𝑆)‘𝑅)‘𝑦) = 𝐴)) |
20 | 18, 19 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐴 ∈ ran ((𝐼 evalSub 𝑆)‘𝑅) ↔ ∃𝑦 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))(((𝐼 evalSub 𝑆)‘𝑅)‘𝑦) = 𝐴)) |
21 | 3, 20 | mpbid 221 |
. . 3
⊢ (𝜑 → ∃𝑦 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))(((𝐼 evalSub 𝑆)‘𝑅)‘𝑦) = 𝐴) |
22 | | ffun 5961 |
. . . . . . . 8
⊢ (((𝐼 evalSub 𝑆)‘𝑅):(Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))⟶(Base‘(𝑆 ↑s (𝐵 ↑𝑚
𝐼))) → Fun ((𝐼 evalSub 𝑆)‘𝑅)) |
23 | 16, 22 | syl 17 |
. . . . . . 7
⊢ (𝜑 → Fun ((𝐼 evalSub 𝑆)‘𝑅)) |
24 | 23 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) → Fun ((𝐼 evalSub 𝑆)‘𝑅)) |
25 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘(𝑆
↾s 𝑅)) =
(Base‘(𝑆
↾s 𝑅)) |
26 | | eqid 2610 |
. . . . . . 7
⊢ (𝐼 mVar (𝑆 ↾s 𝑅)) = (𝐼 mVar (𝑆 ↾s 𝑅)) |
27 | | eqid 2610 |
. . . . . . 7
⊢
(+g‘(𝐼 mPoly (𝑆 ↾s 𝑅))) = (+g‘(𝐼 mPoly (𝑆 ↾s 𝑅))) |
28 | | eqid 2610 |
. . . . . . 7
⊢
(.r‘(𝐼 mPoly (𝑆 ↾s 𝑅))) = (.r‘(𝐼 mPoly (𝑆 ↾s 𝑅))) |
29 | | eqid 2610 |
. . . . . . 7
⊢
(algSc‘(𝐼
mPoly (𝑆
↾s 𝑅))) =
(algSc‘(𝐼 mPoly
(𝑆 ↾s
𝑅))) |
30 | 5 | simp1d 1066 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐼 ∈ V) |
31 | 5 | simp2d 1067 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ∈ CRing) |
32 | 5 | simp3d 1068 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 ∈ (SubRing‘𝑆)) |
33 | 8 | subrgcrng 18607 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ CRing ∧ 𝑅 ∈ (SubRing‘𝑆)) → (𝑆 ↾s 𝑅) ∈ CRing) |
34 | 31, 32, 33 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆 ↾s 𝑅) ∈ CRing) |
35 | | crngring 18381 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ↾s 𝑅) ∈ CRing → (𝑆 ↾s 𝑅) ∈ Ring) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆 ↾s 𝑅) ∈ Ring) |
37 | 7 | mplring 19273 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ V ∧ (𝑆 ↾s 𝑅) ∈ Ring) → (𝐼 mPoly (𝑆 ↾s 𝑅)) ∈ Ring) |
38 | 30, 36, 37 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐼 mPoly (𝑆 ↾s 𝑅)) ∈ Ring) |
39 | 38 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (𝐼 mPoly (𝑆 ↾s 𝑅)) ∈ Ring) |
40 | | simprl 790 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → 𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓})) |
41 | | elpreima 6245 |
. . . . . . . . . . . . . 14
⊢ (((𝐼 evalSub 𝑆)‘𝑅) Fn (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) → (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ (𝑖 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥 ∣ 𝜓}))) |
42 | 18, 41 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ (𝑖 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥 ∣ 𝜓}))) |
43 | 42 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ (𝑖 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥 ∣ 𝜓}))) |
44 | 40, 43 | mpbid 221 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (𝑖 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥 ∣ 𝜓})) |
45 | 44 | simpld 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → 𝑖 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) |
46 | | simprr 792 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓})) |
47 | | elpreima 6245 |
. . . . . . . . . . . . . 14
⊢ (((𝐼 evalSub 𝑆)‘𝑅) Fn (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) → (𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ (𝑗 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥 ∣ 𝜓}))) |
48 | 18, 47 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ (𝑗 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥 ∣ 𝜓}))) |
49 | 48 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ (𝑗 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥 ∣ 𝜓}))) |
50 | 46, 49 | mpbid 221 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (𝑗 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥 ∣ 𝜓})) |
51 | 50 | simpld 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → 𝑗 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) |
52 | 13, 27 | ringacl 18401 |
. . . . . . . . . 10
⊢ (((𝐼 mPoly (𝑆 ↾s 𝑅)) ∈ Ring ∧ 𝑖 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) ∧ 𝑗 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) → (𝑖(+g‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗) ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) |
53 | 39, 45, 51, 52 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (𝑖(+g‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗) ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) |
54 | | rhmghm 18548 |
. . . . . . . . . . . . . 14
⊢ (((𝐼 evalSub 𝑆)‘𝑅) ∈ ((𝐼 mPoly (𝑆 ↾s 𝑅)) RingHom (𝑆 ↑s (𝐵 ↑𝑚
𝐼))) → ((𝐼 evalSub 𝑆)‘𝑅) ∈ ((𝐼 mPoly (𝑆 ↾s 𝑅)) GrpHom (𝑆 ↑s (𝐵 ↑𝑚
𝐼)))) |
55 | 12, 54 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐼 evalSub 𝑆)‘𝑅) ∈ ((𝐼 mPoly (𝑆 ↾s 𝑅)) GrpHom (𝑆 ↑s (𝐵 ↑𝑚
𝐼)))) |
56 | 55 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → ((𝐼 evalSub 𝑆)‘𝑅) ∈ ((𝐼 mPoly (𝑆 ↾s 𝑅)) GrpHom (𝑆 ↑s (𝐵 ↑𝑚
𝐼)))) |
57 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(+g‘(𝑆 ↑s (𝐵 ↑𝑚
𝐼))) =
(+g‘(𝑆
↑s (𝐵 ↑𝑚 𝐼))) |
58 | 13, 27, 57 | ghmlin 17488 |
. . . . . . . . . . . 12
⊢ ((((𝐼 evalSub 𝑆)‘𝑅) ∈ ((𝐼 mPoly (𝑆 ↾s 𝑅)) GrpHom (𝑆 ↑s (𝐵 ↑𝑚
𝐼))) ∧ 𝑖 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) ∧ 𝑗 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) → (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(+g‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗)) = ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖)(+g‘(𝑆 ↑s (𝐵 ↑𝑚
𝐼)))(((𝐼 evalSub 𝑆)‘𝑅)‘𝑗))) |
59 | 56, 45, 51, 58 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(+g‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗)) = ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖)(+g‘(𝑆 ↑s (𝐵 ↑𝑚
𝐼)))(((𝐼 evalSub 𝑆)‘𝑅)‘𝑗))) |
60 | 31 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → 𝑆 ∈ CRing) |
61 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢ (𝐵 ↑𝑚
𝐼) ∈
V |
62 | 61 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (𝐵 ↑𝑚 𝐼) ∈ V) |
63 | 16 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → ((𝐼 evalSub 𝑆)‘𝑅):(Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))⟶(Base‘(𝑆 ↑s (𝐵 ↑𝑚
𝐼)))) |
64 | 63, 45 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ (Base‘(𝑆 ↑s (𝐵 ↑𝑚
𝐼)))) |
65 | 63, 51 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ (Base‘(𝑆 ↑s (𝐵 ↑𝑚
𝐼)))) |
66 | | mpfind.cp |
. . . . . . . . . . . 12
⊢ + =
(+g‘𝑆) |
67 | 9, 14, 60, 62, 64, 65, 66, 57 | pwsplusgval 15973 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖)(+g‘(𝑆 ↑s (𝐵 ↑𝑚
𝐼)))(((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) = ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘𝑓 + (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗))) |
68 | 59, 67 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(+g‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗)) = ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘𝑓 + (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗))) |
69 | | simpl 472 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → 𝜑) |
70 | 18 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → ((𝐼 evalSub 𝑆)‘𝑅) Fn (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) |
71 | | fnfvelrn 6264 |
. . . . . . . . . . . . . 14
⊢ ((((𝐼 evalSub 𝑆)‘𝑅) Fn (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) ∧ 𝑖 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ ran ((𝐼 evalSub 𝑆)‘𝑅)) |
72 | 70, 45, 71 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ ran ((𝐼 evalSub 𝑆)‘𝑅)) |
73 | 72, 2 | syl6eleqr 2699 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ 𝑄) |
74 | 23 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → Fun ((𝐼 evalSub 𝑆)‘𝑅)) |
75 | | fvimacnvi 6239 |
. . . . . . . . . . . . 13
⊢ ((Fun
((𝐼 evalSub 𝑆)‘𝑅) ∧ 𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓})) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥 ∣ 𝜓}) |
76 | 74, 40, 75 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥 ∣ 𝜓}) |
77 | 73, 76 | jca 553 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥 ∣ 𝜓})) |
78 | | fnfvelrn 6264 |
. . . . . . . . . . . . . 14
⊢ ((((𝐼 evalSub 𝑆)‘𝑅) Fn (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) ∧ 𝑗 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ ran ((𝐼 evalSub 𝑆)‘𝑅)) |
79 | 70, 51, 78 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ ran ((𝐼 evalSub 𝑆)‘𝑅)) |
80 | 79, 2 | syl6eleqr 2699 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ 𝑄) |
81 | | fvimacnvi 6239 |
. . . . . . . . . . . . 13
⊢ ((Fun
((𝐼 evalSub 𝑆)‘𝑅) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓})) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥 ∣ 𝜓}) |
82 | 74, 46, 81 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥 ∣ 𝜓}) |
83 | 80, 82 | jca 553 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥 ∣ 𝜓})) |
84 | | fvex 6113 |
. . . . . . . . . . . 12
⊢ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ V |
85 | | fvex 6113 |
. . . . . . . . . . . 12
⊢ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ V |
86 | | eleq1 2676 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) → (𝑓 ∈ 𝑄 ↔ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ 𝑄)) |
87 | | vex 3176 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑓 ∈ V |
88 | | mpfind.wc |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑓 → (𝜓 ↔ 𝜏)) |
89 | 87, 88 | elab 3319 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ {𝑥 ∣ 𝜓} ↔ 𝜏) |
90 | | eleq1 2676 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) → (𝑓 ∈ {𝑥 ∣ 𝜓} ↔ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥 ∣ 𝜓})) |
91 | 89, 90 | syl5bbr 273 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) → (𝜏 ↔ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥 ∣ 𝜓})) |
92 | 86, 91 | anbi12d 743 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) → ((𝑓 ∈ 𝑄 ∧ 𝜏) ↔ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥 ∣ 𝜓}))) |
93 | | eleq1 2676 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) → (𝑔 ∈ 𝑄 ↔ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ 𝑄)) |
94 | | vex 3176 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑔 ∈ V |
95 | | mpfind.wd |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑔 → (𝜓 ↔ 𝜂)) |
96 | 94, 95 | elab 3319 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 ∈ {𝑥 ∣ 𝜓} ↔ 𝜂) |
97 | | eleq1 2676 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) → (𝑔 ∈ {𝑥 ∣ 𝜓} ↔ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥 ∣ 𝜓})) |
98 | 96, 97 | syl5bbr 273 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) → (𝜂 ↔ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥 ∣ 𝜓})) |
99 | 93, 98 | anbi12d 743 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) → ((𝑔 ∈ 𝑄 ∧ 𝜂) ↔ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥 ∣ 𝜓}))) |
100 | 92, 99 | bi2anan9 913 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∧ 𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) → (((𝑓 ∈ 𝑄 ∧ 𝜏) ∧ (𝑔 ∈ 𝑄 ∧ 𝜂)) ↔ (((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥 ∣ 𝜓}) ∧ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥 ∣ 𝜓})))) |
101 | 100 | anbi2d 736 |
. . . . . . . . . . . . 13
⊢ ((𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∧ 𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) → ((𝜑 ∧ ((𝑓 ∈ 𝑄 ∧ 𝜏) ∧ (𝑔 ∈ 𝑄 ∧ 𝜂))) ↔ (𝜑 ∧ (((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥 ∣ 𝜓}) ∧ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥 ∣ 𝜓}))))) |
102 | | ovex 6577 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∘𝑓
+ 𝑔) ∈ V |
103 | | mpfind.we |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑓 ∘𝑓 + 𝑔) → (𝜓 ↔ 𝜁)) |
104 | 102, 103 | elab 3319 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∘𝑓
+ 𝑔) ∈ {𝑥 ∣ 𝜓} ↔ 𝜁) |
105 | | oveq12 6558 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∧ 𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) → (𝑓 ∘𝑓 + 𝑔) = ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘𝑓 + (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗))) |
106 | 105 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∧ 𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) → ((𝑓 ∘𝑓 + 𝑔) ∈ {𝑥 ∣ 𝜓} ↔ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘𝑓 + (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) ∈ {𝑥 ∣ 𝜓})) |
107 | 104, 106 | syl5bbr 273 |
. . . . . . . . . . . . 13
⊢ ((𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∧ 𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) → (𝜁 ↔ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘𝑓 + (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) ∈ {𝑥 ∣ 𝜓})) |
108 | 101, 107 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ ((𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∧ 𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) → (((𝜑 ∧ ((𝑓 ∈ 𝑄 ∧ 𝜏) ∧ (𝑔 ∈ 𝑄 ∧ 𝜂))) → 𝜁) ↔ ((𝜑 ∧ (((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥 ∣ 𝜓}) ∧ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥 ∣ 𝜓}))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘𝑓 + (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) ∈ {𝑥 ∣ 𝜓}))) |
109 | | mpfind.ad |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑄 ∧ 𝜏) ∧ (𝑔 ∈ 𝑄 ∧ 𝜂))) → 𝜁) |
110 | 84, 85, 108, 109 | vtocl2 3234 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥 ∣ 𝜓}) ∧ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥 ∣ 𝜓}))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘𝑓 + (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) ∈ {𝑥 ∣ 𝜓}) |
111 | 69, 77, 83, 110 | syl12anc 1316 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘𝑓 + (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) ∈ {𝑥 ∣ 𝜓}) |
112 | 68, 111 | eqeltrd 2688 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(+g‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗)) ∈ {𝑥 ∣ 𝜓}) |
113 | | elpreima 6245 |
. . . . . . . . . . 11
⊢ (((𝐼 evalSub 𝑆)‘𝑅) Fn (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) → ((𝑖(+g‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗) ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ ((𝑖(+g‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗) ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(+g‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗)) ∈ {𝑥 ∣ 𝜓}))) |
114 | 18, 113 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑖(+g‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗) ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ ((𝑖(+g‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗) ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(+g‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗)) ∈ {𝑥 ∣ 𝜓}))) |
115 | 114 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → ((𝑖(+g‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗) ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ ((𝑖(+g‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗) ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(+g‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗)) ∈ {𝑥 ∣ 𝜓}))) |
116 | 53, 112, 115 | mpbir2and 959 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (𝑖(+g‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗) ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓})) |
117 | 116 | adantlr 747 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (𝑖(+g‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗) ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓})) |
118 | 13, 28 | ringcl 18384 |
. . . . . . . . . 10
⊢ (((𝐼 mPoly (𝑆 ↾s 𝑅)) ∈ Ring ∧ 𝑖 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) ∧ 𝑗 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) → (𝑖(.r‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗) ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) |
119 | 39, 45, 51, 118 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (𝑖(.r‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗) ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) |
120 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(mulGrp‘(𝐼
mPoly (𝑆
↾s 𝑅))) =
(mulGrp‘(𝐼 mPoly
(𝑆 ↾s
𝑅))) |
121 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(mulGrp‘(𝑆
↑s (𝐵 ↑𝑚 𝐼))) = (mulGrp‘(𝑆 ↑s
(𝐵
↑𝑚 𝐼))) |
122 | 120, 121 | rhmmhm 18545 |
. . . . . . . . . . . . . 14
⊢ (((𝐼 evalSub 𝑆)‘𝑅) ∈ ((𝐼 mPoly (𝑆 ↾s 𝑅)) RingHom (𝑆 ↑s (𝐵 ↑𝑚
𝐼))) → ((𝐼 evalSub 𝑆)‘𝑅) ∈ ((mulGrp‘(𝐼 mPoly (𝑆 ↾s 𝑅))) MndHom (mulGrp‘(𝑆 ↑s (𝐵 ↑𝑚
𝐼))))) |
123 | 12, 122 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐼 evalSub 𝑆)‘𝑅) ∈ ((mulGrp‘(𝐼 mPoly (𝑆 ↾s 𝑅))) MndHom (mulGrp‘(𝑆 ↑s (𝐵 ↑𝑚
𝐼))))) |
124 | 123 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → ((𝐼 evalSub 𝑆)‘𝑅) ∈ ((mulGrp‘(𝐼 mPoly (𝑆 ↾s 𝑅))) MndHom (mulGrp‘(𝑆 ↑s (𝐵 ↑𝑚
𝐼))))) |
125 | 120, 13 | mgpbas 18318 |
. . . . . . . . . . . . 13
⊢
(Base‘(𝐼 mPoly
(𝑆 ↾s
𝑅))) =
(Base‘(mulGrp‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) |
126 | 120, 28 | mgpplusg 18316 |
. . . . . . . . . . . . 13
⊢
(.r‘(𝐼 mPoly (𝑆 ↾s 𝑅))) =
(+g‘(mulGrp‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) |
127 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(.r‘(𝑆 ↑s (𝐵 ↑𝑚
𝐼))) =
(.r‘(𝑆
↑s (𝐵 ↑𝑚 𝐼))) |
128 | 121, 127 | mgpplusg 18316 |
. . . . . . . . . . . . 13
⊢
(.r‘(𝑆 ↑s (𝐵 ↑𝑚
𝐼))) =
(+g‘(mulGrp‘(𝑆 ↑s (𝐵 ↑𝑚
𝐼)))) |
129 | 125, 126,
128 | mhmlin 17165 |
. . . . . . . . . . . 12
⊢ ((((𝐼 evalSub 𝑆)‘𝑅) ∈ ((mulGrp‘(𝐼 mPoly (𝑆 ↾s 𝑅))) MndHom (mulGrp‘(𝑆 ↑s (𝐵 ↑𝑚
𝐼)))) ∧ 𝑖 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) ∧ 𝑗 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) → (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(.r‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗)) = ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖)(.r‘(𝑆 ↑s (𝐵 ↑𝑚
𝐼)))(((𝐼 evalSub 𝑆)‘𝑅)‘𝑗))) |
130 | 124, 45, 51, 129 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(.r‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗)) = ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖)(.r‘(𝑆 ↑s (𝐵 ↑𝑚
𝐼)))(((𝐼 evalSub 𝑆)‘𝑅)‘𝑗))) |
131 | | mpfind.ct |
. . . . . . . . . . . 12
⊢ · =
(.r‘𝑆) |
132 | 9, 14, 60, 62, 64, 65, 131, 127 | pwsmulrval 15974 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖)(.r‘(𝑆 ↑s (𝐵 ↑𝑚
𝐼)))(((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) = ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘𝑓 ·
(((𝐼 evalSub 𝑆)‘𝑅)‘𝑗))) |
133 | 130, 132 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(.r‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗)) = ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘𝑓 ·
(((𝐼 evalSub 𝑆)‘𝑅)‘𝑗))) |
134 | | ovex 6577 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∘𝑓
·
𝑔) ∈
V |
135 | | mpfind.wf |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑓 ∘𝑓 · 𝑔) → (𝜓 ↔ 𝜎)) |
136 | 134, 135 | elab 3319 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∘𝑓
·
𝑔) ∈ {𝑥 ∣ 𝜓} ↔ 𝜎) |
137 | | oveq12 6558 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∧ 𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) → (𝑓 ∘𝑓 · 𝑔) = ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘𝑓 ·
(((𝐼 evalSub 𝑆)‘𝑅)‘𝑗))) |
138 | 137 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∧ 𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) → ((𝑓 ∘𝑓 · 𝑔) ∈ {𝑥 ∣ 𝜓} ↔ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘𝑓 ·
(((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) ∈ {𝑥 ∣ 𝜓})) |
139 | 136, 138 | syl5bbr 273 |
. . . . . . . . . . . . 13
⊢ ((𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∧ 𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) → (𝜎 ↔ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘𝑓 ·
(((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) ∈ {𝑥 ∣ 𝜓})) |
140 | 101, 139 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ ((𝑓 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∧ 𝑔 = (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) → (((𝜑 ∧ ((𝑓 ∈ 𝑄 ∧ 𝜏) ∧ (𝑔 ∈ 𝑄 ∧ 𝜂))) → 𝜎) ↔ ((𝜑 ∧ (((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥 ∣ 𝜓}) ∧ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥 ∣ 𝜓}))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘𝑓 ·
(((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) ∈ {𝑥 ∣ 𝜓}))) |
141 | | mpfind.mu |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑓 ∈ 𝑄 ∧ 𝜏) ∧ (𝑔 ∈ 𝑄 ∧ 𝜂))) → 𝜎) |
142 | 84, 85, 140, 141 | vtocl2 3234 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∈ {𝑥 ∣ 𝜓}) ∧ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ 𝑄 ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘𝑗) ∈ {𝑥 ∣ 𝜓}))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘𝑓 ·
(((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) ∈ {𝑥 ∣ 𝜓}) |
143 | 69, 77, 83, 142 | syl12anc 1316 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑖) ∘𝑓 ·
(((𝐼 evalSub 𝑆)‘𝑅)‘𝑗)) ∈ {𝑥 ∣ 𝜓}) |
144 | 133, 143 | eqeltrd 2688 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(.r‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗)) ∈ {𝑥 ∣ 𝜓}) |
145 | | elpreima 6245 |
. . . . . . . . . . 11
⊢ (((𝐼 evalSub 𝑆)‘𝑅) Fn (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) → ((𝑖(.r‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗) ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ ((𝑖(.r‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗) ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(.r‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗)) ∈ {𝑥 ∣ 𝜓}))) |
146 | 18, 145 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑖(.r‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗) ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ ((𝑖(.r‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗) ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(.r‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗)) ∈ {𝑥 ∣ 𝜓}))) |
147 | 146 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → ((𝑖(.r‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗) ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ ((𝑖(.r‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗) ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘(𝑖(.r‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗)) ∈ {𝑥 ∣ 𝜓}))) |
148 | 119, 144,
147 | mpbir2and 959 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (𝑖(.r‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗) ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓})) |
149 | 148 | adantlr 747 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) ∧ (𝑖 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ∧ 𝑗 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}))) → (𝑖(.r‘(𝐼 mPoly (𝑆 ↾s 𝑅)))𝑗) ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓})) |
150 | 7 | mplassa 19275 |
. . . . . . . . . . . . . 14
⊢ ((𝐼 ∈ V ∧ (𝑆 ↾s 𝑅) ∈ CRing) → (𝐼 mPoly (𝑆 ↾s 𝑅)) ∈ AssAlg) |
151 | 30, 34, 150 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐼 mPoly (𝑆 ↾s 𝑅)) ∈ AssAlg) |
152 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(Scalar‘(𝐼
mPoly (𝑆
↾s 𝑅))) =
(Scalar‘(𝐼 mPoly
(𝑆 ↾s
𝑅))) |
153 | 29, 152 | asclrhm 19163 |
. . . . . . . . . . . . 13
⊢ ((𝐼 mPoly (𝑆 ↾s 𝑅)) ∈ AssAlg → (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅))) ∈ ((Scalar‘(𝐼 mPoly (𝑆 ↾s 𝑅))) RingHom (𝐼 mPoly (𝑆 ↾s 𝑅)))) |
154 | 151, 153 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅))) ∈ ((Scalar‘(𝐼 mPoly (𝑆 ↾s 𝑅))) RingHom (𝐼 mPoly (𝑆 ↾s 𝑅)))) |
155 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(Base‘(Scalar‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) = (Base‘(Scalar‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) |
156 | 155, 13 | rhmf 18549 |
. . . . . . . . . . . 12
⊢
((algSc‘(𝐼
mPoly (𝑆
↾s 𝑅)))
∈ ((Scalar‘(𝐼
mPoly (𝑆
↾s 𝑅)))
RingHom (𝐼 mPoly (𝑆 ↾s 𝑅))) → (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅))):(Base‘(Scalar‘(𝐼 mPoly (𝑆 ↾s 𝑅))))⟶(Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) |
157 | 154, 156 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅))):(Base‘(Scalar‘(𝐼 mPoly (𝑆 ↾s 𝑅))))⟶(Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) |
158 | 157 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (Base‘(𝑆 ↾s 𝑅))) → (algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅))):(Base‘(Scalar‘(𝐼 mPoly (𝑆 ↾s 𝑅))))⟶(Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) |
159 | 7, 30, 34 | mplsca 19266 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆 ↾s 𝑅) = (Scalar‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) |
160 | 159 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝜑 → (Base‘(𝑆 ↾s 𝑅)) =
(Base‘(Scalar‘(𝐼 mPoly (𝑆 ↾s 𝑅))))) |
161 | 160 | eleq2d 2673 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑖 ∈ (Base‘(𝑆 ↾s 𝑅)) ↔ 𝑖 ∈ (Base‘(Scalar‘(𝐼 mPoly (𝑆 ↾s 𝑅)))))) |
162 | 161 | biimpa 500 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (Base‘(𝑆 ↾s 𝑅))) → 𝑖 ∈ (Base‘(Scalar‘(𝐼 mPoly (𝑆 ↾s 𝑅))))) |
163 | 158, 162 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (Base‘(𝑆 ↾s 𝑅))) → ((algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))‘𝑖) ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) |
164 | 30 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (Base‘(𝑆 ↾s 𝑅))) → 𝐼 ∈ V) |
165 | 31 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (Base‘(𝑆 ↾s 𝑅))) → 𝑆 ∈ CRing) |
166 | 32 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (Base‘(𝑆 ↾s 𝑅))) → 𝑅 ∈ (SubRing‘𝑆)) |
167 | 10 | subrgss 18604 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ (SubRing‘𝑆) → 𝑅 ⊆ 𝐵) |
168 | 32, 167 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑅 ⊆ 𝐵) |
169 | 8, 10 | ressbas2 15758 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ⊆ 𝐵 → 𝑅 = (Base‘(𝑆 ↾s 𝑅))) |
170 | 168, 169 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 = (Base‘(𝑆 ↾s 𝑅))) |
171 | 170 | eleq2d 2673 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑖 ∈ 𝑅 ↔ 𝑖 ∈ (Base‘(𝑆 ↾s 𝑅)))) |
172 | 171 | biimpar 501 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (Base‘(𝑆 ↾s 𝑅))) → 𝑖 ∈ 𝑅) |
173 | 6, 7, 8, 10, 29, 164, 165, 166, 172 | evlssca 19343 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (Base‘(𝑆 ↾s 𝑅))) → (((𝐼 evalSub 𝑆)‘𝑅)‘((algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))‘𝑖)) = ((𝐵 ↑𝑚 𝐼) × {𝑖})) |
174 | | mpfind.co |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑅) → 𝜒) |
175 | 174 | ralrimiva 2949 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑓 ∈ 𝑅 𝜒) |
176 | | snex 4835 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑓} ∈ V |
177 | 61, 176 | xpex 6860 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ↑𝑚
𝐼) × {𝑓}) ∈ V |
178 | | mpfind.wa |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = ((𝐵 ↑𝑚 𝐼) × {𝑓}) → (𝜓 ↔ 𝜒)) |
179 | 177, 178 | elab 3319 |
. . . . . . . . . . . . . . 15
⊢ (((𝐵 ↑𝑚
𝐼) × {𝑓}) ∈ {𝑥 ∣ 𝜓} ↔ 𝜒) |
180 | | sneq 4135 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = 𝑖 → {𝑓} = {𝑖}) |
181 | 180 | xpeq2d 5063 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = 𝑖 → ((𝐵 ↑𝑚 𝐼) × {𝑓}) = ((𝐵 ↑𝑚 𝐼) × {𝑖})) |
182 | 181 | eleq1d 2672 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 𝑖 → (((𝐵 ↑𝑚 𝐼) × {𝑓}) ∈ {𝑥 ∣ 𝜓} ↔ ((𝐵 ↑𝑚 𝐼) × {𝑖}) ∈ {𝑥 ∣ 𝜓})) |
183 | 179, 182 | syl5bbr 273 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝑖 → (𝜒 ↔ ((𝐵 ↑𝑚 𝐼) × {𝑖}) ∈ {𝑥 ∣ 𝜓})) |
184 | 183 | cbvralv 3147 |
. . . . . . . . . . . . 13
⊢
(∀𝑓 ∈
𝑅 𝜒 ↔ ∀𝑖 ∈ 𝑅 ((𝐵 ↑𝑚 𝐼) × {𝑖}) ∈ {𝑥 ∣ 𝜓}) |
185 | 175, 184 | sylib 207 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑖 ∈ 𝑅 ((𝐵 ↑𝑚 𝐼) × {𝑖}) ∈ {𝑥 ∣ 𝜓}) |
186 | 185 | r19.21bi 2916 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝑅) → ((𝐵 ↑𝑚 𝐼) × {𝑖}) ∈ {𝑥 ∣ 𝜓}) |
187 | 172, 186 | syldan 486 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (Base‘(𝑆 ↾s 𝑅))) → ((𝐵 ↑𝑚 𝐼) × {𝑖}) ∈ {𝑥 ∣ 𝜓}) |
188 | 173, 187 | eqeltrd 2688 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (Base‘(𝑆 ↾s 𝑅))) → (((𝐼 evalSub 𝑆)‘𝑅)‘((algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))‘𝑖)) ∈ {𝑥 ∣ 𝜓}) |
189 | | elpreima 6245 |
. . . . . . . . . . 11
⊢ (((𝐼 evalSub 𝑆)‘𝑅) Fn (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) → (((algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))‘𝑖) ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ (((algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))‘𝑖) ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘((algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))‘𝑖)) ∈ {𝑥 ∣ 𝜓}))) |
190 | 18, 189 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (((algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))‘𝑖) ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ (((algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))‘𝑖) ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘((algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))‘𝑖)) ∈ {𝑥 ∣ 𝜓}))) |
191 | 190 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (Base‘(𝑆 ↾s 𝑅))) → (((algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))‘𝑖) ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ (((algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))‘𝑖) ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘((algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))‘𝑖)) ∈ {𝑥 ∣ 𝜓}))) |
192 | 163, 188,
191 | mpbir2and 959 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (Base‘(𝑆 ↾s 𝑅))) → ((algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))‘𝑖) ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓})) |
193 | 192 | adantlr 747 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) ∧ 𝑖 ∈ (Base‘(𝑆 ↾s 𝑅))) → ((algSc‘(𝐼 mPoly (𝑆 ↾s 𝑅)))‘𝑖) ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓})) |
194 | 30 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → 𝐼 ∈ V) |
195 | 36 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝑆 ↾s 𝑅) ∈ Ring) |
196 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → 𝑖 ∈ 𝐼) |
197 | 7, 26, 13, 194, 195, 196 | mvrcl 19270 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → ((𝐼 mVar (𝑆 ↾s 𝑅))‘𝑖) ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) |
198 | 31 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → 𝑆 ∈ CRing) |
199 | 32 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → 𝑅 ∈ (SubRing‘𝑆)) |
200 | 6, 26, 8, 10, 194, 198, 199, 196 | evlsvar 19344 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (((𝐼 evalSub 𝑆)‘𝑅)‘((𝐼 mVar (𝑆 ↾s 𝑅))‘𝑖)) = (𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑖))) |
201 | | mpfind.pr |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐼) → 𝜃) |
202 | 61 | mptex 6390 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑓)) ∈ V |
203 | | mpfind.wb |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑓)) → (𝜓 ↔ 𝜃)) |
204 | 202, 203 | elab 3319 |
. . . . . . . . . . . . . 14
⊢ ((𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑓)) ∈ {𝑥 ∣ 𝜓} ↔ 𝜃) |
205 | 201, 204 | sylibr 223 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐼) → (𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑓)) ∈ {𝑥 ∣ 𝜓}) |
206 | 205 | ralrimiva 2949 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑓 ∈ 𝐼 (𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑓)) ∈ {𝑥 ∣ 𝜓}) |
207 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 𝑖 → (𝑔‘𝑓) = (𝑔‘𝑖)) |
208 | 207 | mpteq2dv 4673 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝑖 → (𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑓)) = (𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑖))) |
209 | 208 | eleq1d 2672 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝑖 → ((𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑓)) ∈ {𝑥 ∣ 𝜓} ↔ (𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑖)) ∈ {𝑥 ∣ 𝜓})) |
210 | 209 | cbvralv 3147 |
. . . . . . . . . . . 12
⊢
(∀𝑓 ∈
𝐼 (𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑓)) ∈ {𝑥 ∣ 𝜓} ↔ ∀𝑖 ∈ 𝐼 (𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑖)) ∈ {𝑥 ∣ 𝜓}) |
211 | 206, 210 | sylib 207 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑖 ∈ 𝐼 (𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑖)) ∈ {𝑥 ∣ 𝜓}) |
212 | 211 | r19.21bi 2916 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝑔 ∈ (𝐵 ↑𝑚 𝐼) ↦ (𝑔‘𝑖)) ∈ {𝑥 ∣ 𝜓}) |
213 | 200, 212 | eqeltrd 2688 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (((𝐼 evalSub 𝑆)‘𝑅)‘((𝐼 mVar (𝑆 ↾s 𝑅))‘𝑖)) ∈ {𝑥 ∣ 𝜓}) |
214 | | elpreima 6245 |
. . . . . . . . . . 11
⊢ (((𝐼 evalSub 𝑆)‘𝑅) Fn (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) → (((𝐼 mVar (𝑆 ↾s 𝑅))‘𝑖) ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ (((𝐼 mVar (𝑆 ↾s 𝑅))‘𝑖) ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘((𝐼 mVar (𝑆 ↾s 𝑅))‘𝑖)) ∈ {𝑥 ∣ 𝜓}))) |
215 | 18, 214 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐼 mVar (𝑆 ↾s 𝑅))‘𝑖) ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ (((𝐼 mVar (𝑆 ↾s 𝑅))‘𝑖) ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘((𝐼 mVar (𝑆 ↾s 𝑅))‘𝑖)) ∈ {𝑥 ∣ 𝜓}))) |
216 | 215 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (((𝐼 mVar (𝑆 ↾s 𝑅))‘𝑖) ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓}) ↔ (((𝐼 mVar (𝑆 ↾s 𝑅))‘𝑖) ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅))) ∧ (((𝐼 evalSub 𝑆)‘𝑅)‘((𝐼 mVar (𝑆 ↾s 𝑅))‘𝑖)) ∈ {𝑥 ∣ 𝜓}))) |
217 | 197, 213,
216 | mpbir2and 959 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → ((𝐼 mVar (𝑆 ↾s 𝑅))‘𝑖) ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓})) |
218 | 217 | adantlr 747 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) ∧ 𝑖 ∈ 𝐼) → ((𝐼 mVar (𝑆 ↾s 𝑅))‘𝑖) ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓})) |
219 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) → 𝑦 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) |
220 | 30 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) → 𝐼 ∈ V) |
221 | 34 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) → (𝑆 ↾s 𝑅) ∈ CRing) |
222 | 25, 26, 7, 27, 28, 29, 13, 117, 149, 193, 218, 219, 220, 221 | mplind 19323 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) → 𝑦 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓})) |
223 | | fvimacnvi 6239 |
. . . . . 6
⊢ ((Fun
((𝐼 evalSub 𝑆)‘𝑅) ∧ 𝑦 ∈ (◡((𝐼 evalSub 𝑆)‘𝑅) “ {𝑥 ∣ 𝜓})) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑦) ∈ {𝑥 ∣ 𝜓}) |
224 | 24, 222, 223 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) → (((𝐼 evalSub 𝑆)‘𝑅)‘𝑦) ∈ {𝑥 ∣ 𝜓}) |
225 | | eleq1 2676 |
. . . . 5
⊢ ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑦) = 𝐴 → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑦) ∈ {𝑥 ∣ 𝜓} ↔ 𝐴 ∈ {𝑥 ∣ 𝜓})) |
226 | 224, 225 | syl5ibcom 234 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))) → ((((𝐼 evalSub 𝑆)‘𝑅)‘𝑦) = 𝐴 → 𝐴 ∈ {𝑥 ∣ 𝜓})) |
227 | 226 | rexlimdva 3013 |
. . 3
⊢ (𝜑 → (∃𝑦 ∈ (Base‘(𝐼 mPoly (𝑆 ↾s 𝑅)))(((𝐼 evalSub 𝑆)‘𝑅)‘𝑦) = 𝐴 → 𝐴 ∈ {𝑥 ∣ 𝜓})) |
228 | 21, 227 | mpd 15 |
. 2
⊢ (𝜑 → 𝐴 ∈ {𝑥 ∣ 𝜓}) |
229 | | mpfind.wg |
. . . 4
⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜌)) |
230 | 229 | elabg 3320 |
. . 3
⊢ (𝐴 ∈ 𝑄 → (𝐴 ∈ {𝑥 ∣ 𝜓} ↔ 𝜌)) |
231 | 1, 230 | syl 17 |
. 2
⊢ (𝜑 → (𝐴 ∈ {𝑥 ∣ 𝜓} ↔ 𝜌)) |
232 | 228, 231 | mpbid 221 |
1
⊢ (𝜑 → 𝜌) |