| Step | Hyp | Ref
| Expression |
| 1 | | rrgsupp.i |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
| 2 | | rrgsupp.x |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ 𝐸) |
| 3 | 2 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝑋 ∈ 𝐸) |
| 4 | | fvexd 6921 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑌‘𝑦) ∈ V) |
| 5 | | fconstmpt 5747 |
. . . . . . . . . 10
⊢ (𝐼 × {𝑋}) = (𝑦 ∈ 𝐼 ↦ 𝑋) |
| 6 | 5 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (𝐼 × {𝑋}) = (𝑦 ∈ 𝐼 ↦ 𝑋)) |
| 7 | | rrgsupp.y |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌:𝐼⟶𝐵) |
| 8 | 7 | feqmptd 6977 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 = (𝑦 ∈ 𝐼 ↦ (𝑌‘𝑦))) |
| 9 | 1, 3, 4, 6, 8 | offval2 7717 |
. . . . . . . 8
⊢ (𝜑 → ((𝐼 × {𝑋}) ∘f · 𝑌) = (𝑦 ∈ 𝐼 ↦ (𝑋 · (𝑌‘𝑦)))) |
| 10 | 9 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐼 × {𝑋}) ∘f · 𝑌) = (𝑦 ∈ 𝐼 ↦ (𝑋 · (𝑌‘𝑦)))) |
| 11 | 10 | fveq1d 6908 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (((𝐼 × {𝑋}) ∘f · 𝑌)‘𝑥) = ((𝑦 ∈ 𝐼 ↦ (𝑋 · (𝑌‘𝑦)))‘𝑥)) |
| 12 | | simpr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼) |
| 13 | | ovex 7464 |
. . . . . . 7
⊢ (𝑋 · (𝑌‘𝑥)) ∈ V |
| 14 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → (𝑌‘𝑦) = (𝑌‘𝑥)) |
| 15 | 14 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (𝑋 · (𝑌‘𝑦)) = (𝑋 · (𝑌‘𝑥))) |
| 16 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐼 ↦ (𝑋 · (𝑌‘𝑦))) = (𝑦 ∈ 𝐼 ↦ (𝑋 · (𝑌‘𝑦))) |
| 17 | 15, 16 | fvmptg 7014 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐼 ∧ (𝑋 · (𝑌‘𝑥)) ∈ V) → ((𝑦 ∈ 𝐼 ↦ (𝑋 · (𝑌‘𝑦)))‘𝑥) = (𝑋 · (𝑌‘𝑥))) |
| 18 | 12, 13, 17 | sylancl 586 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑦 ∈ 𝐼 ↦ (𝑋 · (𝑌‘𝑦)))‘𝑥) = (𝑋 · (𝑌‘𝑥))) |
| 19 | 11, 18 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (((𝐼 × {𝑋}) ∘f · 𝑌)‘𝑥) = (𝑋 · (𝑌‘𝑥))) |
| 20 | 19 | neeq1d 3000 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((((𝐼 × {𝑋}) ∘f · 𝑌)‘𝑥) ≠ 0 ↔ (𝑋 · (𝑌‘𝑥)) ≠ 0 )) |
| 21 | 20 | rabbidva 3443 |
. . 3
⊢ (𝜑 → {𝑥 ∈ 𝐼 ∣ (((𝐼 × {𝑋}) ∘f · 𝑌)‘𝑥) ≠ 0 } = {𝑥 ∈ 𝐼 ∣ (𝑋 · (𝑌‘𝑥)) ≠ 0 }) |
| 22 | | rrgsupp.r |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 23 | 22 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ Ring) |
| 24 | 2 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑋 ∈ 𝐸) |
| 25 | 7 | ffvelcdmda 7104 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑌‘𝑥) ∈ 𝐵) |
| 26 | | rrgval.e |
. . . . . . 7
⊢ 𝐸 = (RLReg‘𝑅) |
| 27 | | rrgval.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑅) |
| 28 | | rrgval.t |
. . . . . . 7
⊢ · =
(.r‘𝑅) |
| 29 | | rrgval.z |
. . . . . . 7
⊢ 0 =
(0g‘𝑅) |
| 30 | 26, 27, 28, 29 | rrgeq0 20700 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐸 ∧ (𝑌‘𝑥) ∈ 𝐵) → ((𝑋 · (𝑌‘𝑥)) = 0 ↔ (𝑌‘𝑥) = 0 )) |
| 31 | 23, 24, 25, 30 | syl3anc 1373 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑋 · (𝑌‘𝑥)) = 0 ↔ (𝑌‘𝑥) = 0 )) |
| 32 | 31 | necon3bid 2985 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑋 · (𝑌‘𝑥)) ≠ 0 ↔ (𝑌‘𝑥) ≠ 0 )) |
| 33 | 32 | rabbidva 3443 |
. . 3
⊢ (𝜑 → {𝑥 ∈ 𝐼 ∣ (𝑋 · (𝑌‘𝑥)) ≠ 0 } = {𝑥 ∈ 𝐼 ∣ (𝑌‘𝑥) ≠ 0 }) |
| 34 | 21, 33 | eqtrd 2777 |
. 2
⊢ (𝜑 → {𝑥 ∈ 𝐼 ∣ (((𝐼 × {𝑋}) ∘f · 𝑌)‘𝑥) ≠ 0 } = {𝑥 ∈ 𝐼 ∣ (𝑌‘𝑥) ≠ 0 }) |
| 35 | | ovex 7464 |
. . . . . 6
⊢ (𝑋 · (𝑌‘𝑦)) ∈ V |
| 36 | 35, 16 | fnmpti 6711 |
. . . . 5
⊢ (𝑦 ∈ 𝐼 ↦ (𝑋 · (𝑌‘𝑦))) Fn 𝐼 |
| 37 | | fneq1 6659 |
. . . . 5
⊢ (((𝐼 × {𝑋}) ∘f · 𝑌) = (𝑦 ∈ 𝐼 ↦ (𝑋 · (𝑌‘𝑦))) → (((𝐼 × {𝑋}) ∘f · 𝑌) Fn 𝐼 ↔ (𝑦 ∈ 𝐼 ↦ (𝑋 · (𝑌‘𝑦))) Fn 𝐼)) |
| 38 | 36, 37 | mpbiri 258 |
. . . 4
⊢ (((𝐼 × {𝑋}) ∘f · 𝑌) = (𝑦 ∈ 𝐼 ↦ (𝑋 · (𝑌‘𝑦))) → ((𝐼 × {𝑋}) ∘f · 𝑌) Fn 𝐼) |
| 39 | 9, 38 | syl 17 |
. . 3
⊢ (𝜑 → ((𝐼 × {𝑋}) ∘f · 𝑌) Fn 𝐼) |
| 40 | 29 | fvexi 6920 |
. . . 4
⊢ 0 ∈
V |
| 41 | 40 | a1i 11 |
. . 3
⊢ (𝜑 → 0 ∈ V) |
| 42 | | suppvalfn 8193 |
. . 3
⊢ ((((𝐼 × {𝑋}) ∘f · 𝑌) Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → (((𝐼 × {𝑋}) ∘f · 𝑌) supp 0 ) = {𝑥 ∈ 𝐼 ∣ (((𝐼 × {𝑋}) ∘f · 𝑌)‘𝑥) ≠ 0 }) |
| 43 | 39, 1, 41, 42 | syl3anc 1373 |
. 2
⊢ (𝜑 → (((𝐼 × {𝑋}) ∘f · 𝑌) supp 0 ) = {𝑥 ∈ 𝐼 ∣ (((𝐼 × {𝑋}) ∘f · 𝑌)‘𝑥) ≠ 0 }) |
| 44 | 7 | ffnd 6737 |
. . 3
⊢ (𝜑 → 𝑌 Fn 𝐼) |
| 45 | | suppvalfn 8193 |
. . 3
⊢ ((𝑌 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → (𝑌 supp 0 ) = {𝑥 ∈ 𝐼 ∣ (𝑌‘𝑥) ≠ 0 }) |
| 46 | 44, 1, 41, 45 | syl3anc 1373 |
. 2
⊢ (𝜑 → (𝑌 supp 0 ) = {𝑥 ∈ 𝐼 ∣ (𝑌‘𝑥) ≠ 0 }) |
| 47 | 34, 43, 46 | 3eqtr4d 2787 |
1
⊢ (𝜑 → (((𝐼 × {𝑋}) ∘f · 𝑌) supp 0 ) = (𝑌 supp 0 )) |