Step | Hyp | Ref
| Expression |
1 | | rrxmetlem.6 |
. 2
β’ (π β ((πΉ supp 0) βͺ (πΊ supp 0)) β π΄) |
2 | | rrxmetlem.4 |
. . . . . . 7
β’ (π β π΄ β πΌ) |
3 | 1, 2 | sstrd 3955 |
. . . . . 6
β’ (π β ((πΉ supp 0) βͺ (πΊ supp 0)) β πΌ) |
4 | 3 | sselda 3945 |
. . . . 5
β’ ((π β§ π β ((πΉ supp 0) βͺ (πΊ supp 0))) β π β πΌ) |
5 | | rrxmval.1 |
. . . . . . . 8
β’ π = {β β (β βm πΌ) β£ β finSupp 0} |
6 | | rrxmetlem.2 |
. . . . . . . 8
β’ (π β πΉ β π) |
7 | 5, 6 | rrxf 24768 |
. . . . . . 7
β’ (π β πΉ:πΌβΆβ) |
8 | 7 | ffvelcdmda 7036 |
. . . . . 6
β’ ((π β§ π β πΌ) β (πΉβπ) β β) |
9 | 8 | recnd 11184 |
. . . . 5
β’ ((π β§ π β πΌ) β (πΉβπ) β β) |
10 | 4, 9 | syldan 592 |
. . . 4
β’ ((π β§ π β ((πΉ supp 0) βͺ (πΊ supp 0))) β (πΉβπ) β β) |
11 | | rrxmetlem.3 |
. . . . . . . 8
β’ (π β πΊ β π) |
12 | 5, 11 | rrxf 24768 |
. . . . . . 7
β’ (π β πΊ:πΌβΆβ) |
13 | 12 | ffvelcdmda 7036 |
. . . . . 6
β’ ((π β§ π β πΌ) β (πΊβπ) β β) |
14 | 13 | recnd 11184 |
. . . . 5
β’ ((π β§ π β πΌ) β (πΊβπ) β β) |
15 | 4, 14 | syldan 592 |
. . . 4
β’ ((π β§ π β ((πΉ supp 0) βͺ (πΊ supp 0))) β (πΊβπ) β β) |
16 | 10, 15 | subcld 11513 |
. . 3
β’ ((π β§ π β ((πΉ supp 0) βͺ (πΊ supp 0))) β ((πΉβπ) β (πΊβπ)) β β) |
17 | 16 | sqcld 14050 |
. 2
β’ ((π β§ π β ((πΉ supp 0) βͺ (πΊ supp 0))) β (((πΉβπ) β (πΊβπ))β2) β β) |
18 | 2 | ssdifd 4101 |
. . . 4
β’ (π β (π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0)))) |
19 | 18 | sselda 3945 |
. . 3
β’ ((π β§ π β (π΄ β ((πΉ supp 0) βͺ (πΊ supp 0)))) β π β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0)))) |
20 | | simpr 486 |
. . . . . . 7
β’ ((π β§ π β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0)))) β π β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0)))) |
21 | 20 | eldifad 3923 |
. . . . . 6
β’ ((π β§ π β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0)))) β π β πΌ) |
22 | 21, 9 | syldan 592 |
. . . . 5
β’ ((π β§ π β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0)))) β (πΉβπ) β β) |
23 | | ssun1 4133 |
. . . . . . . 8
β’ (πΉ supp 0) β ((πΉ supp 0) βͺ (πΊ supp 0)) |
24 | 23 | a1i 11 |
. . . . . . 7
β’ (π β (πΉ supp 0) β ((πΉ supp 0) βͺ (πΊ supp 0))) |
25 | | rrxmetlem.1 |
. . . . . . 7
β’ (π β πΌ β π) |
26 | | 0red 11159 |
. . . . . . 7
β’ (π β 0 β
β) |
27 | 7, 24, 25, 26 | suppssr 8128 |
. . . . . 6
β’ ((π β§ π β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0)))) β (πΉβπ) = 0) |
28 | | ssun2 4134 |
. . . . . . . 8
β’ (πΊ supp 0) β ((πΉ supp 0) βͺ (πΊ supp 0)) |
29 | 28 | a1i 11 |
. . . . . . 7
β’ (π β (πΊ supp 0) β ((πΉ supp 0) βͺ (πΊ supp 0))) |
30 | 12, 29, 25, 26 | suppssr 8128 |
. . . . . 6
β’ ((π β§ π β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0)))) β (πΊβπ) = 0) |
31 | 27, 30 | eqtr4d 2780 |
. . . . 5
β’ ((π β§ π β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0)))) β (πΉβπ) = (πΊβπ)) |
32 | 22, 31 | subeq0bd 11582 |
. . . 4
β’ ((π β§ π β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0)))) β ((πΉβπ) β (πΊβπ)) = 0) |
33 | 32 | sq0id 14099 |
. . 3
β’ ((π β§ π β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0)))) β (((πΉβπ) β (πΊβπ))β2) = 0) |
34 | 19, 33 | syldan 592 |
. 2
β’ ((π β§ π β (π΄ β ((πΉ supp 0) βͺ (πΊ supp 0)))) β (((πΉβπ) β (πΊβπ))β2) = 0) |
35 | | rrxmetlem.5 |
. 2
β’ (π β π΄ β Fin) |
36 | 1, 17, 34, 35 | fsumss 15611 |
1
β’ (π β Ξ£π β ((πΉ supp 0) βͺ (πΊ supp 0))(((πΉβπ) β (πΊβπ))β2) = Ξ£π β π΄ (((πΉβπ) β (πΊβπ))β2)) |