Step | Hyp | Ref
| Expression |
1 | | dprdff.w |
. . . . 5
⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 } |
2 | | dprdff.1 |
. . . . 5
⊢ (𝜑 → 𝐺dom DProd 𝑆) |
3 | | dprdff.2 |
. . . . 5
⊢ (𝜑 → dom 𝑆 = 𝐼) |
4 | | dprdff.3 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ 𝑊) |
5 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝐺) =
(Base‘𝐺) |
6 | 1, 2, 3, 4, 5 | dprdff 19399 |
. . . 4
⊢ (𝜑 → 𝐹:𝐼⟶(Base‘𝐺)) |
7 | 6 | ffnd 6546 |
. . 3
⊢ (𝜑 → 𝐹 Fn 𝐼) |
8 | 6 | ffvelrnda 6904 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝐹‘𝑦) ∈ (Base‘𝐺)) |
9 | | simpr 488 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 = 𝑧) → 𝑦 = 𝑧) |
10 | 9 | fveq2d 6721 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 = 𝑧) → (𝐹‘𝑦) = (𝐹‘𝑧)) |
11 | 9 | equcomd 2027 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 = 𝑧) → 𝑧 = 𝑦) |
12 | 11 | fveq2d 6721 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 = 𝑧) → (𝐹‘𝑧) = (𝐹‘𝑦)) |
13 | 10, 12 | oveq12d 7231 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 = 𝑧) → ((𝐹‘𝑦)(+g‘𝐺)(𝐹‘𝑧)) = ((𝐹‘𝑧)(+g‘𝐺)(𝐹‘𝑦))) |
14 | 2 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 ≠ 𝑧) → 𝐺dom DProd 𝑆) |
15 | 3 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 ≠ 𝑧) → dom 𝑆 = 𝐼) |
16 | | simpllr 776 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 ≠ 𝑧) → 𝑦 ∈ 𝐼) |
17 | | simplr 769 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 ≠ 𝑧) → 𝑧 ∈ 𝐼) |
18 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 ≠ 𝑧) → 𝑦 ≠ 𝑧) |
19 | | dprdfcntz.z |
. . . . . . . . . . 11
⊢ 𝑍 = (Cntz‘𝐺) |
20 | 14, 15, 16, 17, 18, 19 | dprdcntz 19395 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 ≠ 𝑧) → (𝑆‘𝑦) ⊆ (𝑍‘(𝑆‘𝑧))) |
21 | 1, 2, 3, 4 | dprdfcl 19400 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝐹‘𝑦) ∈ (𝑆‘𝑦)) |
22 | 21 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 ≠ 𝑧) → (𝐹‘𝑦) ∈ (𝑆‘𝑦)) |
23 | 20, 22 | sseldd 3902 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 ≠ 𝑧) → (𝐹‘𝑦) ∈ (𝑍‘(𝑆‘𝑧))) |
24 | 1, 2, 3, 4 | dprdfcl 19400 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) ∈ (𝑆‘𝑧)) |
25 | 24 | ad4ant13 751 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 ≠ 𝑧) → (𝐹‘𝑧) ∈ (𝑆‘𝑧)) |
26 | | eqid 2737 |
. . . . . . . . . 10
⊢
(+g‘𝐺) = (+g‘𝐺) |
27 | 26, 19 | cntzi 18723 |
. . . . . . . . 9
⊢ (((𝐹‘𝑦) ∈ (𝑍‘(𝑆‘𝑧)) ∧ (𝐹‘𝑧) ∈ (𝑆‘𝑧)) → ((𝐹‘𝑦)(+g‘𝐺)(𝐹‘𝑧)) = ((𝐹‘𝑧)(+g‘𝐺)(𝐹‘𝑦))) |
28 | 23, 25, 27 | syl2anc 587 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 ≠ 𝑧) → ((𝐹‘𝑦)(+g‘𝐺)(𝐹‘𝑧)) = ((𝐹‘𝑧)(+g‘𝐺)(𝐹‘𝑦))) |
29 | 13, 28 | pm2.61dane 3029 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) → ((𝐹‘𝑦)(+g‘𝐺)(𝐹‘𝑧)) = ((𝐹‘𝑧)(+g‘𝐺)(𝐹‘𝑦))) |
30 | 29 | ralrimiva 3105 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → ∀𝑧 ∈ 𝐼 ((𝐹‘𝑦)(+g‘𝐺)(𝐹‘𝑧)) = ((𝐹‘𝑧)(+g‘𝐺)(𝐹‘𝑦))) |
31 | 7 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝐹 Fn 𝐼) |
32 | | oveq2 7221 |
. . . . . . . . 9
⊢ (𝑥 = (𝐹‘𝑧) → ((𝐹‘𝑦)(+g‘𝐺)𝑥) = ((𝐹‘𝑦)(+g‘𝐺)(𝐹‘𝑧))) |
33 | | oveq1 7220 |
. . . . . . . . 9
⊢ (𝑥 = (𝐹‘𝑧) → (𝑥(+g‘𝐺)(𝐹‘𝑦)) = ((𝐹‘𝑧)(+g‘𝐺)(𝐹‘𝑦))) |
34 | 32, 33 | eqeq12d 2753 |
. . . . . . . 8
⊢ (𝑥 = (𝐹‘𝑧) → (((𝐹‘𝑦)(+g‘𝐺)𝑥) = (𝑥(+g‘𝐺)(𝐹‘𝑦)) ↔ ((𝐹‘𝑦)(+g‘𝐺)(𝐹‘𝑧)) = ((𝐹‘𝑧)(+g‘𝐺)(𝐹‘𝑦)))) |
35 | 34 | ralrn 6907 |
. . . . . . 7
⊢ (𝐹 Fn 𝐼 → (∀𝑥 ∈ ran 𝐹((𝐹‘𝑦)(+g‘𝐺)𝑥) = (𝑥(+g‘𝐺)(𝐹‘𝑦)) ↔ ∀𝑧 ∈ 𝐼 ((𝐹‘𝑦)(+g‘𝐺)(𝐹‘𝑧)) = ((𝐹‘𝑧)(+g‘𝐺)(𝐹‘𝑦)))) |
36 | 31, 35 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (∀𝑥 ∈ ran 𝐹((𝐹‘𝑦)(+g‘𝐺)𝑥) = (𝑥(+g‘𝐺)(𝐹‘𝑦)) ↔ ∀𝑧 ∈ 𝐼 ((𝐹‘𝑦)(+g‘𝐺)(𝐹‘𝑧)) = ((𝐹‘𝑧)(+g‘𝐺)(𝐹‘𝑦)))) |
37 | 30, 36 | mpbird 260 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → ∀𝑥 ∈ ran 𝐹((𝐹‘𝑦)(+g‘𝐺)𝑥) = (𝑥(+g‘𝐺)(𝐹‘𝑦))) |
38 | 6 | frnd 6553 |
. . . . . . 7
⊢ (𝜑 → ran 𝐹 ⊆ (Base‘𝐺)) |
39 | 38 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → ran 𝐹 ⊆ (Base‘𝐺)) |
40 | 5, 26, 19 | elcntz 18716 |
. . . . . 6
⊢ (ran
𝐹 ⊆ (Base‘𝐺) → ((𝐹‘𝑦) ∈ (𝑍‘ran 𝐹) ↔ ((𝐹‘𝑦) ∈ (Base‘𝐺) ∧ ∀𝑥 ∈ ran 𝐹((𝐹‘𝑦)(+g‘𝐺)𝑥) = (𝑥(+g‘𝐺)(𝐹‘𝑦))))) |
41 | 39, 40 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → ((𝐹‘𝑦) ∈ (𝑍‘ran 𝐹) ↔ ((𝐹‘𝑦) ∈ (Base‘𝐺) ∧ ∀𝑥 ∈ ran 𝐹((𝐹‘𝑦)(+g‘𝐺)𝑥) = (𝑥(+g‘𝐺)(𝐹‘𝑦))))) |
42 | 8, 37, 41 | mpbir2and 713 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝐹‘𝑦) ∈ (𝑍‘ran 𝐹)) |
43 | 42 | ralrimiva 3105 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ 𝐼 (𝐹‘𝑦) ∈ (𝑍‘ran 𝐹)) |
44 | | ffnfv 6935 |
. . 3
⊢ (𝐹:𝐼⟶(𝑍‘ran 𝐹) ↔ (𝐹 Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 (𝐹‘𝑦) ∈ (𝑍‘ran 𝐹))) |
45 | 7, 43, 44 | sylanbrc 586 |
. 2
⊢ (𝜑 → 𝐹:𝐼⟶(𝑍‘ran 𝐹)) |
46 | 45 | frnd 6553 |
1
⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |