Step | Hyp | Ref
| Expression |
1 | | simprl 770 |
. . . . . . . . . 10
β’ ((((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π₯ β πΌ) β§ ((πΉβπ₯) = 0 β§ (πΊβπ₯) = 0)) β (πΉβπ₯) = 0) |
2 | | 0cn 11148 |
. . . . . . . . . 10
β’ 0 β
β |
3 | 1, 2 | eqeltrdi 2846 |
. . . . . . . . 9
β’ ((((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π₯ β πΌ) β§ ((πΉβπ₯) = 0 β§ (πΊβπ₯) = 0)) β (πΉβπ₯) β β) |
4 | | simprr 772 |
. . . . . . . . . 10
β’ ((((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π₯ β πΌ) β§ ((πΉβπ₯) = 0 β§ (πΊβπ₯) = 0)) β (πΊβπ₯) = 0) |
5 | 1, 4 | eqtr4d 2780 |
. . . . . . . . 9
β’ ((((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π₯ β πΌ) β§ ((πΉβπ₯) = 0 β§ (πΊβπ₯) = 0)) β (πΉβπ₯) = (πΊβπ₯)) |
6 | 3, 5 | subeq0bd 11582 |
. . . . . . . 8
β’ ((((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π₯ β πΌ) β§ ((πΉβπ₯) = 0 β§ (πΊβπ₯) = 0)) β ((πΉβπ₯) β (πΊβπ₯)) = 0) |
7 | 6 | sq0id 14099 |
. . . . . . 7
β’ ((((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π₯ β πΌ) β§ ((πΉβπ₯) = 0 β§ (πΊβπ₯) = 0)) β (((πΉβπ₯) β (πΊβπ₯))β2) = 0) |
8 | 7 | ex 414 |
. . . . . 6
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π₯ β πΌ) β (((πΉβπ₯) = 0 β§ (πΊβπ₯) = 0) β (((πΉβπ₯) β (πΊβπ₯))β2) = 0)) |
9 | | ioran 983 |
. . . . . . . 8
β’ (Β¬
((πΉβπ₯) β 0 β¨ (πΊβπ₯) β 0) β (Β¬ (πΉβπ₯) β 0 β§ Β¬ (πΊβπ₯) β 0)) |
10 | | nne 2948 |
. . . . . . . . 9
β’ (Β¬
(πΉβπ₯) β 0 β (πΉβπ₯) = 0) |
11 | | nne 2948 |
. . . . . . . . 9
β’ (Β¬
(πΊβπ₯) β 0 β (πΊβπ₯) = 0) |
12 | 10, 11 | anbi12i 628 |
. . . . . . . 8
β’ ((Β¬
(πΉβπ₯) β 0 β§ Β¬ (πΊβπ₯) β 0) β ((πΉβπ₯) = 0 β§ (πΊβπ₯) = 0)) |
13 | 9, 12 | bitri 275 |
. . . . . . 7
β’ (Β¬
((πΉβπ₯) β 0 β¨ (πΊβπ₯) β 0) β ((πΉβπ₯) = 0 β§ (πΊβπ₯) = 0)) |
14 | 13 | a1i 11 |
. . . . . 6
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π₯ β πΌ) β (Β¬ ((πΉβπ₯) β 0 β¨ (πΊβπ₯) β 0) β ((πΉβπ₯) = 0 β§ (πΊβπ₯) = 0))) |
15 | | eqidd 2738 |
. . . . . . . . . 10
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π₯ β πΌ) β (π β πΌ β¦ (((πΉβπ) β (πΊβπ))β2)) = (π β πΌ β¦ (((πΉβπ) β (πΊβπ))β2))) |
16 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π₯ β πΌ) β§ π = π₯) β π = π₯) |
17 | 16 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ ((((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π₯ β πΌ) β§ π = π₯) β (πΉβπ) = (πΉβπ₯)) |
18 | 16 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ ((((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π₯ β πΌ) β§ π = π₯) β (πΊβπ) = (πΊβπ₯)) |
19 | 17, 18 | oveq12d 7376 |
. . . . . . . . . . 11
β’ ((((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π₯ β πΌ) β§ π = π₯) β ((πΉβπ) β (πΊβπ)) = ((πΉβπ₯) β (πΊβπ₯))) |
20 | 19 | oveq1d 7373 |
. . . . . . . . . 10
β’ ((((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π₯ β πΌ) β§ π = π₯) β (((πΉβπ) β (πΊβπ))β2) = (((πΉβπ₯) β (πΊβπ₯))β2)) |
21 | | simpr 486 |
. . . . . . . . . 10
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π₯ β πΌ) β π₯ β πΌ) |
22 | | ovex 7391 |
. . . . . . . . . . 11
β’ (((πΉβπ₯) β (πΊβπ₯))β2) β V |
23 | 22 | a1i 11 |
. . . . . . . . . 10
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π₯ β πΌ) β (((πΉβπ₯) β (πΊβπ₯))β2) β V) |
24 | 15, 20, 21, 23 | fvmptd 6956 |
. . . . . . . . 9
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π₯ β πΌ) β ((π β πΌ β¦ (((πΉβπ) β (πΊβπ))β2))βπ₯) = (((πΉβπ₯) β (πΊβπ₯))β2)) |
25 | 24 | neeq1d 3004 |
. . . . . . . 8
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π₯ β πΌ) β (((π β πΌ β¦ (((πΉβπ) β (πΊβπ))β2))βπ₯) β 0 β (((πΉβπ₯) β (πΊβπ₯))β2) β 0)) |
26 | 25 | bicomd 222 |
. . . . . . 7
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π₯ β πΌ) β ((((πΉβπ₯) β (πΊβπ₯))β2) β 0 β ((π β πΌ β¦ (((πΉβπ) β (πΊβπ))β2))βπ₯) β 0)) |
27 | 26 | necon1bbid 2984 |
. . . . . 6
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π₯ β πΌ) β (Β¬ ((π β πΌ β¦ (((πΉβπ) β (πΊβπ))β2))βπ₯) β 0 β (((πΉβπ₯) β (πΊβπ₯))β2) = 0)) |
28 | 8, 14, 27 | 3imtr4d 294 |
. . . . 5
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π₯ β πΌ) β (Β¬ ((πΉβπ₯) β 0 β¨ (πΊβπ₯) β 0) β Β¬ ((π β πΌ β¦ (((πΉβπ) β (πΊβπ))β2))βπ₯) β 0)) |
29 | 28 | con4d 115 |
. . . 4
β’ (((πΌ β π β§ πΉ β π β§ πΊ β π) β§ π₯ β πΌ) β (((π β πΌ β¦ (((πΉβπ) β (πΊβπ))β2))βπ₯) β 0 β ((πΉβπ₯) β 0 β¨ (πΊβπ₯) β 0))) |
30 | 29 | ss2rabdv 4034 |
. . 3
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β {π₯ β πΌ β£ ((π β πΌ β¦ (((πΉβπ) β (πΊβπ))β2))βπ₯) β 0} β {π₯ β πΌ β£ ((πΉβπ₯) β 0 β¨ (πΊβπ₯) β 0)}) |
31 | | unrab 4266 |
. . 3
β’ ({π₯ β πΌ β£ (πΉβπ₯) β 0} βͺ {π₯ β πΌ β£ (πΊβπ₯) β 0}) = {π₯ β πΌ β£ ((πΉβπ₯) β 0 β¨ (πΊβπ₯) β 0)} |
32 | 30, 31 | sseqtrrdi 3996 |
. 2
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β {π₯ β πΌ β£ ((π β πΌ β¦ (((πΉβπ) β (πΊβπ))β2))βπ₯) β 0} β ({π₯ β πΌ β£ (πΉβπ₯) β 0} βͺ {π₯ β πΌ β£ (πΊβπ₯) β 0})) |
33 | | simp1 1137 |
. . 3
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β πΌ β π) |
34 | | ovex 7391 |
. . . . 5
β’ (((πΉβπ) β (πΊβπ))β2) β V |
35 | | eqid 2737 |
. . . . 5
β’ (π β πΌ β¦ (((πΉβπ) β (πΊβπ))β2)) = (π β πΌ β¦ (((πΉβπ) β (πΊβπ))β2)) |
36 | 34, 35 | fnmpti 6645 |
. . . 4
β’ (π β πΌ β¦ (((πΉβπ) β (πΊβπ))β2)) Fn πΌ |
37 | | suppvalfn 8101 |
. . . 4
β’ (((π β πΌ β¦ (((πΉβπ) β (πΊβπ))β2)) Fn πΌ β§ πΌ β π β§ 0 β β) β ((π β πΌ β¦ (((πΉβπ) β (πΊβπ))β2)) supp 0) = {π₯ β πΌ β£ ((π β πΌ β¦ (((πΉβπ) β (πΊβπ))β2))βπ₯) β 0}) |
38 | 36, 2, 37 | mp3an13 1453 |
. . 3
β’ (πΌ β π β ((π β πΌ β¦ (((πΉβπ) β (πΊβπ))β2)) supp 0) = {π₯ β πΌ β£ ((π β πΌ β¦ (((πΉβπ) β (πΊβπ))β2))βπ₯) β 0}) |
39 | 33, 38 | syl 17 |
. 2
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β ((π β πΌ β¦ (((πΉβπ) β (πΊβπ))β2)) supp 0) = {π₯ β πΌ β£ ((π β πΌ β¦ (((πΉβπ) β (πΊβπ))β2))βπ₯) β 0}) |
40 | | elrabi 3640 |
. . . . . . 7
β’ (πΉ β {β β (β βm πΌ) β£ β finSupp 0} β πΉ β (β βm πΌ)) |
41 | | rrxmval.1 |
. . . . . . 7
β’ π = {β β (β βm πΌ) β£ β finSupp 0} |
42 | 40, 41 | eleq2s 2856 |
. . . . . 6
β’ (πΉ β π β πΉ β (β βm πΌ)) |
43 | | elmapi 8788 |
. . . . . 6
β’ (πΉ β (β
βm πΌ)
β πΉ:πΌβΆβ) |
44 | | ffn 6669 |
. . . . . 6
β’ (πΉ:πΌβΆβ β πΉ Fn πΌ) |
45 | 42, 43, 44 | 3syl 18 |
. . . . 5
β’ (πΉ β π β πΉ Fn πΌ) |
46 | 45 | 3ad2ant2 1135 |
. . . 4
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β πΉ Fn πΌ) |
47 | 2 | a1i 11 |
. . . 4
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β 0 β β) |
48 | | suppvalfn 8101 |
. . . 4
β’ ((πΉ Fn πΌ β§ πΌ β π β§ 0 β β) β (πΉ supp 0) = {π₯ β πΌ β£ (πΉβπ₯) β 0}) |
49 | 46, 33, 47, 48 | syl3anc 1372 |
. . 3
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β (πΉ supp 0) = {π₯ β πΌ β£ (πΉβπ₯) β 0}) |
50 | | elrabi 3640 |
. . . . . . 7
β’ (πΊ β {β β (β βm πΌ) β£ β finSupp 0} β πΊ β (β βm πΌ)) |
51 | 50, 41 | eleq2s 2856 |
. . . . . 6
β’ (πΊ β π β πΊ β (β βm πΌ)) |
52 | | elmapi 8788 |
. . . . . 6
β’ (πΊ β (β
βm πΌ)
β πΊ:πΌβΆβ) |
53 | | ffn 6669 |
. . . . . 6
β’ (πΊ:πΌβΆβ β πΊ Fn πΌ) |
54 | 51, 52, 53 | 3syl 18 |
. . . . 5
β’ (πΊ β π β πΊ Fn πΌ) |
55 | 54 | 3ad2ant3 1136 |
. . . 4
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β πΊ Fn πΌ) |
56 | | suppvalfn 8101 |
. . . 4
β’ ((πΊ Fn πΌ β§ πΌ β π β§ 0 β β) β (πΊ supp 0) = {π₯ β πΌ β£ (πΊβπ₯) β 0}) |
57 | 55, 33, 47, 56 | syl3anc 1372 |
. . 3
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β (πΊ supp 0) = {π₯ β πΌ β£ (πΊβπ₯) β 0}) |
58 | 49, 57 | uneq12d 4125 |
. 2
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β ((πΉ supp 0) βͺ (πΊ supp 0)) = ({π₯ β πΌ β£ (πΉβπ₯) β 0} βͺ {π₯ β πΌ β£ (πΊβπ₯) β 0})) |
59 | 32, 39, 58 | 3sstr4d 3992 |
1
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β ((π β πΌ β¦ (((πΉβπ) β (πΊβπ))β2)) supp 0) β ((πΉ supp 0) βͺ (πΊ supp 0))) |