Step | Hyp | Ref
| Expression |
1 | | eqid 2732 |
. . 3
β’
((ordTopβ β€ ) βΎt (0[,]+β)) =
((ordTopβ β€ ) βΎt (0[,]+β)) |
2 | | esummulc2.a |
. . 3
β’ (π β π΄ β π) |
3 | | esummulc2.b |
. . 3
β’ ((π β§ π β π΄) β π΅ β (0[,]+β)) |
4 | | eqid 2732 |
. . . 4
β’ (π§ β (0[,]+β) β¦
(π§ Β·e
πΆ)) = (π§ β (0[,]+β) β¦ (π§ Β·e πΆ)) |
5 | | esummulc2.c |
. . . 4
β’ (π β πΆ β (0[,)+β)) |
6 | 1, 4, 5 | xrge0mulc1cn 32916 |
. . 3
β’ (π β (π§ β (0[,]+β) β¦ (π§ Β·e πΆ)) β (((ordTopβ β€
) βΎt (0[,]+β)) Cn ((ordTopβ β€ )
βΎt (0[,]+β)))) |
7 | | eqidd 2733 |
. . . 4
β’ (π β (π§ β (0[,]+β) β¦ (π§ Β·e πΆ)) = (π§ β (0[,]+β) β¦ (π§ Β·e πΆ))) |
8 | | oveq1 7415 |
. . . . 5
β’ (π§ = 0 β (π§ Β·e πΆ) = (0 Β·e πΆ)) |
9 | | icossxr 13408 |
. . . . . . 7
β’
(0[,)+β) β β* |
10 | 9, 5 | sselid 3980 |
. . . . . 6
β’ (π β πΆ β
β*) |
11 | | xmul02 13246 |
. . . . . 6
β’ (πΆ β β*
β (0 Β·e πΆ) = 0) |
12 | 10, 11 | syl 17 |
. . . . 5
β’ (π β (0 Β·e
πΆ) = 0) |
13 | 8, 12 | sylan9eqr 2794 |
. . . 4
β’ ((π β§ π§ = 0) β (π§ Β·e πΆ) = 0) |
14 | | 0e0iccpnf 13435 |
. . . . 5
β’ 0 β
(0[,]+β) |
15 | 14 | a1i 11 |
. . . 4
β’ (π β 0 β
(0[,]+β)) |
16 | 7, 13, 15, 15 | fvmptd 7005 |
. . 3
β’ (π β ((π§ β (0[,]+β) β¦ (π§ Β·e πΆ))β0) =
0) |
17 | | simp2 1137 |
. . . . 5
β’ ((π β§ π₯ β (0[,]+β) β§ π¦ β (0[,]+β)) β
π₯ β
(0[,]+β)) |
18 | | simp3 1138 |
. . . . 5
β’ ((π β§ π₯ β (0[,]+β) β§ π¦ β (0[,]+β)) β
π¦ β
(0[,]+β)) |
19 | | icossicc 13412 |
. . . . . 6
β’
(0[,)+β) β (0[,]+β) |
20 | 5 | 3ad2ant1 1133 |
. . . . . 6
β’ ((π β§ π₯ β (0[,]+β) β§ π¦ β (0[,]+β)) β
πΆ β
(0[,)+β)) |
21 | 19, 20 | sselid 3980 |
. . . . 5
β’ ((π β§ π₯ β (0[,]+β) β§ π¦ β (0[,]+β)) β
πΆ β
(0[,]+β)) |
22 | | xrge0adddir 32188 |
. . . . 5
β’ ((π₯ β (0[,]+β) β§
π¦ β (0[,]+β)
β§ πΆ β
(0[,]+β)) β ((π₯
+π π¦)
Β·e πΆ) =
((π₯ Β·e
πΆ) +π
(π¦ Β·e
πΆ))) |
23 | 17, 18, 21, 22 | syl3anc 1371 |
. . . 4
β’ ((π β§ π₯ β (0[,]+β) β§ π¦ β (0[,]+β)) β
((π₯ +π
π¦) Β·e
πΆ) = ((π₯ Β·e πΆ) +π (π¦ Β·e πΆ))) |
24 | | eqidd 2733 |
. . . . 5
β’ ((π β§ π₯ β (0[,]+β) β§ π¦ β (0[,]+β)) β
(π§ β (0[,]+β)
β¦ (π§
Β·e πΆ)) =
(π§ β (0[,]+β)
β¦ (π§
Β·e πΆ))) |
25 | | simpr 485 |
. . . . . 6
β’ (((π β§ π₯ β (0[,]+β) β§ π¦ β (0[,]+β)) β§
π§ = (π₯ +π π¦)) β π§ = (π₯ +π π¦)) |
26 | 25 | oveq1d 7423 |
. . . . 5
β’ (((π β§ π₯ β (0[,]+β) β§ π¦ β (0[,]+β)) β§
π§ = (π₯ +π π¦)) β (π§ Β·e πΆ) = ((π₯ +π π¦) Β·e πΆ)) |
27 | | ge0xaddcl 13438 |
. . . . . 6
β’ ((π₯ β (0[,]+β) β§
π¦ β (0[,]+β))
β (π₯
+π π¦)
β (0[,]+β)) |
28 | 27 | 3adant1 1130 |
. . . . 5
β’ ((π β§ π₯ β (0[,]+β) β§ π¦ β (0[,]+β)) β
(π₯ +π
π¦) β
(0[,]+β)) |
29 | | ovexd 7443 |
. . . . 5
β’ ((π β§ π₯ β (0[,]+β) β§ π¦ β (0[,]+β)) β
((π₯ +π
π¦) Β·e
πΆ) β
V) |
30 | 24, 26, 28, 29 | fvmptd 7005 |
. . . 4
β’ ((π β§ π₯ β (0[,]+β) β§ π¦ β (0[,]+β)) β
((π§ β (0[,]+β)
β¦ (π§
Β·e πΆ))β(π₯ +π π¦)) = ((π₯ +π π¦) Β·e πΆ)) |
31 | | simpr 485 |
. . . . . . 7
β’ (((π β§ π₯ β (0[,]+β) β§ π¦ β (0[,]+β)) β§
π§ = π₯) β π§ = π₯) |
32 | 31 | oveq1d 7423 |
. . . . . 6
β’ (((π β§ π₯ β (0[,]+β) β§ π¦ β (0[,]+β)) β§
π§ = π₯) β (π§ Β·e πΆ) = (π₯ Β·e πΆ)) |
33 | | ovexd 7443 |
. . . . . 6
β’ ((π β§ π₯ β (0[,]+β) β§ π¦ β (0[,]+β)) β
(π₯ Β·e
πΆ) β
V) |
34 | 24, 32, 17, 33 | fvmptd 7005 |
. . . . 5
β’ ((π β§ π₯ β (0[,]+β) β§ π¦ β (0[,]+β)) β
((π§ β (0[,]+β)
β¦ (π§
Β·e πΆ))βπ₯) = (π₯ Β·e πΆ)) |
35 | | simpr 485 |
. . . . . . 7
β’ (((π β§ π₯ β (0[,]+β) β§ π¦ β (0[,]+β)) β§
π§ = π¦) β π§ = π¦) |
36 | 35 | oveq1d 7423 |
. . . . . 6
β’ (((π β§ π₯ β (0[,]+β) β§ π¦ β (0[,]+β)) β§
π§ = π¦) β (π§ Β·e πΆ) = (π¦ Β·e πΆ)) |
37 | | ovexd 7443 |
. . . . . 6
β’ ((π β§ π₯ β (0[,]+β) β§ π¦ β (0[,]+β)) β
(π¦ Β·e
πΆ) β
V) |
38 | 24, 36, 18, 37 | fvmptd 7005 |
. . . . 5
β’ ((π β§ π₯ β (0[,]+β) β§ π¦ β (0[,]+β)) β
((π§ β (0[,]+β)
β¦ (π§
Β·e πΆ))βπ¦) = (π¦ Β·e πΆ)) |
39 | 34, 38 | oveq12d 7426 |
. . . 4
β’ ((π β§ π₯ β (0[,]+β) β§ π¦ β (0[,]+β)) β
(((π§ β (0[,]+β)
β¦ (π§
Β·e πΆ))βπ₯) +π ((π§ β (0[,]+β) β¦ (π§ Β·e πΆ))βπ¦)) = ((π₯ Β·e πΆ) +π (π¦ Β·e πΆ))) |
40 | 23, 30, 39 | 3eqtr4d 2782 |
. . 3
β’ ((π β§ π₯ β (0[,]+β) β§ π¦ β (0[,]+β)) β
((π§ β (0[,]+β)
β¦ (π§
Β·e πΆ))β(π₯ +π π¦)) = (((π§ β (0[,]+β) β¦ (π§ Β·e πΆ))βπ₯) +π ((π§ β (0[,]+β) β¦ (π§ Β·e πΆ))βπ¦))) |
41 | 1, 2, 3, 6, 16, 40 | esumcocn 33073 |
. 2
β’ (π β ((π§ β (0[,]+β) β¦ (π§ Β·e πΆ))βΞ£*π β π΄π΅) = Ξ£*π β π΄((π§ β (0[,]+β) β¦ (π§ Β·e πΆ))βπ΅)) |
42 | | simpr 485 |
. . . 4
β’ ((π β§ π§ = Ξ£*π β π΄π΅) β π§ = Ξ£*π β π΄π΅) |
43 | 42 | oveq1d 7423 |
. . 3
β’ ((π β§ π§ = Ξ£*π β π΄π΅) β (π§ Β·e πΆ) = (Ξ£*π β π΄π΅ Β·e πΆ)) |
44 | 3 | ralrimiva 3146 |
. . . 4
β’ (π β βπ β π΄ π΅ β (0[,]+β)) |
45 | | nfcv 2903 |
. . . . 5
β’
β²ππ΄ |
46 | 45 | esumcl 33023 |
. . . 4
β’ ((π΄ β π β§ βπ β π΄ π΅ β (0[,]+β)) β
Ξ£*π β
π΄π΅ β (0[,]+β)) |
47 | 2, 44, 46 | syl2anc 584 |
. . 3
β’ (π β Ξ£*π β π΄π΅ β (0[,]+β)) |
48 | | ovexd 7443 |
. . 3
β’ (π β (Ξ£*π β π΄π΅ Β·e πΆ) β V) |
49 | 7, 43, 47, 48 | fvmptd 7005 |
. 2
β’ (π β ((π§ β (0[,]+β) β¦ (π§ Β·e πΆ))βΞ£*π β π΄π΅) = (Ξ£*π β π΄π΅ Β·e πΆ)) |
50 | | eqidd 2733 |
. . . 4
β’ ((π β§ π β π΄) β (π§ β (0[,]+β) β¦ (π§ Β·e πΆ)) = (π§ β (0[,]+β) β¦ (π§ Β·e πΆ))) |
51 | | simpr 485 |
. . . . 5
β’ (((π β§ π β π΄) β§ π§ = π΅) β π§ = π΅) |
52 | 51 | oveq1d 7423 |
. . . 4
β’ (((π β§ π β π΄) β§ π§ = π΅) β (π§ Β·e πΆ) = (π΅ Β·e πΆ)) |
53 | | ovexd 7443 |
. . . 4
β’ ((π β§ π β π΄) β (π΅ Β·e πΆ) β V) |
54 | 50, 52, 3, 53 | fvmptd 7005 |
. . 3
β’ ((π β§ π β π΄) β ((π§ β (0[,]+β) β¦ (π§ Β·e πΆ))βπ΅) = (π΅ Β·e πΆ)) |
55 | 54 | esumeq2dv 33031 |
. 2
β’ (π β Ξ£*π β π΄((π§ β (0[,]+β) β¦ (π§ Β·e πΆ))βπ΅) = Ξ£*π β π΄(π΅ Β·e πΆ)) |
56 | 41, 49, 55 | 3eqtr3d 2780 |
1
β’ (π β (Ξ£*π β π΄π΅ Β·e πΆ) = Ξ£*π β π΄(π΅ Β·e πΆ)) |