| 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 20032 | . . . 4
⊢ (𝜑 → 𝐹:𝐼⟶(Base‘𝐺)) | 
| 7 | 6 | ffnd 6737 | . . 3
⊢ (𝜑 → 𝐹 Fn 𝐼) | 
| 8 | 6 | ffvelcdmda 7104 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝐹‘𝑦) ∈ (Base‘𝐺)) | 
| 9 |  | simpr 484 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 = 𝑧) → 𝑦 = 𝑧) | 
| 10 | 9 | fveq2d 6910 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 = 𝑧) → (𝐹‘𝑦) = (𝐹‘𝑧)) | 
| 11 | 9 | equcomd 2018 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 = 𝑧) → 𝑧 = 𝑦) | 
| 12 | 11 | fveq2d 6910 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 = 𝑧) → (𝐹‘𝑧) = (𝐹‘𝑦)) | 
| 13 | 10, 12 | oveq12d 7449 | . . . . . . . 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 484 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 ≠ 𝑧) → 𝑦 ≠ 𝑧) | 
| 19 |  | dprdfcntz.z | . . . . . . . . . . 11
⊢ 𝑍 = (Cntz‘𝐺) | 
| 20 | 14, 15, 16, 17, 18, 19 | dprdcntz 20028 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 ≠ 𝑧) → (𝑆‘𝑦) ⊆ (𝑍‘(𝑆‘𝑧))) | 
| 21 | 1, 2, 3, 4 | dprdfcl 20033 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝐹‘𝑦) ∈ (𝑆‘𝑦)) | 
| 22 | 21 | ad2antrr 726 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 ≠ 𝑧) → (𝐹‘𝑦) ∈ (𝑆‘𝑦)) | 
| 23 | 20, 22 | sseldd 3984 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 ≠ 𝑧) → (𝐹‘𝑦) ∈ (𝑍‘(𝑆‘𝑧))) | 
| 24 | 1, 2, 3, 4 | dprdfcl 20033 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑧 ∈ 𝐼) → (𝐹‘𝑧) ∈ (𝑆‘𝑧)) | 
| 25 | 24 | ad4ant13 751 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 ≠ 𝑧) → (𝐹‘𝑧) ∈ (𝑆‘𝑧)) | 
| 26 |  | eqid 2737 | . . . . . . . . . 10
⊢
(+g‘𝐺) = (+g‘𝐺) | 
| 27 | 26, 19 | cntzi 19347 | . . . . . . . . 9
⊢ (((𝐹‘𝑦) ∈ (𝑍‘(𝑆‘𝑧)) ∧ (𝐹‘𝑧) ∈ (𝑆‘𝑧)) → ((𝐹‘𝑦)(+g‘𝐺)(𝐹‘𝑧)) = ((𝐹‘𝑧)(+g‘𝐺)(𝐹‘𝑦))) | 
| 28 | 23, 25, 27 | syl2anc 584 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) ∧ 𝑦 ≠ 𝑧) → ((𝐹‘𝑦)(+g‘𝐺)(𝐹‘𝑧)) = ((𝐹‘𝑧)(+g‘𝐺)(𝐹‘𝑦))) | 
| 29 | 13, 28 | pm2.61dane 3029 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐼) ∧ 𝑧 ∈ 𝐼) → ((𝐹‘𝑦)(+g‘𝐺)(𝐹‘𝑧)) = ((𝐹‘𝑧)(+g‘𝐺)(𝐹‘𝑦))) | 
| 30 | 29 | ralrimiva 3146 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → ∀𝑧 ∈ 𝐼 ((𝐹‘𝑦)(+g‘𝐺)(𝐹‘𝑧)) = ((𝐹‘𝑧)(+g‘𝐺)(𝐹‘𝑦))) | 
| 31 | 7 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝐹 Fn 𝐼) | 
| 32 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑥 = (𝐹‘𝑧) → ((𝐹‘𝑦)(+g‘𝐺)𝑥) = ((𝐹‘𝑦)(+g‘𝐺)(𝐹‘𝑧))) | 
| 33 |  | oveq1 7438 | . . . . . . . . 9
⊢ (𝑥 = (𝐹‘𝑧) → (𝑥(+g‘𝐺)(𝐹‘𝑦)) = ((𝐹‘𝑧)(+g‘𝐺)(𝐹‘𝑦))) | 
| 34 | 32, 33 | eqeq12d 2753 | . . . . . . . 8
⊢ (𝑥 = (𝐹‘𝑧) → (((𝐹‘𝑦)(+g‘𝐺)𝑥) = (𝑥(+g‘𝐺)(𝐹‘𝑦)) ↔ ((𝐹‘𝑦)(+g‘𝐺)(𝐹‘𝑧)) = ((𝐹‘𝑧)(+g‘𝐺)(𝐹‘𝑦)))) | 
| 35 | 34 | ralrn 7108 | . . . . . . 7
⊢ (𝐹 Fn 𝐼 → (∀𝑥 ∈ ran 𝐹((𝐹‘𝑦)(+g‘𝐺)𝑥) = (𝑥(+g‘𝐺)(𝐹‘𝑦)) ↔ ∀𝑧 ∈ 𝐼 ((𝐹‘𝑦)(+g‘𝐺)(𝐹‘𝑧)) = ((𝐹‘𝑧)(+g‘𝐺)(𝐹‘𝑦)))) | 
| 36 | 31, 35 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (∀𝑥 ∈ ran 𝐹((𝐹‘𝑦)(+g‘𝐺)𝑥) = (𝑥(+g‘𝐺)(𝐹‘𝑦)) ↔ ∀𝑧 ∈ 𝐼 ((𝐹‘𝑦)(+g‘𝐺)(𝐹‘𝑧)) = ((𝐹‘𝑧)(+g‘𝐺)(𝐹‘𝑦)))) | 
| 37 | 30, 36 | mpbird 257 | . . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → ∀𝑥 ∈ ran 𝐹((𝐹‘𝑦)(+g‘𝐺)𝑥) = (𝑥(+g‘𝐺)(𝐹‘𝑦))) | 
| 38 | 6 | frnd 6744 | . . . . . . 7
⊢ (𝜑 → ran 𝐹 ⊆ (Base‘𝐺)) | 
| 39 | 38 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → ran 𝐹 ⊆ (Base‘𝐺)) | 
| 40 | 5, 26, 19 | elcntz 19340 | . . . . . 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 3146 | . . 3
⊢ (𝜑 → ∀𝑦 ∈ 𝐼 (𝐹‘𝑦) ∈ (𝑍‘ran 𝐹)) | 
| 44 |  | ffnfv 7139 | . . 3
⊢ (𝐹:𝐼⟶(𝑍‘ran 𝐹) ↔ (𝐹 Fn 𝐼 ∧ ∀𝑦 ∈ 𝐼 (𝐹‘𝑦) ∈ (𝑍‘ran 𝐹))) | 
| 45 | 7, 43, 44 | sylanbrc 583 | . 2
⊢ (𝜑 → 𝐹:𝐼⟶(𝑍‘ran 𝐹)) | 
| 46 | 45 | frnd 6744 | 1
⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) |