Step | Hyp | Ref
| Expression |
1 | | rrxmval.d |
. . . . 5
β’ π· =
(distβ(β^βπΌ)) |
2 | | eqid 2732 |
. . . . . 6
β’
(β^βπΌ) =
(β^βπΌ) |
3 | | eqid 2732 |
. . . . . 6
β’
(Baseβ(β^βπΌ)) = (Baseβ(β^βπΌ)) |
4 | 2, 3 | rrxds 25134 |
. . . . 5
β’ (πΌ β π β (π β (Baseβ(β^βπΌ)), π β (Baseβ(β^βπΌ)) β¦
(ββ(βfld Ξ£g (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2))))) =
(distβ(β^βπΌ))) |
5 | 1, 4 | eqtr4id 2791 |
. . . 4
β’ (πΌ β π β π· = (π β (Baseβ(β^βπΌ)), π β (Baseβ(β^βπΌ)) β¦
(ββ(βfld Ξ£g (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2)))))) |
6 | | rrxmval.1 |
. . . . . 6
β’ π = {β β (β βm πΌ) β£ β finSupp 0} |
7 | 2, 3 | rrxbase 25129 |
. . . . . 6
β’ (πΌ β π β (Baseβ(β^βπΌ)) = {β β (β βm πΌ) β£ β finSupp 0}) |
8 | 6, 7 | eqtr4id 2791 |
. . . . 5
β’ (πΌ β π β π = (Baseβ(β^βπΌ))) |
9 | | mpoeq12 7484 |
. . . . 5
β’ ((π =
(Baseβ(β^βπΌ)) β§ π = (Baseβ(β^βπΌ))) β (π β π, π β π β¦
(ββ(βfld Ξ£g (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2))))) = (π β (Baseβ(β^βπΌ)), π β (Baseβ(β^βπΌ)) β¦
(ββ(βfld Ξ£g (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2)))))) |
10 | 8, 8, 9 | syl2anc 584 |
. . . 4
β’ (πΌ β π β (π β π, π β π β¦
(ββ(βfld Ξ£g (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2))))) = (π β (Baseβ(β^βπΌ)), π β (Baseβ(β^βπΌ)) β¦
(ββ(βfld Ξ£g (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2)))))) |
11 | 5, 10 | eqtr4d 2775 |
. . 3
β’ (πΌ β π β π· = (π β π, π β π β¦
(ββ(βfld Ξ£g (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2)))))) |
12 | 11 | 3ad2ant1 1133 |
. 2
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β π· = (π β π, π β π β¦
(ββ(βfld Ξ£g (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2)))))) |
13 | | simprl 769 |
. . . . . . . . 9
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ (π = πΉ β§ π = πΊ)) β π = πΉ) |
14 | 13 | fveq1d 6893 |
. . . . . . . 8
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ (π = πΉ β§ π = πΊ)) β (πβπ₯) = (πΉβπ₯)) |
15 | | simprr 771 |
. . . . . . . . 9
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ (π = πΉ β§ π = πΊ)) β π = πΊ) |
16 | 15 | fveq1d 6893 |
. . . . . . . 8
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ (π = πΉ β§ π = πΊ)) β (πβπ₯) = (πΊβπ₯)) |
17 | 14, 16 | oveq12d 7429 |
. . . . . . 7
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ (π = πΉ β§ π = πΊ)) β ((πβπ₯) β (πβπ₯)) = ((πΉβπ₯) β (πΊβπ₯))) |
18 | 17 | oveq1d 7426 |
. . . . . 6
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ (π = πΉ β§ π = πΊ)) β (((πβπ₯) β (πβπ₯))β2) = (((πΉβπ₯) β (πΊβπ₯))β2)) |
19 | 18 | mpteq2dv 5250 |
. . . . 5
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ (π = πΉ β§ π = πΊ)) β (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2)) = (π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2))) |
20 | 19 | oveq2d 7427 |
. . . 4
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ (π = πΉ β§ π = πΊ)) β (βfld
Ξ£g (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2))) = (βfld
Ξ£g (π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)))) |
21 | | simp2 1137 |
. . . . . . . . . . . 12
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β πΉ β π) |
22 | 6, 21 | rrxf 25142 |
. . . . . . . . . . 11
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β πΉ:πΌβΆβ) |
23 | 22 | ffvelcdmda 7086 |
. . . . . . . . . 10
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π₯ β πΌ) β (πΉβπ₯) β β) |
24 | | simp3 1138 |
. . . . . . . . . . . 12
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β πΊ β π) |
25 | 6, 24 | rrxf 25142 |
. . . . . . . . . . 11
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β πΊ:πΌβΆβ) |
26 | 25 | ffvelcdmda 7086 |
. . . . . . . . . 10
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π₯ β πΌ) β (πΊβπ₯) β β) |
27 | 23, 26 | resubcld 11646 |
. . . . . . . . 9
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π₯ β πΌ) β ((πΉβπ₯) β (πΊβπ₯)) β β) |
28 | 27 | resqcld 14094 |
. . . . . . . 8
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π₯ β πΌ) β (((πΉβπ₯) β (πΊβπ₯))β2) β β) |
29 | 28 | fmpttd 7116 |
. . . . . . 7
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β (π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)):πΌβΆβ) |
30 | 6, 21 | rrxfsupp 25143 |
. . . . . . . . . 10
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β (πΉ supp 0) β Fin) |
31 | 6, 24 | rrxfsupp 25143 |
. . . . . . . . . 10
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β (πΊ supp 0) β Fin) |
32 | | unfi 9174 |
. . . . . . . . . 10
β’ (((πΉ supp 0) β Fin β§ (πΊ supp 0) β Fin) β
((πΉ supp 0) βͺ (πΊ supp 0)) β
Fin) |
33 | 30, 31, 32 | syl2anc 584 |
. . . . . . . . 9
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β ((πΉ supp 0) βͺ (πΊ supp 0)) β Fin) |
34 | 6 | rrxmvallem 25145 |
. . . . . . . . 9
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) supp 0) β ((πΉ supp 0) βͺ (πΊ supp 0))) |
35 | 33, 34 | ssfid 9269 |
. . . . . . . 8
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) supp 0) β
Fin) |
36 | | mptexg 7225 |
. . . . . . . . . 10
β’ (πΌ β π β (π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) β V) |
37 | | funmpt 6586 |
. . . . . . . . . . 11
β’ Fun
(π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) |
38 | | 0cn 11210 |
. . . . . . . . . . 11
β’ 0 β
β |
39 | | funisfsupp 9369 |
. . . . . . . . . . 11
β’ ((Fun
(π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) β§ (π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) β V β§ 0 β β)
β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) finSupp 0 β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) supp 0) β
Fin)) |
40 | 37, 38, 39 | mp3an13 1452 |
. . . . . . . . . 10
β’ ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) β V β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) finSupp 0 β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) supp 0) β
Fin)) |
41 | 36, 40 | syl 17 |
. . . . . . . . 9
β’ (πΌ β π β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) finSupp 0 β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) supp 0) β
Fin)) |
42 | 41 | 3ad2ant1 1133 |
. . . . . . . 8
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) finSupp 0 β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) supp 0) β
Fin)) |
43 | 35, 42 | mpbird 256 |
. . . . . . 7
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β (π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) finSupp 0) |
44 | | simp1 1136 |
. . . . . . 7
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β πΌ β π) |
45 | | regsumsupp 21394 |
. . . . . . 7
β’ (((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)):πΌβΆβ β§ (π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) finSupp 0 β§ πΌ β π) β (βfld
Ξ£g (π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2))) = Ξ£π β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) supp 0)((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2))βπ)) |
46 | 29, 43, 44, 45 | syl3anc 1371 |
. . . . . 6
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β (βfld
Ξ£g (π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2))) = Ξ£π β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) supp 0)((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2))βπ)) |
47 | | suppssdm 8164 |
. . . . . . . . . . 11
β’ ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) supp 0) β dom (π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) |
48 | | eqid 2732 |
. . . . . . . . . . . 12
β’ (π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) = (π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) |
49 | 48 | dmmptss 6240 |
. . . . . . . . . . 11
β’ dom
(π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) β πΌ |
50 | 47, 49 | sstri 3991 |
. . . . . . . . . 10
β’ ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) supp 0) β πΌ |
51 | 50 | a1i 11 |
. . . . . . . . 9
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) supp 0) β πΌ) |
52 | 51 | sselda 3982 |
. . . . . . . 8
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) supp 0)) β π β πΌ) |
53 | | eqidd 2733 |
. . . . . . . . . 10
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π β πΌ) β (π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) = (π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2))) |
54 | | simpr 485 |
. . . . . . . . . . . . 13
β’ ((((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π β πΌ) β§ π₯ = π) β π₯ = π) |
55 | 54 | fveq2d 6895 |
. . . . . . . . . . . 12
β’ ((((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π β πΌ) β§ π₯ = π) β (πΉβπ₯) = (πΉβπ)) |
56 | 54 | fveq2d 6895 |
. . . . . . . . . . . 12
β’ ((((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π β πΌ) β§ π₯ = π) β (πΊβπ₯) = (πΊβπ)) |
57 | 55, 56 | oveq12d 7429 |
. . . . . . . . . . 11
β’ ((((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π β πΌ) β§ π₯ = π) β ((πΉβπ₯) β (πΊβπ₯)) = ((πΉβπ) β (πΊβπ))) |
58 | 57 | oveq1d 7426 |
. . . . . . . . . 10
β’ ((((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π β πΌ) β§ π₯ = π) β (((πΉβπ₯) β (πΊβπ₯))β2) = (((πΉβπ) β (πΊβπ))β2)) |
59 | | simpr 485 |
. . . . . . . . . 10
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π β πΌ) β π β πΌ) |
60 | | ovexd 7446 |
. . . . . . . . . 10
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π β πΌ) β (((πΉβπ) β (πΊβπ))β2) β V) |
61 | 53, 58, 59, 60 | fvmptd 7005 |
. . . . . . . . 9
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π β πΌ) β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2))βπ) = (((πΉβπ) β (πΊβπ))β2)) |
62 | 61 | eqcomd 2738 |
. . . . . . . 8
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π β πΌ) β (((πΉβπ) β (πΊβπ))β2) = ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2))βπ)) |
63 | 52, 62 | syldan 591 |
. . . . . . 7
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) supp 0)) β (((πΉβπ) β (πΊβπ))β2) = ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2))βπ)) |
64 | 63 | sumeq2dv 15653 |
. . . . . 6
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β Ξ£π β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) supp 0)(((πΉβπ) β (πΊβπ))β2) = Ξ£π β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) supp 0)((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2))βπ)) |
65 | 46, 64 | eqtr4d 2775 |
. . . . 5
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β (βfld
Ξ£g (π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2))) = Ξ£π β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) supp 0)(((πΉβπ) β (πΊβπ))β2)) |
66 | 65 | adantr 481 |
. . . 4
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ (π = πΉ β§ π = πΊ)) β (βfld
Ξ£g (π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2))) = Ξ£π β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) supp 0)(((πΉβπ) β (πΊβπ))β2)) |
67 | 22 | ffvelcdmda 7086 |
. . . . . . . . . 10
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π β πΌ) β (πΉβπ) β β) |
68 | 67 | recnd 11246 |
. . . . . . . . 9
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π β πΌ) β (πΉβπ) β β) |
69 | 25 | ffvelcdmda 7086 |
. . . . . . . . . 10
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π β πΌ) β (πΊβπ) β β) |
70 | 69 | recnd 11246 |
. . . . . . . . 9
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π β πΌ) β (πΊβπ) β β) |
71 | 68, 70 | subcld 11575 |
. . . . . . . 8
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π β πΌ) β ((πΉβπ) β (πΊβπ)) β β) |
72 | 71 | sqcld 14113 |
. . . . . . 7
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π β πΌ) β (((πΉβπ) β (πΊβπ))β2) β β) |
73 | 52, 72 | syldan 591 |
. . . . . 6
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) supp 0)) β (((πΉβπ) β (πΊβπ))β2) β β) |
74 | 6, 21 | rrxsuppss 25144 |
. . . . . . . . . . 11
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β (πΉ supp 0) β πΌ) |
75 | 6, 24 | rrxsuppss 25144 |
. . . . . . . . . . 11
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β (πΊ supp 0) β πΌ) |
76 | 74, 75 | unssd 4186 |
. . . . . . . . . 10
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β ((πΉ supp 0) βͺ (πΊ supp 0)) β πΌ) |
77 | 76 | ssdifssd 4142 |
. . . . . . . . 9
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β (((πΉ supp 0) βͺ (πΊ supp 0)) β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) supp 0)) β πΌ) |
78 | 77 | sselda 3982 |
. . . . . . . 8
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π β (((πΉ supp 0) βͺ (πΊ supp 0)) β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) supp 0))) β π β πΌ) |
79 | 78, 62 | syldan 591 |
. . . . . . 7
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π β (((πΉ supp 0) βͺ (πΊ supp 0)) β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) supp 0))) β (((πΉβπ) β (πΊβπ))β2) = ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2))βπ)) |
80 | 76 | ssdifd 4140 |
. . . . . . . . 9
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β (((πΉ supp 0) βͺ (πΊ supp 0)) β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) supp 0)) β (πΌ β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) supp 0))) |
81 | 80 | sselda 3982 |
. . . . . . . 8
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π β (((πΉ supp 0) βͺ (πΊ supp 0)) β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) supp 0))) β π β (πΌ β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) supp 0))) |
82 | | ssidd 4005 |
. . . . . . . . 9
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) supp 0) β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) supp 0)) |
83 | | 0cnd 11211 |
. . . . . . . . 9
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β 0 β β) |
84 | 29, 82, 44, 83 | suppssr 8183 |
. . . . . . . 8
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π β (πΌ β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) supp 0))) β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2))βπ) = 0) |
85 | 81, 84 | syldan 591 |
. . . . . . 7
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π β (((πΉ supp 0) βͺ (πΊ supp 0)) β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) supp 0))) β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2))βπ) = 0) |
86 | 79, 85 | eqtrd 2772 |
. . . . . 6
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π β (((πΉ supp 0) βͺ (πΊ supp 0)) β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) supp 0))) β (((πΉβπ) β (πΊβπ))β2) = 0) |
87 | 34, 73, 86, 33 | fsumss 15675 |
. . . . 5
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β Ξ£π β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) supp 0)(((πΉβπ) β (πΊβπ))β2) = Ξ£π β ((πΉ supp 0) βͺ (πΊ supp 0))(((πΉβπ) β (πΊβπ))β2)) |
88 | 87 | adantr 481 |
. . . 4
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ (π = πΉ β§ π = πΊ)) β Ξ£π β ((π₯ β πΌ β¦ (((πΉβπ₯) β (πΊβπ₯))β2)) supp 0)(((πΉβπ) β (πΊβπ))β2) = Ξ£π β ((πΉ supp 0) βͺ (πΊ supp 0))(((πΉβπ) β (πΊβπ))β2)) |
89 | 20, 66, 88 | 3eqtrd 2776 |
. . 3
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ (π = πΉ β§ π = πΊ)) β (βfld
Ξ£g (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2))) = Ξ£π β ((πΉ supp 0) βͺ (πΊ supp 0))(((πΉβπ) β (πΊβπ))β2)) |
90 | 89 | fveq2d 6895 |
. 2
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ (π = πΉ β§ π = πΊ)) β
(ββ(βfld Ξ£g (π₯ β πΌ β¦ (((πβπ₯) β (πβπ₯))β2)))) = (ββΞ£π β ((πΉ supp 0) βͺ (πΊ supp 0))(((πΉβπ) β (πΊβπ))β2))) |
91 | | fvexd 6906 |
. 2
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β (ββΞ£π β ((πΉ supp 0) βͺ (πΊ supp 0))(((πΉβπ) β (πΊβπ))β2)) β V) |
92 | 12, 90, 21, 24, 91 | ovmpod 7562 |
1
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β (πΉπ·πΊ) = (ββΞ£π β ((πΉ supp 0) βͺ (πΊ supp 0))(((πΉβπ) β (πΊβπ))β2))) |