Step | Hyp | Ref
| Expression |
1 | | gsumdixp.b |
. . . 4
⊢ 𝐵 = (Base‘𝑅) |
2 | | gsumdixp.z |
. . . 4
⊢ 0 =
(0g‘𝑅) |
3 | | gsumdixp.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ Ring) |
4 | 3 | ringcmnd 20173 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ CMnd) |
5 | | gsumdixp.i |
. . . 4
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
6 | | gsumdixp.j |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ 𝑊) |
7 | 6 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → 𝐽 ∈ 𝑊) |
8 | | gsumdixp.t |
. . . . 5
⊢ · =
(.r‘𝑅) |
9 | 3 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽)) → 𝑅 ∈ Ring) |
10 | | gsumdixp.x |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑋 ∈ 𝐵) |
11 | 10 | fmpttd 7116 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝑋):𝐼⟶𝐵) |
12 | | simpl 482 |
. . . . . 6
⊢ ((𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽) → 𝑖 ∈ 𝐼) |
13 | | ffvelcdm 7083 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐼 ↦ 𝑋):𝐼⟶𝐵 ∧ 𝑖 ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) ∈ 𝐵) |
14 | 11, 12, 13 | syl2an 595 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽)) → ((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) ∈ 𝐵) |
15 | | gsumdixp.y |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → 𝑌 ∈ 𝐵) |
16 | 15 | fmpttd 7116 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ 𝑌):𝐽⟶𝐵) |
17 | | simpr 484 |
. . . . . 6
⊢ ((𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽) → 𝑗 ∈ 𝐽) |
18 | | ffvelcdm 7083 |
. . . . . 6
⊢ (((𝑦 ∈ 𝐽 ↦ 𝑌):𝐽⟶𝐵 ∧ 𝑗 ∈ 𝐽) → ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗) ∈ 𝐵) |
19 | 16, 17, 18 | syl2an 595 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽)) → ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗) ∈ 𝐵) |
20 | 1, 8, 9, 14, 19 | ringcld 20152 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽)) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)) ∈ 𝐵) |
21 | | gsumdixp.xf |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝑋) finSupp 0 ) |
22 | 21 | fsuppimpd 9373 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) ∈
Fin) |
23 | | gsumdixp.yf |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ 𝑌) finSupp 0 ) |
24 | 23 | fsuppimpd 9373 |
. . . . 5
⊢ (𝜑 → ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ) ∈
Fin) |
25 | | xpfi 9321 |
. . . . 5
⊢ ((((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) ∈ Fin ∧ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ) ∈ Fin) →
(((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) × ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )) ∈
Fin) |
26 | 22, 24, 25 | syl2anc 583 |
. . . 4
⊢ (𝜑 → (((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) × ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )) ∈
Fin) |
27 | | ianor 979 |
. . . . . . 7
⊢ (¬
(𝑖 ∈ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) ∧ 𝑗 ∈ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )) ↔ (¬ 𝑖 ∈ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) ∨ ¬ 𝑗 ∈ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) |
28 | | brxp 5725 |
. . . . . . 7
⊢ (𝑖(((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) × ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))𝑗 ↔ (𝑖 ∈ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) ∧ 𝑗 ∈ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) |
29 | 27, 28 | xchnxbir 333 |
. . . . . 6
⊢ (¬
𝑖(((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) × ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))𝑗 ↔ (¬ 𝑖 ∈ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) ∨ ¬ 𝑗 ∈ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) |
30 | | simprl 768 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽)) → 𝑖 ∈ 𝐼) |
31 | | eldif 3958 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) ↔ (𝑖 ∈ 𝐼 ∧ ¬ 𝑖 ∈ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ))) |
32 | 31 | biimpri 227 |
. . . . . . . . . . 11
⊢ ((𝑖 ∈ 𝐼 ∧ ¬ 𝑖 ∈ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) → 𝑖 ∈ (𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ))) |
33 | 30, 32 | sylan 579 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽)) ∧ ¬ 𝑖 ∈ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) → 𝑖 ∈ (𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ))) |
34 | 11 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽)) → (𝑥 ∈ 𝐼 ↦ 𝑋):𝐼⟶𝐵) |
35 | | ssidd 4005 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽)) → ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) ⊆ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) |
36 | 5 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽)) → 𝐼 ∈ 𝑉) |
37 | 2 | fvexi 6905 |
. . . . . . . . . . . 12
⊢ 0 ∈
V |
38 | 37 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽)) → 0 ∈ V) |
39 | 34, 35, 36, 38 | suppssr 8185 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽)) ∧ 𝑖 ∈ (𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ))) → ((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) = 0 ) |
40 | 33, 39 | syldan 590 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽)) ∧ ¬ 𝑖 ∈ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) → ((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) = 0 ) |
41 | 40 | oveq1d 7427 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽)) ∧ ¬ 𝑖 ∈ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)) = ( 0 · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗))) |
42 | 1, 8, 2 | ringlz 20182 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗) ∈ 𝐵) → ( 0 · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)) = 0 ) |
43 | 9, 19, 42 | syl2anc 583 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽)) → ( 0 · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)) = 0 ) |
44 | 43 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽)) ∧ ¬ 𝑖 ∈ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) → ( 0 ·
((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)) = 0 ) |
45 | 41, 44 | eqtrd 2771 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽)) ∧ ¬ 𝑖 ∈ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)) = 0 ) |
46 | | simprr 770 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽)) → 𝑗 ∈ 𝐽) |
47 | | eldif 3958 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )) ↔ (𝑗 ∈ 𝐽 ∧ ¬ 𝑗 ∈ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) |
48 | 47 | biimpri 227 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ 𝐽 ∧ ¬ 𝑗 ∈ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )) → 𝑗 ∈ (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) |
49 | 46, 48 | sylan 579 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽)) ∧ ¬ 𝑗 ∈ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )) → 𝑗 ∈ (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) |
50 | 16 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽)) → (𝑦 ∈ 𝐽 ↦ 𝑌):𝐽⟶𝐵) |
51 | | ssidd 4005 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽)) → ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ) ⊆ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )) |
52 | 6 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽)) → 𝐽 ∈ 𝑊) |
53 | 50, 51, 52, 38 | suppssr 8185 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽)) ∧ 𝑗 ∈ (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) → ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗) = 0 ) |
54 | 49, 53 | syldan 590 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽)) ∧ ¬ 𝑗 ∈ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )) → ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗) = 0 ) |
55 | 54 | oveq2d 7428 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽)) ∧ ¬ 𝑗 ∈ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)) = (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · 0 )) |
56 | 1, 8, 2 | ringrz 20183 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ Ring ∧ ((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) ∈ 𝐵) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · 0 ) = 0 ) |
57 | 9, 14, 56 | syl2anc 583 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽)) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · 0 ) = 0 ) |
58 | 57 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽)) ∧ ¬ 𝑗 ∈ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · 0 ) = 0 ) |
59 | 55, 58 | eqtrd 2771 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽)) ∧ ¬ 𝑗 ∈ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)) = 0 ) |
60 | 45, 59 | jaodan 955 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽)) ∧ (¬ 𝑖 ∈ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) ∨ ¬ 𝑗 ∈ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)) = 0 ) |
61 | 29, 60 | sylan2b 593 |
. . . . 5
⊢ (((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽)) ∧ ¬ 𝑖(((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) × ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))𝑗) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)) = 0 ) |
62 | 61 | anasss 466 |
. . . 4
⊢ ((𝜑 ∧ ((𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽) ∧ ¬ 𝑖(((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) × ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))𝑗)) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)) = 0 ) |
63 | 1, 2, 4, 5, 7, 20,
26, 62 | gsum2d2 19884 |
. . 3
⊢ (𝜑 → (𝑅 Σg (𝑖 ∈ 𝐼, 𝑗 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)))) = (𝑅 Σg (𝑖 ∈ 𝐼 ↦ (𝑅 Σg (𝑗 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗))))))) |
64 | | nffvmpt1 6902 |
. . . . . . 7
⊢
Ⅎ𝑥((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) |
65 | | nfcv 2902 |
. . . . . . 7
⊢
Ⅎ𝑥
· |
66 | | nfcv 2902 |
. . . . . . 7
⊢
Ⅎ𝑥((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗) |
67 | 64, 65, 66 | nfov 7442 |
. . . . . 6
⊢
Ⅎ𝑥(((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)) |
68 | | nfcv 2902 |
. . . . . . 7
⊢
Ⅎ𝑦((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) |
69 | | nfcv 2902 |
. . . . . . 7
⊢
Ⅎ𝑦
· |
70 | | nffvmpt1 6902 |
. . . . . . 7
⊢
Ⅎ𝑦((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗) |
71 | 68, 69, 70 | nfov 7442 |
. . . . . 6
⊢
Ⅎ𝑦(((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)) |
72 | | nfcv 2902 |
. . . . . 6
⊢
Ⅎ𝑖(((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦)) |
73 | | nfcv 2902 |
. . . . . 6
⊢
Ⅎ𝑗(((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦)) |
74 | | fveq2 6891 |
. . . . . . 7
⊢ (𝑖 = 𝑥 → ((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) = ((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥)) |
75 | | fveq2 6891 |
. . . . . . 7
⊢ (𝑗 = 𝑦 → ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗) = ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦)) |
76 | 74, 75 | oveqan12d 7431 |
. . . . . 6
⊢ ((𝑖 = 𝑥 ∧ 𝑗 = 𝑦) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)) = (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦))) |
77 | 67, 71, 72, 73, 76 | cbvmpo 7506 |
. . . . 5
⊢ (𝑖 ∈ 𝐼, 𝑗 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗))) = (𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦))) |
78 | | simp2 1136 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽) → 𝑥 ∈ 𝐼) |
79 | 10 | 3adant3 1131 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽) → 𝑋 ∈ 𝐵) |
80 | | eqid 2731 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐼 ↦ 𝑋) = (𝑥 ∈ 𝐼 ↦ 𝑋) |
81 | 80 | fvmpt2 7009 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵) → ((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) = 𝑋) |
82 | 78, 79, 81 | syl2anc 583 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽) → ((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) = 𝑋) |
83 | | simp3 1137 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽) → 𝑦 ∈ 𝐽) |
84 | | eqid 2731 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐽 ↦ 𝑌) = (𝑦 ∈ 𝐽 ↦ 𝑌) |
85 | 84 | fvmpt2 7009 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝐽 ∧ 𝑌 ∈ 𝐵) → ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦) = 𝑌) |
86 | 83, 15, 85 | 3imp3i2an 1344 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽) → ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦) = 𝑌) |
87 | 82, 86 | oveq12d 7430 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦)) = (𝑋 · 𝑌)) |
88 | 87 | mpoeq3dva 7489 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦))) = (𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (𝑋 · 𝑌))) |
89 | 77, 88 | eqtrid 2783 |
. . . 4
⊢ (𝜑 → (𝑖 ∈ 𝐼, 𝑗 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗))) = (𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (𝑋 · 𝑌))) |
90 | 89 | oveq2d 7428 |
. . 3
⊢ (𝜑 → (𝑅 Σg (𝑖 ∈ 𝐼, 𝑗 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)))) = (𝑅 Σg (𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (𝑋 · 𝑌)))) |
91 | | nfcv 2902 |
. . . . . . 7
⊢
Ⅎ𝑥𝑅 |
92 | | nfcv 2902 |
. . . . . . 7
⊢
Ⅎ𝑥
Σg |
93 | | nfcv 2902 |
. . . . . . . 8
⊢
Ⅎ𝑥𝐽 |
94 | 93, 67 | nfmpt 5255 |
. . . . . . 7
⊢
Ⅎ𝑥(𝑗 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗))) |
95 | 91, 92, 94 | nfov 7442 |
. . . . . 6
⊢
Ⅎ𝑥(𝑅 Σg (𝑗 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)))) |
96 | | nfcv 2902 |
. . . . . 6
⊢
Ⅎ𝑖(𝑅 Σg (𝑦 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦)))) |
97 | 74 | oveq1d 7427 |
. . . . . . . . 9
⊢ (𝑖 = 𝑥 → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)) = (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗))) |
98 | 97 | mpteq2dv 5250 |
. . . . . . . 8
⊢ (𝑖 = 𝑥 → (𝑗 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗))) = (𝑗 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)))) |
99 | | nfcv 2902 |
. . . . . . . . . 10
⊢
Ⅎ𝑦((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) |
100 | 99, 69, 70 | nfov 7442 |
. . . . . . . . 9
⊢
Ⅎ𝑦(((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)) |
101 | 75 | oveq2d 7428 |
. . . . . . . . 9
⊢ (𝑗 = 𝑦 → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)) = (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦))) |
102 | 100, 73, 101 | cbvmpt 5259 |
. . . . . . . 8
⊢ (𝑗 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗))) = (𝑦 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦))) |
103 | 98, 102 | eqtrdi 2787 |
. . . . . . 7
⊢ (𝑖 = 𝑥 → (𝑗 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗))) = (𝑦 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦)))) |
104 | 103 | oveq2d 7428 |
. . . . . 6
⊢ (𝑖 = 𝑥 → (𝑅 Σg (𝑗 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)))) = (𝑅 Σg (𝑦 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦))))) |
105 | 95, 96, 104 | cbvmpt 5259 |
. . . . 5
⊢ (𝑖 ∈ 𝐼 ↦ (𝑅 Σg (𝑗 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗))))) = (𝑥 ∈ 𝐼 ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦))))) |
106 | 87 | 3expa 1117 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐽) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦)) = (𝑋 · 𝑌)) |
107 | 106 | mpteq2dva 5248 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑦 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦))) = (𝑦 ∈ 𝐽 ↦ (𝑋 · 𝑌))) |
108 | 107 | oveq2d 7428 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑅 Σg (𝑦 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦)))) = (𝑅 Σg (𝑦 ∈ 𝐽 ↦ (𝑋 · 𝑌)))) |
109 | 108 | mpteq2dva 5248 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦))))) = (𝑥 ∈ 𝐼 ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ (𝑋 · 𝑌))))) |
110 | 105, 109 | eqtrid 2783 |
. . . 4
⊢ (𝜑 → (𝑖 ∈ 𝐼 ↦ (𝑅 Σg (𝑗 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗))))) = (𝑥 ∈ 𝐼 ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ (𝑋 · 𝑌))))) |
111 | 110 | oveq2d 7428 |
. . 3
⊢ (𝜑 → (𝑅 Σg (𝑖 ∈ 𝐼 ↦ (𝑅 Σg (𝑗 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)))))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ (𝑋 · 𝑌)))))) |
112 | 63, 90, 111 | 3eqtr3d 2779 |
. 2
⊢ (𝜑 → (𝑅 Σg (𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (𝑋 · 𝑌))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ (𝑋 · 𝑌)))))) |
113 | 3 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ Ring) |
114 | 6 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐽 ∈ 𝑊) |
115 | 15 | adantlr 712 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐼) ∧ 𝑦 ∈ 𝐽) → 𝑌 ∈ 𝐵) |
116 | 23 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑦 ∈ 𝐽 ↦ 𝑌) finSupp 0 ) |
117 | 1, 2, 8, 113, 114, 10, 115, 116 | gsummulc2 20206 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑅 Σg (𝑦 ∈ 𝐽 ↦ (𝑋 · 𝑌))) = (𝑋 · (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑌)))) |
118 | 117 | mpteq2dva 5248 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ (𝑋 · 𝑌)))) = (𝑥 ∈ 𝐼 ↦ (𝑋 · (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑌))))) |
119 | 118 | oveq2d 7428 |
. 2
⊢ (𝜑 → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ (𝑋 · 𝑌))))) = (𝑅 Σg (𝑥 ∈ 𝐼 ↦ (𝑋 · (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑌)))))) |
120 | 1, 2, 4, 6, 16, 23 | gsumcl 19825 |
. . 3
⊢ (𝜑 → (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑌)) ∈ 𝐵) |
121 | 1, 2, 8, 3, 5, 120, 10, 21 | gsummulc1 20205 |
. 2
⊢ (𝜑 → (𝑅 Σg (𝑥 ∈ 𝐼 ↦ (𝑋 · (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑌))))) = ((𝑅 Σg (𝑥 ∈ 𝐼 ↦ 𝑋)) · (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑌)))) |
122 | 112, 119,
121 | 3eqtrrd 2776 |
1
⊢ (𝜑 → ((𝑅 Σg (𝑥 ∈ 𝐼 ↦ 𝑋)) · (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑌))) = (𝑅 Σg (𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (𝑋 · 𝑌)))) |