Step | Hyp | Ref
| Expression |
1 | | rrgsupp.i |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
2 | | rrgsupp.x |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ 𝐸) |
3 | 2 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → 𝑋 ∈ 𝐸) |
4 | | fvex 6113 |
. . . . . . . . . 10
⊢ (𝑌‘𝑦) ∈ V |
5 | 4 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → (𝑌‘𝑦) ∈ V) |
6 | | fconstmpt 5085 |
. . . . . . . . . 10
⊢ (𝐼 × {𝑋}) = (𝑦 ∈ 𝐼 ↦ 𝑋) |
7 | 6 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (𝐼 × {𝑋}) = (𝑦 ∈ 𝐼 ↦ 𝑋)) |
8 | | rrgsupp.y |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌:𝐼⟶𝐵) |
9 | 8 | feqmptd 6159 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 = (𝑦 ∈ 𝐼 ↦ (𝑌‘𝑦))) |
10 | 1, 3, 5, 7, 9 | offval2 6812 |
. . . . . . . 8
⊢ (𝜑 → ((𝐼 × {𝑋}) ∘𝑓 · 𝑌) = (𝑦 ∈ 𝐼 ↦ (𝑋 · (𝑌‘𝑦)))) |
11 | 10 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐼 × {𝑋}) ∘𝑓 · 𝑌) = (𝑦 ∈ 𝐼 ↦ (𝑋 · (𝑌‘𝑦)))) |
12 | 11 | fveq1d 6105 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (((𝐼 × {𝑋}) ∘𝑓 · 𝑌)‘𝑥) = ((𝑦 ∈ 𝐼 ↦ (𝑋 · (𝑌‘𝑦)))‘𝑥)) |
13 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑥 ∈ 𝐼) |
14 | | ovex 6577 |
. . . . . . 7
⊢ (𝑋 · (𝑌‘𝑥)) ∈ V |
15 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → (𝑌‘𝑦) = (𝑌‘𝑥)) |
16 | 15 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (𝑋 · (𝑌‘𝑦)) = (𝑋 · (𝑌‘𝑥))) |
17 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐼 ↦ (𝑋 · (𝑌‘𝑦))) = (𝑦 ∈ 𝐼 ↦ (𝑋 · (𝑌‘𝑦))) |
18 | 16, 17 | fvmptg 6189 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐼 ∧ (𝑋 · (𝑌‘𝑥)) ∈ V) → ((𝑦 ∈ 𝐼 ↦ (𝑋 · (𝑌‘𝑦)))‘𝑥) = (𝑋 · (𝑌‘𝑥))) |
19 | 13, 14, 18 | sylancl 693 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑦 ∈ 𝐼 ↦ (𝑋 · (𝑌‘𝑦)))‘𝑥) = (𝑋 · (𝑌‘𝑥))) |
20 | 12, 19 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (((𝐼 × {𝑋}) ∘𝑓 · 𝑌)‘𝑥) = (𝑋 · (𝑌‘𝑥))) |
21 | 20 | neeq1d 2841 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((((𝐼 × {𝑋}) ∘𝑓 · 𝑌)‘𝑥) ≠ 0 ↔ (𝑋 · (𝑌‘𝑥)) ≠ 0 )) |
22 | 21 | rabbidva 3163 |
. . 3
⊢ (𝜑 → {𝑥 ∈ 𝐼 ∣ (((𝐼 × {𝑋}) ∘𝑓 · 𝑌)‘𝑥) ≠ 0 } = {𝑥 ∈ 𝐼 ∣ (𝑋 · (𝑌‘𝑥)) ≠ 0 }) |
23 | | rrgsupp.r |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Ring) |
24 | 23 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ Ring) |
25 | 2 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑋 ∈ 𝐸) |
26 | 8 | ffvelrnda 6267 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑌‘𝑥) ∈ 𝐵) |
27 | | rrgval.e |
. . . . . . 7
⊢ 𝐸 = (RLReg‘𝑅) |
28 | | rrgval.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑅) |
29 | | rrgval.t |
. . . . . . 7
⊢ · =
(.r‘𝑅) |
30 | | rrgval.z |
. . . . . . 7
⊢ 0 =
(0g‘𝑅) |
31 | 27, 28, 29, 30 | rrgeq0 19111 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐸 ∧ (𝑌‘𝑥) ∈ 𝐵) → ((𝑋 · (𝑌‘𝑥)) = 0 ↔ (𝑌‘𝑥) = 0 )) |
32 | 24, 25, 26, 31 | syl3anc 1318 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑋 · (𝑌‘𝑥)) = 0 ↔ (𝑌‘𝑥) = 0 )) |
33 | 32 | necon3bid 2826 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑋 · (𝑌‘𝑥)) ≠ 0 ↔ (𝑌‘𝑥) ≠ 0 )) |
34 | 33 | rabbidva 3163 |
. . 3
⊢ (𝜑 → {𝑥 ∈ 𝐼 ∣ (𝑋 · (𝑌‘𝑥)) ≠ 0 } = {𝑥 ∈ 𝐼 ∣ (𝑌‘𝑥) ≠ 0 }) |
35 | 22, 34 | eqtrd 2644 |
. 2
⊢ (𝜑 → {𝑥 ∈ 𝐼 ∣ (((𝐼 × {𝑋}) ∘𝑓 · 𝑌)‘𝑥) ≠ 0 } = {𝑥 ∈ 𝐼 ∣ (𝑌‘𝑥) ≠ 0 }) |
36 | | ovex 6577 |
. . . . . 6
⊢ (𝑋 · (𝑌‘𝑦)) ∈ V |
37 | 36, 17 | fnmpti 5935 |
. . . . 5
⊢ (𝑦 ∈ 𝐼 ↦ (𝑋 · (𝑌‘𝑦))) Fn 𝐼 |
38 | | fneq1 5893 |
. . . . 5
⊢ (((𝐼 × {𝑋}) ∘𝑓 · 𝑌) = (𝑦 ∈ 𝐼 ↦ (𝑋 · (𝑌‘𝑦))) → (((𝐼 × {𝑋}) ∘𝑓 · 𝑌) Fn 𝐼 ↔ (𝑦 ∈ 𝐼 ↦ (𝑋 · (𝑌‘𝑦))) Fn 𝐼)) |
39 | 37, 38 | mpbiri 247 |
. . . 4
⊢ (((𝐼 × {𝑋}) ∘𝑓 · 𝑌) = (𝑦 ∈ 𝐼 ↦ (𝑋 · (𝑌‘𝑦))) → ((𝐼 × {𝑋}) ∘𝑓 · 𝑌) Fn 𝐼) |
40 | 10, 39 | syl 17 |
. . 3
⊢ (𝜑 → ((𝐼 × {𝑋}) ∘𝑓 · 𝑌) Fn 𝐼) |
41 | | fvex 6113 |
. . . . 5
⊢
(0g‘𝑅) ∈ V |
42 | 30, 41 | eqeltri 2684 |
. . . 4
⊢ 0 ∈
V |
43 | 42 | a1i 11 |
. . 3
⊢ (𝜑 → 0 ∈ V) |
44 | | suppvalfn 7189 |
. . 3
⊢ ((((𝐼 × {𝑋}) ∘𝑓 · 𝑌) Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → (((𝐼 × {𝑋}) ∘𝑓 · 𝑌) supp 0 ) = {𝑥 ∈ 𝐼 ∣ (((𝐼 × {𝑋}) ∘𝑓 · 𝑌)‘𝑥) ≠ 0 }) |
45 | 40, 1, 43, 44 | syl3anc 1318 |
. 2
⊢ (𝜑 → (((𝐼 × {𝑋}) ∘𝑓 · 𝑌) supp 0 ) = {𝑥 ∈ 𝐼 ∣ (((𝐼 × {𝑋}) ∘𝑓 · 𝑌)‘𝑥) ≠ 0 }) |
46 | | ffn 5958 |
. . . 4
⊢ (𝑌:𝐼⟶𝐵 → 𝑌 Fn 𝐼) |
47 | 8, 46 | syl 17 |
. . 3
⊢ (𝜑 → 𝑌 Fn 𝐼) |
48 | | suppvalfn 7189 |
. . 3
⊢ ((𝑌 Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V) → (𝑌 supp 0 ) = {𝑥 ∈ 𝐼 ∣ (𝑌‘𝑥) ≠ 0 }) |
49 | 47, 1, 43, 48 | syl3anc 1318 |
. 2
⊢ (𝜑 → (𝑌 supp 0 ) = {𝑥 ∈ 𝐼 ∣ (𝑌‘𝑥) ≠ 0 }) |
50 | 35, 45, 49 | 3eqtr4d 2654 |
1
⊢ (𝜑 → (((𝐼 × {𝑋}) ∘𝑓 · 𝑌) supp 0 ) = (𝑌 supp 0 )) |