Step | Hyp | Ref
| Expression |
1 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑖(((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦)) |
2 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑗(((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦)) |
3 | | nffvmpt1 6111 |
. . . . . . 7
⊢
Ⅎ𝑥((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) |
4 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑥
· |
5 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑥((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗) |
6 | 3, 4, 5 | nfov 6575 |
. . . . . 6
⊢
Ⅎ𝑥(((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)) |
7 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑦((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) |
8 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑦
· |
9 | | nffvmpt1 6111 |
. . . . . . 7
⊢
Ⅎ𝑦((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗) |
10 | 7, 8, 9 | nfov 6575 |
. . . . . 6
⊢
Ⅎ𝑦(((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)) |
11 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = 𝑖 → ((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) = ((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖)) |
12 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑦 = 𝑗 → ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦) = ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)) |
13 | 11, 12 | oveqan12d 6568 |
. . . . . 6
⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦)) = (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗))) |
14 | 1, 2, 6, 10, 13 | cbvmpt2 6632 |
. . . . 5
⊢ (𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦))) = (𝑖 ∈ 𝐼, 𝑗 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗))) |
15 | | vex 3176 |
. . . . . . . 8
⊢ 𝑖 ∈ V |
16 | | vex 3176 |
. . . . . . . 8
⊢ 𝑗 ∈ V |
17 | 15, 16 | eqop2 7100 |
. . . . . . 7
⊢ (𝑧 = 〈𝑖, 𝑗〉 ↔ (𝑧 ∈ (V × V) ∧ ((1st
‘𝑧) = 𝑖 ∧ (2nd
‘𝑧) = 𝑗))) |
18 | | fveq2 6103 |
. . . . . . . . 9
⊢
((1st ‘𝑧) = 𝑖 → ((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) = ((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖)) |
19 | | fveq2 6103 |
. . . . . . . . 9
⊢
((2nd ‘𝑧) = 𝑗 → ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)) = ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)) |
20 | 18, 19 | oveqan12d 6568 |
. . . . . . . 8
⊢
(((1st ‘𝑧) = 𝑖 ∧ (2nd ‘𝑧) = 𝑗) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))) = (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗))) |
21 | 20 | adantl 481 |
. . . . . . 7
⊢ ((𝑧 ∈ (V × V) ∧
((1st ‘𝑧)
= 𝑖 ∧ (2nd
‘𝑧) = 𝑗)) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))) = (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗))) |
22 | 17, 21 | sylbi 206 |
. . . . . 6
⊢ (𝑧 = 〈𝑖, 𝑗〉 → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))) = (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗))) |
23 | 22 | mpt2mpt 6650 |
. . . . 5
⊢ (𝑧 ∈ (𝐼 × 𝐽) ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)))) = (𝑖 ∈ 𝐼, 𝑗 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗))) |
24 | 14, 23 | eqtr4i 2635 |
. . . 4
⊢ (𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦))) = (𝑧 ∈ (𝐼 × 𝐽) ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)))) |
25 | | simp2 1055 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽) → 𝑥 ∈ 𝐼) |
26 | | evlslem4.x |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑋 ∈ 𝐵) |
27 | 26 | 3adant3 1074 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽) → 𝑋 ∈ 𝐵) |
28 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐼 ↦ 𝑋) = (𝑥 ∈ 𝐼 ↦ 𝑋) |
29 | 28 | fvmpt2 6200 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵) → ((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) = 𝑋) |
30 | 25, 27, 29 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽) → ((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) = 𝑋) |
31 | | simp3 1056 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽) → 𝑦 ∈ 𝐽) |
32 | | evlslem4.y |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → 𝑌 ∈ 𝐵) |
33 | 32 | 3adant2 1073 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽) → 𝑌 ∈ 𝐵) |
34 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐽 ↦ 𝑌) = (𝑦 ∈ 𝐽 ↦ 𝑌) |
35 | 34 | fvmpt2 6200 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐽 ∧ 𝑌 ∈ 𝐵) → ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦) = 𝑌) |
36 | 31, 33, 35 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽) → ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦) = 𝑌) |
37 | 30, 36 | oveq12d 6567 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦)) = (𝑋 · 𝑌)) |
38 | 37 | mpt2eq3dva 6617 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦))) = (𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (𝑋 · 𝑌))) |
39 | 24, 38 | syl5reqr 2659 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (𝑋 · 𝑌)) = (𝑧 ∈ (𝐼 × 𝐽) ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))))) |
40 | 39 | oveq1d 6564 |
. 2
⊢ (𝜑 → ((𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (𝑋 · 𝑌)) supp 0 ) = ((𝑧 ∈ (𝐼 × 𝐽) ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)))) supp 0 )) |
41 | | difxp 5477 |
. . . . . 6
⊢ ((𝐼 × 𝐽) ∖ (((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) × ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) = (((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽) ∪ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )))) |
42 | 41 | eleq2i 2680 |
. . . . 5
⊢ (𝑧 ∈ ((𝐼 × 𝐽) ∖ (((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) × ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) ↔ 𝑧 ∈ (((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽) ∪ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))))) |
43 | | elun 3715 |
. . . . 5
⊢ (𝑧 ∈ (((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽) ∪ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )))) ↔ (𝑧 ∈ ((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽) ∨ 𝑧 ∈ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))))) |
44 | 42, 43 | bitri 263 |
. . . 4
⊢ (𝑧 ∈ ((𝐼 × 𝐽) ∖ (((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) × ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) ↔ (𝑧 ∈ ((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽) ∨ 𝑧 ∈ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))))) |
45 | | xp1st 7089 |
. . . . . . . 8
⊢ (𝑧 ∈ ((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽) → (1st
‘𝑧) ∈ (𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ))) |
46 | 26, 28 | fmptd 6292 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝑋):𝐼⟶𝐵) |
47 | | ssid 3587 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) ⊆ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) |
48 | 47 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) ⊆ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) |
49 | | evlslem4.i |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
50 | | evlslem4.z |
. . . . . . . . . . 11
⊢ 0 =
(0g‘𝑅) |
51 | | fvex 6113 |
. . . . . . . . . . 11
⊢
(0g‘𝑅) ∈ V |
52 | 50, 51 | eqeltri 2684 |
. . . . . . . . . 10
⊢ 0 ∈
V |
53 | 52 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈ V) |
54 | 46, 48, 49, 53 | suppssr 7213 |
. . . . . . . 8
⊢ ((𝜑 ∧ (1st
‘𝑧) ∈ (𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ))) → ((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) = 0 ) |
55 | 45, 54 | sylan2 490 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽)) → ((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) = 0 ) |
56 | 55 | oveq1d 6564 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽)) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))) = ( 0 · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)))) |
57 | | evlslem4.r |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ Ring) |
58 | 57 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽)) → 𝑅 ∈ Ring) |
59 | 32, 34 | fmptd 6292 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ 𝑌):𝐽⟶𝐵) |
60 | | xp2nd 7090 |
. . . . . . . 8
⊢ (𝑧 ∈ ((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽) → (2nd
‘𝑧) ∈ 𝐽) |
61 | | ffvelrn 6265 |
. . . . . . . 8
⊢ (((𝑦 ∈ 𝐽 ↦ 𝑌):𝐽⟶𝐵 ∧ (2nd ‘𝑧) ∈ 𝐽) → ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)) ∈ 𝐵) |
62 | 59, 60, 61 | syl2an 493 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽)) → ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)) ∈ 𝐵) |
63 | | evlslem4.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑅) |
64 | | evlslem4.t |
. . . . . . . 8
⊢ · =
(.r‘𝑅) |
65 | 63, 64, 50 | ringlz 18410 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)) ∈ 𝐵) → ( 0 · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))) = 0 ) |
66 | 58, 62, 65 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽)) → ( 0 · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))) = 0 ) |
67 | 56, 66 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽)) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))) = 0 ) |
68 | | xp2nd 7090 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) → (2nd
‘𝑧) ∈ (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) |
69 | | ssid 3587 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ) ⊆ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ) |
70 | 69 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ) ⊆ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )) |
71 | | evlslem4.j |
. . . . . . . . 9
⊢ (𝜑 → 𝐽 ∈ 𝑊) |
72 | 59, 70, 71, 53 | suppssr 7213 |
. . . . . . . 8
⊢ ((𝜑 ∧ (2nd
‘𝑧) ∈ (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) → ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)) = 0 ) |
73 | 68, 72 | sylan2 490 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )))) → ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)) = 0 ) |
74 | 73 | oveq2d 6565 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )))) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))) = (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · 0 )) |
75 | 57 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )))) → 𝑅 ∈ Ring) |
76 | | xp1st 7089 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) → (1st
‘𝑧) ∈ 𝐼) |
77 | | ffvelrn 6265 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐼 ↦ 𝑋):𝐼⟶𝐵 ∧ (1st ‘𝑧) ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) ∈ 𝐵) |
78 | 46, 76, 77 | syl2an 493 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )))) → ((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) ∈ 𝐵) |
79 | 63, 64, 50 | ringrz 18411 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ ((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) ∈ 𝐵) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · 0 ) = 0 ) |
80 | 75, 78, 79 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )))) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · 0 ) = 0 ) |
81 | 74, 80 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )))) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))) = 0 ) |
82 | 67, 81 | jaodan 822 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽) ∨ 𝑧 ∈ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))))) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))) = 0 ) |
83 | 44, 82 | sylan2b 491 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐼 × 𝐽) ∖ (((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) × ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )))) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))) = 0 ) |
84 | | xpexg 6858 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → (𝐼 × 𝐽) ∈ V) |
85 | 49, 71, 84 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝐼 × 𝐽) ∈ V) |
86 | 83, 85 | suppss2 7216 |
. 2
⊢ (𝜑 → ((𝑧 ∈ (𝐼 × 𝐽) ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)))) supp 0 ) ⊆ (((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) × ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) |
87 | 40, 86 | eqsstrd 3602 |
1
⊢ (𝜑 → ((𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (𝑋 · 𝑌)) supp 0 ) ⊆ (((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) × ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) |