Step | Hyp | Ref
| Expression |
1 | | coe1fzgsumd.m |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝑁 𝑀 ∈ 𝐵) |
2 | | coe1fzgsumd.n |
. . 3
⊢ (𝜑 → 𝑁 ∈ Fin) |
3 | | raleq 3321 |
. . . . . . 7
⊢ (𝑛 = ∅ → (∀𝑥 ∈ 𝑛 𝑀 ∈ 𝐵 ↔ ∀𝑥 ∈ ∅ 𝑀 ∈ 𝐵)) |
4 | 3 | anbi2d 632 |
. . . . . 6
⊢ (𝑛 = ∅ → ((𝜑 ∧ ∀𝑥 ∈ 𝑛 𝑀 ∈ 𝐵) ↔ (𝜑 ∧ ∀𝑥 ∈ ∅ 𝑀 ∈ 𝐵))) |
5 | | mpteq1 5113 |
. . . . . . . . . 10
⊢ (𝑛 = ∅ → (𝑥 ∈ 𝑛 ↦ 𝑀) = (𝑥 ∈ ∅ ↦ 𝑀)) |
6 | 5 | oveq2d 7159 |
. . . . . . . . 9
⊢ (𝑛 = ∅ → (𝑃 Σg
(𝑥 ∈ 𝑛 ↦ 𝑀)) = (𝑃 Σg (𝑥 ∈ ∅ ↦ 𝑀))) |
7 | 6 | fveq2d 6655 |
. . . . . . . 8
⊢ (𝑛 = ∅ →
(coe1‘(𝑃
Σg (𝑥 ∈ 𝑛 ↦ 𝑀))) = (coe1‘(𝑃 Σg
(𝑥 ∈ ∅ ↦
𝑀)))) |
8 | 7 | fveq1d 6653 |
. . . . . . 7
⊢ (𝑛 = ∅ →
((coe1‘(𝑃
Σg (𝑥 ∈ 𝑛 ↦ 𝑀)))‘𝐾) = ((coe1‘(𝑃 Σg
(𝑥 ∈ ∅ ↦
𝑀)))‘𝐾)) |
9 | | mpteq1 5113 |
. . . . . . . 8
⊢ (𝑛 = ∅ → (𝑥 ∈ 𝑛 ↦ ((coe1‘𝑀)‘𝐾)) = (𝑥 ∈ ∅ ↦
((coe1‘𝑀)‘𝐾))) |
10 | 9 | oveq2d 7159 |
. . . . . . 7
⊢ (𝑛 = ∅ → (𝑅 Σg
(𝑥 ∈ 𝑛 ↦
((coe1‘𝑀)‘𝐾))) = (𝑅 Σg (𝑥 ∈ ∅ ↦
((coe1‘𝑀)‘𝐾)))) |
11 | 8, 10 | eqeq12d 2775 |
. . . . . 6
⊢ (𝑛 = ∅ →
(((coe1‘(𝑃
Σg (𝑥 ∈ 𝑛 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑛 ↦ ((coe1‘𝑀)‘𝐾))) ↔ ((coe1‘(𝑃 Σg
(𝑥 ∈ ∅ ↦
𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ ∅ ↦
((coe1‘𝑀)‘𝐾))))) |
12 | 4, 11 | imbi12d 349 |
. . . . 5
⊢ (𝑛 = ∅ → (((𝜑 ∧ ∀𝑥 ∈ 𝑛 𝑀 ∈ 𝐵) → ((coe1‘(𝑃 Σg
(𝑥 ∈ 𝑛 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑛 ↦ ((coe1‘𝑀)‘𝐾)))) ↔ ((𝜑 ∧ ∀𝑥 ∈ ∅ 𝑀 ∈ 𝐵) → ((coe1‘(𝑃 Σg
(𝑥 ∈ ∅ ↦
𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ ∅ ↦
((coe1‘𝑀)‘𝐾)))))) |
13 | | raleq 3321 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (∀𝑥 ∈ 𝑛 𝑀 ∈ 𝐵 ↔ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵)) |
14 | 13 | anbi2d 632 |
. . . . . 6
⊢ (𝑛 = 𝑚 → ((𝜑 ∧ ∀𝑥 ∈ 𝑛 𝑀 ∈ 𝐵) ↔ (𝜑 ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵))) |
15 | | mpteq1 5113 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑚 → (𝑥 ∈ 𝑛 ↦ 𝑀) = (𝑥 ∈ 𝑚 ↦ 𝑀)) |
16 | 15 | oveq2d 7159 |
. . . . . . . . 9
⊢ (𝑛 = 𝑚 → (𝑃 Σg (𝑥 ∈ 𝑛 ↦ 𝑀)) = (𝑃 Σg (𝑥 ∈ 𝑚 ↦ 𝑀))) |
17 | 16 | fveq2d 6655 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → (coe1‘(𝑃 Σg
(𝑥 ∈ 𝑛 ↦ 𝑀))) = (coe1‘(𝑃 Σg
(𝑥 ∈ 𝑚 ↦ 𝑀)))) |
18 | 17 | fveq1d 6653 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → ((coe1‘(𝑃 Σg
(𝑥 ∈ 𝑛 ↦ 𝑀)))‘𝐾) = ((coe1‘(𝑃 Σg
(𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝐾)) |
19 | | mpteq1 5113 |
. . . . . . . 8
⊢ (𝑛 = 𝑚 → (𝑥 ∈ 𝑛 ↦ ((coe1‘𝑀)‘𝐾)) = (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾))) |
20 | 19 | oveq2d 7159 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (𝑅 Σg (𝑥 ∈ 𝑛 ↦ ((coe1‘𝑀)‘𝐾))) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾)))) |
21 | 18, 20 | eqeq12d 2775 |
. . . . . 6
⊢ (𝑛 = 𝑚 → (((coe1‘(𝑃 Σg
(𝑥 ∈ 𝑛 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑛 ↦ ((coe1‘𝑀)‘𝐾))) ↔ ((coe1‘(𝑃 Σg
(𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾))))) |
22 | 14, 21 | imbi12d 349 |
. . . . 5
⊢ (𝑛 = 𝑚 → (((𝜑 ∧ ∀𝑥 ∈ 𝑛 𝑀 ∈ 𝐵) → ((coe1‘(𝑃 Σg
(𝑥 ∈ 𝑛 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑛 ↦ ((coe1‘𝑀)‘𝐾)))) ↔ ((𝜑 ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) → ((coe1‘(𝑃 Σg
(𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾)))))) |
23 | | raleq 3321 |
. . . . . . 7
⊢ (𝑛 = (𝑚 ∪ {𝑎}) → (∀𝑥 ∈ 𝑛 𝑀 ∈ 𝐵 ↔ ∀𝑥 ∈ (𝑚 ∪ {𝑎})𝑀 ∈ 𝐵)) |
24 | 23 | anbi2d 632 |
. . . . . 6
⊢ (𝑛 = (𝑚 ∪ {𝑎}) → ((𝜑 ∧ ∀𝑥 ∈ 𝑛 𝑀 ∈ 𝐵) ↔ (𝜑 ∧ ∀𝑥 ∈ (𝑚 ∪ {𝑎})𝑀 ∈ 𝐵))) |
25 | | mpteq1 5113 |
. . . . . . . . . 10
⊢ (𝑛 = (𝑚 ∪ {𝑎}) → (𝑥 ∈ 𝑛 ↦ 𝑀) = (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)) |
26 | 25 | oveq2d 7159 |
. . . . . . . . 9
⊢ (𝑛 = (𝑚 ∪ {𝑎}) → (𝑃 Σg (𝑥 ∈ 𝑛 ↦ 𝑀)) = (𝑃 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀))) |
27 | 26 | fveq2d 6655 |
. . . . . . . 8
⊢ (𝑛 = (𝑚 ∪ {𝑎}) → (coe1‘(𝑃 Σg
(𝑥 ∈ 𝑛 ↦ 𝑀))) = (coe1‘(𝑃 Σg
(𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))) |
28 | 27 | fveq1d 6653 |
. . . . . . 7
⊢ (𝑛 = (𝑚 ∪ {𝑎}) → ((coe1‘(𝑃 Σg
(𝑥 ∈ 𝑛 ↦ 𝑀)))‘𝐾) = ((coe1‘(𝑃 Σg
(𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝐾)) |
29 | | mpteq1 5113 |
. . . . . . . 8
⊢ (𝑛 = (𝑚 ∪ {𝑎}) → (𝑥 ∈ 𝑛 ↦ ((coe1‘𝑀)‘𝐾)) = (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((coe1‘𝑀)‘𝐾))) |
30 | 29 | oveq2d 7159 |
. . . . . . 7
⊢ (𝑛 = (𝑚 ∪ {𝑎}) → (𝑅 Σg (𝑥 ∈ 𝑛 ↦ ((coe1‘𝑀)‘𝐾))) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((coe1‘𝑀)‘𝐾)))) |
31 | 28, 30 | eqeq12d 2775 |
. . . . . 6
⊢ (𝑛 = (𝑚 ∪ {𝑎}) → (((coe1‘(𝑃 Σg
(𝑥 ∈ 𝑛 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑛 ↦ ((coe1‘𝑀)‘𝐾))) ↔ ((coe1‘(𝑃 Σg
(𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((coe1‘𝑀)‘𝐾))))) |
32 | 24, 31 | imbi12d 349 |
. . . . 5
⊢ (𝑛 = (𝑚 ∪ {𝑎}) → (((𝜑 ∧ ∀𝑥 ∈ 𝑛 𝑀 ∈ 𝐵) → ((coe1‘(𝑃 Σg
(𝑥 ∈ 𝑛 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑛 ↦ ((coe1‘𝑀)‘𝐾)))) ↔ ((𝜑 ∧ ∀𝑥 ∈ (𝑚 ∪ {𝑎})𝑀 ∈ 𝐵) → ((coe1‘(𝑃 Σg
(𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((coe1‘𝑀)‘𝐾)))))) |
33 | | raleq 3321 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (∀𝑥 ∈ 𝑛 𝑀 ∈ 𝐵 ↔ ∀𝑥 ∈ 𝑁 𝑀 ∈ 𝐵)) |
34 | 33 | anbi2d 632 |
. . . . . 6
⊢ (𝑛 = 𝑁 → ((𝜑 ∧ ∀𝑥 ∈ 𝑛 𝑀 ∈ 𝐵) ↔ (𝜑 ∧ ∀𝑥 ∈ 𝑁 𝑀 ∈ 𝐵))) |
35 | | mpteq1 5113 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑁 → (𝑥 ∈ 𝑛 ↦ 𝑀) = (𝑥 ∈ 𝑁 ↦ 𝑀)) |
36 | 35 | oveq2d 7159 |
. . . . . . . . 9
⊢ (𝑛 = 𝑁 → (𝑃 Σg (𝑥 ∈ 𝑛 ↦ 𝑀)) = (𝑃 Σg (𝑥 ∈ 𝑁 ↦ 𝑀))) |
37 | 36 | fveq2d 6655 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (coe1‘(𝑃 Σg
(𝑥 ∈ 𝑛 ↦ 𝑀))) = (coe1‘(𝑃 Σg
(𝑥 ∈ 𝑁 ↦ 𝑀)))) |
38 | 37 | fveq1d 6653 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → ((coe1‘(𝑃 Σg
(𝑥 ∈ 𝑛 ↦ 𝑀)))‘𝐾) = ((coe1‘(𝑃 Σg
(𝑥 ∈ 𝑁 ↦ 𝑀)))‘𝐾)) |
39 | | mpteq1 5113 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (𝑥 ∈ 𝑛 ↦ ((coe1‘𝑀)‘𝐾)) = (𝑥 ∈ 𝑁 ↦ ((coe1‘𝑀)‘𝐾))) |
40 | 39 | oveq2d 7159 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (𝑅 Σg (𝑥 ∈ 𝑛 ↦ ((coe1‘𝑀)‘𝐾))) = (𝑅 Σg (𝑥 ∈ 𝑁 ↦ ((coe1‘𝑀)‘𝐾)))) |
41 | 38, 40 | eqeq12d 2775 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (((coe1‘(𝑃 Σg
(𝑥 ∈ 𝑛 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑛 ↦ ((coe1‘𝑀)‘𝐾))) ↔ ((coe1‘(𝑃 Σg
(𝑥 ∈ 𝑁 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑁 ↦ ((coe1‘𝑀)‘𝐾))))) |
42 | 34, 41 | imbi12d 349 |
. . . . 5
⊢ (𝑛 = 𝑁 → (((𝜑 ∧ ∀𝑥 ∈ 𝑛 𝑀 ∈ 𝐵) → ((coe1‘(𝑃 Σg
(𝑥 ∈ 𝑛 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑛 ↦ ((coe1‘𝑀)‘𝐾)))) ↔ ((𝜑 ∧ ∀𝑥 ∈ 𝑁 𝑀 ∈ 𝐵) → ((coe1‘(𝑃 Σg
(𝑥 ∈ 𝑁 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑁 ↦ ((coe1‘𝑀)‘𝐾)))))) |
43 | | mpt0 6466 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ∅ ↦ 𝑀) = ∅ |
44 | 43 | oveq2i 7154 |
. . . . . . . . . . . 12
⊢ (𝑃 Σg
(𝑥 ∈ ∅ ↦
𝑀)) = (𝑃 Σg
∅) |
45 | | eqid 2759 |
. . . . . . . . . . . . 13
⊢
(0g‘𝑃) = (0g‘𝑃) |
46 | 45 | gsum0 17945 |
. . . . . . . . . . . 12
⊢ (𝑃 Σg
∅) = (0g‘𝑃) |
47 | 44, 46 | eqtri 2782 |
. . . . . . . . . . 11
⊢ (𝑃 Σg
(𝑥 ∈ ∅ ↦
𝑀)) =
(0g‘𝑃) |
48 | 47 | fveq2i 6654 |
. . . . . . . . . 10
⊢
(coe1‘(𝑃 Σg (𝑥 ∈ ∅ ↦ 𝑀))) =
(coe1‘(0g‘𝑃)) |
49 | 48 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 →
(coe1‘(𝑃
Σg (𝑥 ∈ ∅ ↦ 𝑀))) =
(coe1‘(0g‘𝑃))) |
50 | 49 | fveq1d 6653 |
. . . . . . . 8
⊢ (𝜑 →
((coe1‘(𝑃
Σg (𝑥 ∈ ∅ ↦ 𝑀)))‘𝐾) =
((coe1‘(0g‘𝑃))‘𝐾)) |
51 | | coe1fzgsumd.r |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ Ring) |
52 | | coe1fzgsumd.p |
. . . . . . . . . . 11
⊢ 𝑃 = (Poly1‘𝑅) |
53 | | eqid 2759 |
. . . . . . . . . . 11
⊢
(0g‘𝑅) = (0g‘𝑅) |
54 | 52, 45, 53 | coe1z 20972 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring →
(coe1‘(0g‘𝑃)) = (ℕ0 ×
{(0g‘𝑅)})) |
55 | 51, 54 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 →
(coe1‘(0g‘𝑃)) = (ℕ0 ×
{(0g‘𝑅)})) |
56 | 55 | fveq1d 6653 |
. . . . . . . 8
⊢ (𝜑 →
((coe1‘(0g‘𝑃))‘𝐾) = ((ℕ0 ×
{(0g‘𝑅)})‘𝐾)) |
57 | | fvex 6664 |
. . . . . . . . 9
⊢
(0g‘𝑅) ∈ V |
58 | | coe1fzgsumd.k |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
59 | | fvconst2g 6948 |
. . . . . . . . 9
⊢
(((0g‘𝑅) ∈ V ∧ 𝐾 ∈ ℕ0) →
((ℕ0 × {(0g‘𝑅)})‘𝐾) = (0g‘𝑅)) |
60 | 57, 58, 59 | sylancr 591 |
. . . . . . . 8
⊢ (𝜑 → ((ℕ0
× {(0g‘𝑅)})‘𝐾) = (0g‘𝑅)) |
61 | 50, 56, 60 | 3eqtrd 2798 |
. . . . . . 7
⊢ (𝜑 →
((coe1‘(𝑃
Σg (𝑥 ∈ ∅ ↦ 𝑀)))‘𝐾) = (0g‘𝑅)) |
62 | | mpt0 6466 |
. . . . . . . . 9
⊢ (𝑥 ∈ ∅ ↦
((coe1‘𝑀)‘𝐾)) = ∅ |
63 | 62 | oveq2i 7154 |
. . . . . . . 8
⊢ (𝑅 Σg
(𝑥 ∈ ∅ ↦
((coe1‘𝑀)‘𝐾))) = (𝑅 Σg
∅) |
64 | 53 | gsum0 17945 |
. . . . . . . 8
⊢ (𝑅 Σg
∅) = (0g‘𝑅) |
65 | 63, 64 | eqtri 2782 |
. . . . . . 7
⊢ (𝑅 Σg
(𝑥 ∈ ∅ ↦
((coe1‘𝑀)‘𝐾))) = (0g‘𝑅) |
66 | 61, 65 | eqtr4di 2812 |
. . . . . 6
⊢ (𝜑 →
((coe1‘(𝑃
Σg (𝑥 ∈ ∅ ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ ∅ ↦
((coe1‘𝑀)‘𝐾)))) |
67 | 66 | adantr 485 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ ∅ 𝑀 ∈ 𝐵) → ((coe1‘(𝑃 Σg
(𝑥 ∈ ∅ ↦
𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ ∅ ↦
((coe1‘𝑀)‘𝐾)))) |
68 | | coe1fzgsumd.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑃) |
69 | 52, 68, 51, 58 | coe1fzgsumdlem 21010 |
. . . . . . . 8
⊢ ((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑) → ((∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 → ((coe1‘(𝑃 Σg
(𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾)))) → (∀𝑥 ∈ (𝑚 ∪ {𝑎})𝑀 ∈ 𝐵 → ((coe1‘(𝑃 Σg
(𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((coe1‘𝑀)‘𝐾)))))) |
70 | 69 | 3expia 1119 |
. . . . . . 7
⊢ ((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚) → (𝜑 → ((∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 → ((coe1‘(𝑃 Σg
(𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾)))) → (∀𝑥 ∈ (𝑚 ∪ {𝑎})𝑀 ∈ 𝐵 → ((coe1‘(𝑃 Σg
(𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((coe1‘𝑀)‘𝐾))))))) |
71 | 70 | a2d 29 |
. . . . . 6
⊢ ((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚) → ((𝜑 → (∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 → ((coe1‘(𝑃 Σg
(𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾))))) → (𝜑 → (∀𝑥 ∈ (𝑚 ∪ {𝑎})𝑀 ∈ 𝐵 → ((coe1‘(𝑃 Σg
(𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((coe1‘𝑀)‘𝐾))))))) |
72 | | impexp 455 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) → ((coe1‘(𝑃 Σg
(𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾)))) ↔ (𝜑 → (∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵 → ((coe1‘(𝑃 Σg
(𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾)))))) |
73 | | impexp 455 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑥 ∈ (𝑚 ∪ {𝑎})𝑀 ∈ 𝐵) → ((coe1‘(𝑃 Σg
(𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((coe1‘𝑀)‘𝐾)))) ↔ (𝜑 → (∀𝑥 ∈ (𝑚 ∪ {𝑎})𝑀 ∈ 𝐵 → ((coe1‘(𝑃 Σg
(𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((coe1‘𝑀)‘𝐾)))))) |
74 | 71, 72, 73 | 3imtr4g 300 |
. . . . 5
⊢ ((𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚) → (((𝜑 ∧ ∀𝑥 ∈ 𝑚 𝑀 ∈ 𝐵) → ((coe1‘(𝑃 Σg
(𝑥 ∈ 𝑚 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑚 ↦ ((coe1‘𝑀)‘𝐾)))) → ((𝜑 ∧ ∀𝑥 ∈ (𝑚 ∪ {𝑎})𝑀 ∈ 𝐵) → ((coe1‘(𝑃 Σg
(𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ (𝑚 ∪ {𝑎}) ↦ ((coe1‘𝑀)‘𝐾)))))) |
75 | 12, 22, 32, 42, 67, 74 | findcard2s 8777 |
. . . 4
⊢ (𝑁 ∈ Fin → ((𝜑 ∧ ∀𝑥 ∈ 𝑁 𝑀 ∈ 𝐵) → ((coe1‘(𝑃 Σg
(𝑥 ∈ 𝑁 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑁 ↦ ((coe1‘𝑀)‘𝐾))))) |
76 | 75 | expd 420 |
. . 3
⊢ (𝑁 ∈ Fin → (𝜑 → (∀𝑥 ∈ 𝑁 𝑀 ∈ 𝐵 → ((coe1‘(𝑃 Σg
(𝑥 ∈ 𝑁 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑁 ↦ ((coe1‘𝑀)‘𝐾)))))) |
77 | 2, 76 | mpcom 38 |
. 2
⊢ (𝜑 → (∀𝑥 ∈ 𝑁 𝑀 ∈ 𝐵 → ((coe1‘(𝑃 Σg
(𝑥 ∈ 𝑁 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑁 ↦ ((coe1‘𝑀)‘𝐾))))) |
78 | 1, 77 | mpd 15 |
1
⊢ (𝜑 →
((coe1‘(𝑃
Σg (𝑥 ∈ 𝑁 ↦ 𝑀)))‘𝐾) = (𝑅 Σg (𝑥 ∈ 𝑁 ↦ ((coe1‘𝑀)‘𝐾)))) |