Step | Hyp | Ref
| Expression |
1 | | elfvex 6131 |
. . . 4
⊢ (𝐴 ∈ (mzPoly‘𝑉) → 𝑉 ∈ V) |
2 | 1 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ (mzPoly‘𝑉)) → 𝑉 ∈ V) |
3 | | mzpval 36313 |
. . . . . . 7
⊢ (𝑉 ∈ V →
(mzPoly‘𝑉) = ∩ (mzPolyCld‘𝑉)) |
4 | 3 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑉 ∈ V) → (mzPoly‘𝑉) = ∩
(mzPolyCld‘𝑉)) |
5 | | ssrab2 3650 |
. . . . . . . . . 10
⊢ {𝑥 ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ∣ 𝜓} ⊆ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) |
6 | 5 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑉 ∈ V) → {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓} ⊆ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉))) |
7 | | ovex 6577 |
. . . . . . . . . . . . . . 15
⊢ (ℤ
↑𝑚 𝑉) ∈ V |
8 | | zex 11263 |
. . . . . . . . . . . . . . 15
⊢ ℤ
∈ V |
9 | 7, 8 | constmap 36294 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ ℤ → ((ℤ
↑𝑚 𝑉) × {𝑓}) ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉))) |
10 | 9 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ ℤ) → ((ℤ
↑𝑚 𝑉) × {𝑓}) ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉))) |
11 | | mzpindd.co |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ ℤ) → 𝜒) |
12 | | mzpindd.1 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ((ℤ
↑𝑚 𝑉) × {𝑓}) → (𝜓 ↔ 𝜒)) |
13 | 12 | elrab 3331 |
. . . . . . . . . . . . 13
⊢
(((ℤ ↑𝑚 𝑉) × {𝑓}) ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓} ↔ (((ℤ
↑𝑚 𝑉) × {𝑓}) ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∧ 𝜒)) |
14 | 10, 11, 13 | sylanbrc 695 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ ℤ) → ((ℤ
↑𝑚 𝑉) × {𝑓}) ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓}) |
15 | 14 | ralrimiva 2949 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑓 ∈ ℤ ((ℤ
↑𝑚 𝑉) × {𝑓}) ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓}) |
16 | 15 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑉 ∈ V) → ∀𝑓 ∈ ℤ ((ℤ
↑𝑚 𝑉) × {𝑓}) ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓}) |
17 | 8 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑉 ∈ V) ∧ 𝑓 ∈ 𝑉) ∧ 𝑔 ∈ (ℤ ↑𝑚
𝑉)) → ℤ ∈
V) |
18 | | simpllr 795 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑉 ∈ V) ∧ 𝑓 ∈ 𝑉) ∧ 𝑔 ∈ (ℤ ↑𝑚
𝑉)) → 𝑉 ∈ V) |
19 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑉 ∈ V) ∧ 𝑓 ∈ 𝑉) ∧ 𝑔 ∈ (ℤ ↑𝑚
𝑉)) → 𝑔 ∈ (ℤ
↑𝑚 𝑉)) |
20 | | elmapg 7757 |
. . . . . . . . . . . . . . . . 17
⊢ ((ℤ
∈ V ∧ 𝑉 ∈ V)
→ (𝑔 ∈ (ℤ
↑𝑚 𝑉) ↔ 𝑔:𝑉⟶ℤ)) |
21 | 20 | biimpa 500 |
. . . . . . . . . . . . . . . 16
⊢
(((ℤ ∈ V ∧ 𝑉 ∈ V) ∧ 𝑔 ∈ (ℤ ↑𝑚
𝑉)) → 𝑔:𝑉⟶ℤ) |
22 | 17, 18, 19, 21 | syl21anc 1317 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑉 ∈ V) ∧ 𝑓 ∈ 𝑉) ∧ 𝑔 ∈ (ℤ ↑𝑚
𝑉)) → 𝑔:𝑉⟶ℤ) |
23 | | simplr 788 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑉 ∈ V) ∧ 𝑓 ∈ 𝑉) ∧ 𝑔 ∈ (ℤ ↑𝑚
𝑉)) → 𝑓 ∈ 𝑉) |
24 | 22, 23 | ffvelrnd 6268 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑉 ∈ V) ∧ 𝑓 ∈ 𝑉) ∧ 𝑔 ∈ (ℤ ↑𝑚
𝑉)) → (𝑔‘𝑓) ∈ ℤ) |
25 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ (ℤ
↑𝑚 𝑉) ↦ (𝑔‘𝑓)) = (𝑔 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑔‘𝑓)) |
26 | 24, 25 | fmptd 6292 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑉 ∈ V) ∧ 𝑓 ∈ 𝑉) → (𝑔 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑔‘𝑓)):(ℤ ↑𝑚 𝑉)⟶ℤ) |
27 | 8, 7 | elmap 7772 |
. . . . . . . . . . . . 13
⊢ ((𝑔 ∈ (ℤ
↑𝑚 𝑉) ↦ (𝑔‘𝑓)) ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ↔ (𝑔 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑔‘𝑓)):(ℤ ↑𝑚 𝑉)⟶ℤ) |
28 | 26, 27 | sylibr 223 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑉 ∈ V) ∧ 𝑓 ∈ 𝑉) → (𝑔 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑔‘𝑓)) ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉))) |
29 | | mzpindd.pr |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑉) → 𝜃) |
30 | 29 | adantlr 747 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑉 ∈ V) ∧ 𝑓 ∈ 𝑉) → 𝜃) |
31 | | mzpindd.2 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑔 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑔‘𝑓)) → (𝜓 ↔ 𝜃)) |
32 | 31 | elrab 3331 |
. . . . . . . . . . . 12
⊢ ((𝑔 ∈ (ℤ
↑𝑚 𝑉) ↦ (𝑔‘𝑓)) ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓} ↔ ((𝑔 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑔‘𝑓)) ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∧ 𝜃)) |
33 | 28, 30, 32 | sylanbrc 695 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑉 ∈ V) ∧ 𝑓 ∈ 𝑉) → (𝑔 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑔‘𝑓)) ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓}) |
34 | 33 | ralrimiva 2949 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑉 ∈ V) → ∀𝑓 ∈ 𝑉 (𝑔 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑔‘𝑓)) ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓}) |
35 | 16, 34 | jca 553 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑉 ∈ V) → (∀𝑓 ∈ ℤ ((ℤ
↑𝑚 𝑉) × {𝑓}) ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓} ∧ ∀𝑓 ∈ 𝑉 (𝑔 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑔‘𝑓)) ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓})) |
36 | | zaddcl 11294 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (𝑎 + 𝑏) ∈ ℤ) |
37 | 36 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑓:(ℤ
↑𝑚 𝑉)⟶ℤ ∧ 𝑔:(ℤ ↑𝑚 𝑉)⟶ℤ) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑎 + 𝑏) ∈ ℤ) |
38 | | simpl 472 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:(ℤ
↑𝑚 𝑉)⟶ℤ ∧ 𝑔:(ℤ ↑𝑚 𝑉)⟶ℤ) → 𝑓:(ℤ
↑𝑚 𝑉)⟶ℤ) |
39 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:(ℤ
↑𝑚 𝑉)⟶ℤ ∧ 𝑔:(ℤ ↑𝑚 𝑉)⟶ℤ) → 𝑔:(ℤ
↑𝑚 𝑉)⟶ℤ) |
40 | 7 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:(ℤ
↑𝑚 𝑉)⟶ℤ ∧ 𝑔:(ℤ ↑𝑚 𝑉)⟶ℤ) →
(ℤ ↑𝑚 𝑉) ∈ V) |
41 | | inidm 3784 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((ℤ
↑𝑚 𝑉) ∩ (ℤ ↑𝑚
𝑉)) = (ℤ
↑𝑚 𝑉) |
42 | 37, 38, 39, 40, 40, 41 | off 6810 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:(ℤ
↑𝑚 𝑉)⟶ℤ ∧ 𝑔:(ℤ ↑𝑚 𝑉)⟶ℤ) → (𝑓 ∘𝑓 +
𝑔):(ℤ
↑𝑚 𝑉)⟶ℤ) |
43 | 42 | ad2ant2r 779 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑓:(ℤ
↑𝑚 𝑉)⟶ℤ ∧ 𝜏) ∧ (𝑔:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝜂)) → (𝑓 ∘𝑓 + 𝑔):(ℤ
↑𝑚 𝑉)⟶ℤ) |
44 | 43 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑓:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝜏) ∧ (𝑔:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝜂))) → (𝑓 ∘𝑓 + 𝑔):(ℤ
↑𝑚 𝑉)⟶ℤ) |
45 | | mzpindd.ad |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑓:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝜏) ∧ (𝑔:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝜂)) → 𝜁) |
46 | 45 | 3expb 1258 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑓:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝜏) ∧ (𝑔:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝜂))) → 𝜁) |
47 | 44, 46 | jca 553 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑓:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝜏) ∧ (𝑔:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝜂))) → ((𝑓 ∘𝑓 + 𝑔):(ℤ
↑𝑚 𝑉)⟶ℤ ∧ 𝜁)) |
48 | | zmulcl 11303 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (𝑎 · 𝑏) ∈ ℤ) |
49 | 48 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑓:(ℤ
↑𝑚 𝑉)⟶ℤ ∧ 𝑔:(ℤ ↑𝑚 𝑉)⟶ℤ) ∧ (𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ)) → (𝑎 · 𝑏) ∈ ℤ) |
50 | 49, 38, 39, 40, 40, 41 | off 6810 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓:(ℤ
↑𝑚 𝑉)⟶ℤ ∧ 𝑔:(ℤ ↑𝑚 𝑉)⟶ℤ) → (𝑓 ∘𝑓
· 𝑔):(ℤ
↑𝑚 𝑉)⟶ℤ) |
51 | 50 | ad2ant2r 779 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓:(ℤ
↑𝑚 𝑉)⟶ℤ ∧ 𝜏) ∧ (𝑔:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝜂)) → (𝑓 ∘𝑓 · 𝑔):(ℤ
↑𝑚 𝑉)⟶ℤ) |
52 | 51 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑓:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝜏) ∧ (𝑔:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝜂))) → (𝑓 ∘𝑓 · 𝑔):(ℤ
↑𝑚 𝑉)⟶ℤ) |
53 | | mzpindd.mu |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑓:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝜏) ∧ (𝑔:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝜂)) → 𝜎) |
54 | 53 | 3expb 1258 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑓:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝜏) ∧ (𝑔:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝜂))) → 𝜎) |
55 | 47, 52, 54 | jca32 556 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑓:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝜏) ∧ (𝑔:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝜂))) → (((𝑓 ∘𝑓 + 𝑔):(ℤ
↑𝑚 𝑉)⟶ℤ ∧ 𝜁) ∧ ((𝑓 ∘𝑓 · 𝑔):(ℤ
↑𝑚 𝑉)⟶ℤ ∧ 𝜎))) |
56 | 55 | ex 449 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑓:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝜏) ∧ (𝑔:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝜂)) → (((𝑓 ∘𝑓 + 𝑔):(ℤ
↑𝑚 𝑉)⟶ℤ ∧ 𝜁) ∧ ((𝑓 ∘𝑓 · 𝑔):(ℤ
↑𝑚 𝑉)⟶ℤ ∧ 𝜎)))) |
57 | 8, 7 | elmap 7772 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ↔ 𝑓:(ℤ ↑𝑚 𝑉)⟶ℤ) |
58 | 57 | anbi1i 727 |
. . . . . . . . . . . . . 14
⊢ ((𝑓 ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ∧ 𝜏) ↔ (𝑓:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝜏)) |
59 | 8, 7 | elmap 7772 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ↔ 𝑔:(ℤ ↑𝑚 𝑉)⟶ℤ) |
60 | 59 | anbi1i 727 |
. . . . . . . . . . . . . 14
⊢ ((𝑔 ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ∧ 𝜂) ↔ (𝑔:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝜂)) |
61 | 58, 60 | anbi12i 729 |
. . . . . . . . . . . . 13
⊢ (((𝑓 ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ∧ 𝜏) ∧ (𝑔 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∧ 𝜂)) ↔ ((𝑓:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝜏) ∧ (𝑔:(ℤ ↑𝑚 𝑉)⟶ℤ ∧ 𝜂))) |
62 | 8, 7 | elmap 7772 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∘𝑓 +
𝑔) ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ↔ (𝑓 ∘𝑓 + 𝑔):(ℤ
↑𝑚 𝑉)⟶ℤ) |
63 | 62 | anbi1i 727 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 ∘𝑓 +
𝑔) ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ∧ 𝜁) ↔ ((𝑓 ∘𝑓 + 𝑔):(ℤ
↑𝑚 𝑉)⟶ℤ ∧ 𝜁)) |
64 | 8, 7 | elmap 7772 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∘𝑓
· 𝑔) ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ↔ (𝑓 ∘𝑓 · 𝑔):(ℤ
↑𝑚 𝑉)⟶ℤ) |
65 | 64 | anbi1i 727 |
. . . . . . . . . . . . . 14
⊢ (((𝑓 ∘𝑓
· 𝑔) ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ∧ 𝜎) ↔ ((𝑓 ∘𝑓 · 𝑔):(ℤ
↑𝑚 𝑉)⟶ℤ ∧ 𝜎)) |
66 | 63, 65 | anbi12i 729 |
. . . . . . . . . . . . 13
⊢ ((((𝑓 ∘𝑓 +
𝑔) ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ∧ 𝜁) ∧ ((𝑓 ∘𝑓 · 𝑔) ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ∧ 𝜎)) ↔ (((𝑓 ∘𝑓 + 𝑔):(ℤ
↑𝑚 𝑉)⟶ℤ ∧ 𝜁) ∧ ((𝑓 ∘𝑓 · 𝑔):(ℤ
↑𝑚 𝑉)⟶ℤ ∧ 𝜎))) |
67 | 56, 61, 66 | 3imtr4g 284 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑓 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∧ 𝜏) ∧ (𝑔 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∧ 𝜂)) → (((𝑓 ∘𝑓 + 𝑔) ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ∧ 𝜁) ∧ ((𝑓 ∘𝑓 · 𝑔) ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ∧ 𝜎)))) |
68 | | mzpindd.3 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑓 → (𝜓 ↔ 𝜏)) |
69 | 68 | elrab 3331 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓} ↔ (𝑓 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∧ 𝜏)) |
70 | | mzpindd.4 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑔 → (𝜓 ↔ 𝜂)) |
71 | 70 | elrab 3331 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓} ↔ (𝑔 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∧ 𝜂)) |
72 | 69, 71 | anbi12i 729 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓} ∧ 𝑔 ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓}) ↔ ((𝑓 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∧ 𝜏) ∧ (𝑔 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∧ 𝜂))) |
73 | | mzpindd.5 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑓 ∘𝑓 + 𝑔) → (𝜓 ↔ 𝜁)) |
74 | 73 | elrab 3331 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∘𝑓 +
𝑔) ∈ {𝑥 ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ∣ 𝜓} ↔ ((𝑓 ∘𝑓 + 𝑔) ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ∧ 𝜁)) |
75 | | mzpindd.6 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝑓 ∘𝑓 · 𝑔) → (𝜓 ↔ 𝜎)) |
76 | 75 | elrab 3331 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∘𝑓
· 𝑔) ∈ {𝑥 ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ∣ 𝜓} ↔ ((𝑓 ∘𝑓 · 𝑔) ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ∧ 𝜎)) |
77 | 74, 76 | anbi12i 729 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∘𝑓 +
𝑔) ∈ {𝑥 ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ∣ 𝜓} ∧ (𝑓 ∘𝑓 · 𝑔) ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓}) ↔ (((𝑓 ∘𝑓 + 𝑔) ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ∧ 𝜁) ∧ ((𝑓 ∘𝑓 · 𝑔) ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ∧ 𝜎))) |
78 | 67, 72, 77 | 3imtr4g 284 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑓 ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓} ∧ 𝑔 ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓}) → ((𝑓 ∘𝑓 + 𝑔) ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓} ∧ (𝑓 ∘𝑓 · 𝑔) ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓}))) |
79 | 78 | ralrimivv 2953 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑓 ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓}∀𝑔 ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓} ((𝑓 ∘𝑓 + 𝑔) ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓} ∧ (𝑓 ∘𝑓 · 𝑔) ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓})) |
80 | 79 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑉 ∈ V) → ∀𝑓 ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓}∀𝑔 ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓} ((𝑓 ∘𝑓 + 𝑔) ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓} ∧ (𝑓 ∘𝑓 · 𝑔) ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓})) |
81 | 6, 35, 80 | jca32 556 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑉 ∈ V) → ({𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓} ⊆ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ∧ ((∀𝑓 ∈ ℤ ((ℤ
↑𝑚 𝑉) × {𝑓}) ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓} ∧ ∀𝑓 ∈ 𝑉 (𝑔 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑔‘𝑓)) ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓}) ∧ ∀𝑓 ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓}∀𝑔 ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓} ((𝑓 ∘𝑓 + 𝑔) ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓} ∧ (𝑓 ∘𝑓 · 𝑔) ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓})))) |
82 | | elmzpcl 36307 |
. . . . . . . . 9
⊢ (𝑉 ∈ V → ({𝑥 ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ∣ 𝜓} ∈ (mzPolyCld‘𝑉) ↔ ({𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓} ⊆ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ∧ ((∀𝑓 ∈ ℤ ((ℤ
↑𝑚 𝑉) × {𝑓}) ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓} ∧ ∀𝑓 ∈ 𝑉 (𝑔 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑔‘𝑓)) ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓}) ∧ ∀𝑓 ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓}∀𝑔 ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓} ((𝑓 ∘𝑓 + 𝑔) ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓} ∧ (𝑓 ∘𝑓 · 𝑔) ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓}))))) |
83 | 82 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑉 ∈ V) → ({𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓} ∈ (mzPolyCld‘𝑉) ↔ ({𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓} ⊆ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ∧ ((∀𝑓 ∈ ℤ ((ℤ
↑𝑚 𝑉) × {𝑓}) ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓} ∧ ∀𝑓 ∈ 𝑉 (𝑔 ∈ (ℤ ↑𝑚
𝑉) ↦ (𝑔‘𝑓)) ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓}) ∧ ∀𝑓 ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓}∀𝑔 ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓} ((𝑓 ∘𝑓 + 𝑔) ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓} ∧ (𝑓 ∘𝑓 · 𝑔) ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓}))))) |
84 | 81, 83 | mpbird 246 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑉 ∈ V) → {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓} ∈ (mzPolyCld‘𝑉)) |
85 | | intss1 4427 |
. . . . . . 7
⊢ ({𝑥 ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ∣ 𝜓} ∈ (mzPolyCld‘𝑉) → ∩
(mzPolyCld‘𝑉) ⊆
{𝑥 ∈ (ℤ
↑𝑚 (ℤ ↑𝑚 𝑉)) ∣ 𝜓}) |
86 | 84, 85 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑉 ∈ V) → ∩ (mzPolyCld‘𝑉) ⊆ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓}) |
87 | 4, 86 | eqsstrd 3602 |
. . . . 5
⊢ ((𝜑 ∧ 𝑉 ∈ V) → (mzPoly‘𝑉) ⊆ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓}) |
88 | 87 | sselda 3568 |
. . . 4
⊢ (((𝜑 ∧ 𝑉 ∈ V) ∧ 𝐴 ∈ (mzPoly‘𝑉)) → 𝐴 ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓}) |
89 | 88 | an32s 842 |
. . 3
⊢ (((𝜑 ∧ 𝐴 ∈ (mzPoly‘𝑉)) ∧ 𝑉 ∈ V) → 𝐴 ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓}) |
90 | 2, 89 | mpdan 699 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ (mzPoly‘𝑉)) → 𝐴 ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓}) |
91 | | mzpindd.7 |
. . . 4
⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜌)) |
92 | 91 | elrab 3331 |
. . 3
⊢ (𝐴 ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓} ↔ (𝐴 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∧ 𝜌)) |
93 | 92 | simprbi 479 |
. 2
⊢ (𝐴 ∈ {𝑥 ∈ (ℤ ↑𝑚
(ℤ ↑𝑚 𝑉)) ∣ 𝜓} → 𝜌) |
94 | 90, 93 | syl 17 |
1
⊢ ((𝜑 ∧ 𝐴 ∈ (mzPoly‘𝑉)) → 𝜌) |