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 2610 |
. . . . 5
⊢
(Base‘𝐺) =
(Base‘𝐺) |
6 | 1, 2, 3, 4, 5 | dprdff 18234 |
. . . 4
⊢ (𝜑 → 𝐹:𝐼⟶(Base‘𝐺)) |
7 | | ffn 5958 |
. . . 4
⊢ (𝐹:𝐼⟶(Base‘𝐺) → 𝐹 Fn 𝐼) |
8 | 6, 7 | syl 17 |
. . 3
⊢ (𝜑 → 𝐹 Fn 𝐼) |
9 | 6 | ffvelrnda 6267 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝐹‘𝑦) ∈ (Base‘𝐺)) |
10 | | simpr 476 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 = 𝑧) → 𝑦 = 𝑧) |
11 | 10 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 = 𝑧) → (𝐹‘𝑦) = (𝐹‘𝑧)) |
12 | 10 | eqcomd 2616 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 = 𝑧) → 𝑧 = 𝑦) |
13 | 12 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 = 𝑧) → (𝐹‘𝑧) = (𝐹‘𝑦)) |
14 | 11, 13 | oveq12d 6567 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 = 𝑧) → ((𝐹‘𝑦)(+g‘𝐺)(𝐹‘𝑧)) = ((𝐹‘𝑧)(+g‘𝐺)(𝐹‘𝑦))) |
15 | 2 | ad3antrrr 762 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 ≠ 𝑧) → 𝐺dom DProd 𝑆) |
16 | 3 | ad3antrrr 762 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 ≠ 𝑧) → dom 𝑆 = 𝐼) |
17 | | simpllr 795 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 ≠ 𝑧) → 𝑦 ∈ 𝐼) |
18 | | simplr 788 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 ≠ 𝑧) → 𝑧 ∈ 𝐼) |
19 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 ≠ 𝑧) → 𝑦 ≠ 𝑧) |
20 | | dprdfcntz.z |
. . . . . . . . . . 11
⊢ 𝑍 = (Cntz‘𝐺) |
21 | 15, 16, 17, 18, 19, 20 | dprdcntz 18230 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 ≠ 𝑧) → (𝑆‘𝑦) ⊆ (𝑍‘(𝑆‘𝑧))) |
22 | 1, 2, 3, 4 | dprdfcl 18235 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝐹‘𝑦) ∈ (𝑆‘𝑦)) |
23 | 22 | ad2antrr 758 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 ≠ 𝑧) → (𝐹‘𝑦) ∈ (𝑆‘𝑦)) |
24 | 21, 23 | sseldd 3569 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 ≠ 𝑧) → (𝐹‘𝑦) ∈ (𝑍‘(𝑆‘𝑧))) |
25 | 1, 2, 3, 4 | dprdfcl 18235 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) ∈ (𝑆‘𝑧)) |
26 | 25 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) ∈ (𝑆‘𝑧)) |
27 | 26 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 ≠ 𝑧) → (𝐹‘𝑧) ∈ (𝑆‘𝑧)) |
28 | | eqid 2610 |
. . . . . . . . . 10
⊢
(+g‘𝐺) = (+g‘𝐺) |
29 | 28, 20 | cntzi 17585 |
. . . . . . . . 9
⊢ (((𝐹‘𝑦) ∈ (𝑍‘(𝑆‘𝑧)) ∧ (𝐹‘𝑧) ∈ (𝑆‘𝑧)) → ((𝐹‘𝑦)(+g‘𝐺)(𝐹‘𝑧)) = ((𝐹‘𝑧)(+g‘𝐺)(𝐹‘𝑦))) |
30 | 24, 27, 29 | syl2anc 691 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 ≠ 𝑧) → ((𝐹‘𝑦)(+g‘𝐺)(𝐹‘𝑧)) = ((𝐹‘𝑧)(+g‘𝐺)(𝐹‘𝑦))) |
31 | 14, 30 | pm2.61dane 2869 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) → ((𝐹‘𝑦)(+g‘𝐺)(𝐹‘𝑧)) = ((𝐹‘𝑧)(+g‘𝐺)(𝐹‘𝑦))) |
32 | 31 | ralrimiva 2949 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → ∀𝑧 ∈ 𝐼 ((𝐹‘𝑦)(+g‘𝐺)(𝐹‘𝑧)) = ((𝐹‘𝑧)(+g‘𝐺)(𝐹‘𝑦))) |
33 | 8 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝐹 Fn 𝐼) |
34 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑥 = (𝐹‘𝑧) → ((𝐹‘𝑦)(+g‘𝐺)𝑥) = ((𝐹‘𝑦)(+g‘𝐺)(𝐹‘𝑧))) |
35 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑥 = (𝐹‘𝑧) → (𝑥(+g‘𝐺)(𝐹‘𝑦)) = ((𝐹‘𝑧)(+g‘𝐺)(𝐹‘𝑦))) |
36 | 34, 35 | eqeq12d 2625 |
. . . . . . . 8
⊢ (𝑥 = (𝐹‘𝑧) → (((𝐹‘𝑦)(+g‘𝐺)𝑥) = (𝑥(+g‘𝐺)(𝐹‘𝑦)) ↔ ((𝐹‘𝑦)(+g‘𝐺)(𝐹‘𝑧)) = ((𝐹‘𝑧)(+g‘𝐺)(𝐹‘𝑦)))) |
37 | 36 | ralrn 6270 |
. . . . . . 7
⊢ (𝐹 Fn 𝐼 → (∀𝑥 ∈ ran 𝐹((𝐹‘𝑦)(+g‘𝐺)𝑥) = (𝑥(+g‘𝐺)(𝐹‘𝑦)) ↔ ∀𝑧 ∈ 𝐼 ((𝐹‘𝑦)(+g‘𝐺)(𝐹‘𝑧)) = ((𝐹‘𝑧)(+g‘𝐺)(𝐹‘𝑦)))) |
38 | 33, 37 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (∀𝑥 ∈ ran 𝐹((𝐹‘𝑦)(+g‘𝐺)𝑥) = (𝑥(+g‘𝐺)(𝐹‘𝑦)) ↔ ∀𝑧 ∈ 𝐼 ((𝐹‘𝑦)(+g‘𝐺)(𝐹‘𝑧)) = ((𝐹‘𝑧)(+g‘𝐺)(𝐹‘𝑦)))) |
39 | 32, 38 | mpbird 246 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → ∀𝑥 ∈ ran 𝐹((𝐹‘𝑦)(+g‘𝐺)𝑥) = (𝑥(+g‘𝐺)(𝐹‘𝑦))) |
40 | | frn 5966 |
. . . . . . . 8
⊢ (𝐹:𝐼⟶(Base‘𝐺) → ran 𝐹 ⊆ (Base‘𝐺)) |
41 | 6, 40 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ran 𝐹 ⊆ (Base‘𝐺)) |
42 | 41 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → ran 𝐹 ⊆ (Base‘𝐺)) |
43 | 5, 28, 20 | elcntz 17578 |
. . . . . 6
⊢ (ran
𝐹 ⊆ (Base‘𝐺) → ((𝐹‘𝑦) ∈ (𝑍‘ran 𝐹) ↔ ((𝐹‘𝑦) ∈ (Base‘𝐺) ∧ ∀𝑥 ∈ ran 𝐹((𝐹‘𝑦)(+g‘𝐺)𝑥) = (𝑥(+g‘𝐺)(𝐹‘𝑦))))) |
44 | 42, 43 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → ((𝐹‘𝑦) ∈ (𝑍‘ran 𝐹) ↔ ((𝐹‘𝑦) ∈ (Base‘𝐺) ∧ ∀𝑥 ∈ ran 𝐹((𝐹‘𝑦)(+g‘𝐺)𝑥) = (𝑥(+g‘𝐺)(𝐹‘𝑦))))) |
45 | 9, 39, 44 | mpbir2and 959 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝐹‘𝑦) ∈ (𝑍‘ran 𝐹)) |
46 | 45 | ralrimiva 2949 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ 𝐼 (𝐹‘𝑦) ∈ (𝑍‘ran 𝐹)) |
47 | | ffnfv 6295 |
. . 3
⊢ (𝐹:𝐼⟶(𝑍‘ran 𝐹) ↔ (𝐹 Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 (𝐹‘𝑦) ∈ (𝑍‘ran 𝐹))) |
48 | 8, 46, 47 | sylanbrc 695 |
. 2
⊢ (𝜑 → 𝐹:𝐼⟶(𝑍‘ran 𝐹)) |
49 | | frn 5966 |
. 2
⊢ (𝐹:𝐼⟶(𝑍‘ran 𝐹) → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |
50 | 48, 49 | syl 17 |
1
⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |