Step | Hyp | Ref
| Expression |
1 | | simplll 774 |
. . 3
β’ ((((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β πΌ β π) |
2 | | simpr 486 |
. . 3
β’ ((((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) |
3 | | simplr 768 |
. . 3
β’ ((((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β (πΉ β π β§ πΊ β π)) |
4 | | rrxmval.1 |
. . . . . . . . 9
β’ π = {β β (β βm πΌ) β£ β finSupp 0} |
5 | | simprl 770 |
. . . . . . . . 9
β’ (((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β πΉ β π) |
6 | 4, 5 | rrxfsupp 24769 |
. . . . . . . 8
β’ (((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β (πΉ supp 0) β Fin) |
7 | | simprr 772 |
. . . . . . . . 9
β’ (((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β πΊ β π) |
8 | 4, 7 | rrxfsupp 24769 |
. . . . . . . 8
β’ (((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β (πΊ supp 0) β Fin) |
9 | | unfi 9117 |
. . . . . . . 8
β’ (((πΉ supp 0) β Fin β§ (πΊ supp 0) β Fin) β
((πΉ supp 0) βͺ (πΊ supp 0)) β
Fin) |
10 | 6, 8, 9 | syl2anc 585 |
. . . . . . 7
β’ (((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β ((πΉ supp 0) βͺ (πΊ supp 0)) β Fin) |
11 | 4, 5 | rrxsuppss 24770 |
. . . . . . . . . 10
β’ (((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β (πΉ supp 0) β πΌ) |
12 | 4, 7 | rrxsuppss 24770 |
. . . . . . . . . 10
β’ (((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β (πΊ supp 0) β πΌ) |
13 | 11, 12 | unssd 4147 |
. . . . . . . . 9
β’ (((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β ((πΉ supp 0) βͺ (πΊ supp 0)) β πΌ) |
14 | 13 | sselda 3945 |
. . . . . . . 8
β’ ((((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β§ π β ((πΉ supp 0) βͺ (πΊ supp 0))) β π β πΌ) |
15 | 4, 5 | rrxf 24768 |
. . . . . . . . . . 11
β’ (((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β πΉ:πΌβΆβ) |
16 | 15 | ffvelcdmda 7036 |
. . . . . . . . . 10
β’ ((((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β§ π β πΌ) β (πΉβπ) β β) |
17 | 4, 7 | rrxf 24768 |
. . . . . . . . . . 11
β’ (((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β πΊ:πΌβΆβ) |
18 | 17 | ffvelcdmda 7036 |
. . . . . . . . . 10
β’ ((((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β§ π β πΌ) β (πΊβπ) β β) |
19 | 16, 18 | resubcld 11584 |
. . . . . . . . 9
β’ ((((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β§ π β πΌ) β ((πΉβπ) β (πΊβπ)) β β) |
20 | 19 | resqcld 14031 |
. . . . . . . 8
β’ ((((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β§ π β πΌ) β (((πΉβπ) β (πΊβπ))β2) β β) |
21 | 14, 20 | syldan 592 |
. . . . . . 7
β’ ((((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β§ π β ((πΉ supp 0) βͺ (πΊ supp 0))) β (((πΉβπ) β (πΊβπ))β2) β β) |
22 | 19 | sqge0d 14043 |
. . . . . . . 8
β’ ((((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β§ π β πΌ) β 0 β€ (((πΉβπ) β (πΊβπ))β2)) |
23 | 14, 22 | syldan 592 |
. . . . . . 7
β’ ((((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β§ π β ((πΉ supp 0) βͺ (πΊ supp 0))) β 0 β€ (((πΉβπ) β (πΊβπ))β2)) |
24 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = π΄ β (πΉβπ) = (πΉβπ΄)) |
25 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = π΄ β (πΊβπ) = (πΊβπ΄)) |
26 | 24, 25 | oveq12d 7376 |
. . . . . . . 8
β’ (π = π΄ β ((πΉβπ) β (πΊβπ)) = ((πΉβπ΄) β (πΊβπ΄))) |
27 | 26 | oveq1d 7373 |
. . . . . . 7
β’ (π = π΄ β (((πΉβπ) β (πΊβπ))β2) = (((πΉβπ΄) β (πΊβπ΄))β2)) |
28 | | simplr 768 |
. . . . . . 7
β’ (((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) |
29 | 10, 21, 23, 27, 28 | fsumge1 15683 |
. . . . . 6
β’ (((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β (((πΉβπ΄) β (πΊβπ΄))β2) β€ Ξ£π β ((πΉ supp 0) βͺ (πΊ supp 0))(((πΉβπ) β (πΊβπ))β2)) |
30 | 13, 28 | sseldd 3946 |
. . . . . . . . 9
β’ (((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β π΄ β πΌ) |
31 | 15, 30 | ffvelcdmd 7037 |
. . . . . . . 8
β’ (((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β (πΉβπ΄) β β) |
32 | 17, 30 | ffvelcdmd 7037 |
. . . . . . . 8
β’ (((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β (πΊβπ΄) β β) |
33 | 31, 32 | resubcld 11584 |
. . . . . . 7
β’ (((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β ((πΉβπ΄) β (πΊβπ΄)) β β) |
34 | | absresq 15188 |
. . . . . . 7
β’ (((πΉβπ΄) β (πΊβπ΄)) β β β ((absβ((πΉβπ΄) β (πΊβπ΄)))β2) = (((πΉβπ΄) β (πΊβπ΄))β2)) |
35 | 33, 34 | syl 17 |
. . . . . 6
β’ (((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β ((absβ((πΉβπ΄) β (πΊβπ΄)))β2) = (((πΉβπ΄) β (πΊβπ΄))β2)) |
36 | 10, 21 | fsumrecl 15620 |
. . . . . . 7
β’ (((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β Ξ£π β ((πΉ supp 0) βͺ (πΊ supp 0))(((πΉβπ) β (πΊβπ))β2) β β) |
37 | 10, 21, 23 | fsumge0 15681 |
. . . . . . 7
β’ (((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β 0 β€ Ξ£π β ((πΉ supp 0) βͺ (πΊ supp 0))(((πΉβπ) β (πΊβπ))β2)) |
38 | | resqrtth 15141 |
. . . . . . 7
β’
((Ξ£π β
((πΉ supp 0) βͺ (πΊ supp 0))(((πΉβπ) β (πΊβπ))β2) β β β§ 0 β€
Ξ£π β ((πΉ supp 0) βͺ (πΊ supp 0))(((πΉβπ) β (πΊβπ))β2)) β
((ββΞ£π
β ((πΉ supp 0) βͺ
(πΊ supp 0))(((πΉβπ) β (πΊβπ))β2))β2) = Ξ£π β ((πΉ supp 0) βͺ (πΊ supp 0))(((πΉβπ) β (πΊβπ))β2)) |
39 | 36, 37, 38 | syl2anc 585 |
. . . . . 6
β’ (((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β ((ββΞ£π β ((πΉ supp 0) βͺ (πΊ supp 0))(((πΉβπ) β (πΊβπ))β2))β2) = Ξ£π β ((πΉ supp 0) βͺ (πΊ supp 0))(((πΉβπ) β (πΊβπ))β2)) |
40 | 29, 35, 39 | 3brtr4d 5138 |
. . . . 5
β’ (((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β ((absβ((πΉβπ΄) β (πΊβπ΄)))β2) β€
((ββΞ£π
β ((πΉ supp 0) βͺ
(πΊ supp 0))(((πΉβπ) β (πΊβπ))β2))β2)) |
41 | 33 | recnd 11184 |
. . . . . . 7
β’ (((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β ((πΉβπ΄) β (πΊβπ΄)) β β) |
42 | 41 | abscld 15322 |
. . . . . 6
β’ (((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β (absβ((πΉβπ΄) β (πΊβπ΄))) β β) |
43 | 36, 37 | resqrtcld 15303 |
. . . . . 6
β’ (((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β (ββΞ£π β ((πΉ supp 0) βͺ (πΊ supp 0))(((πΉβπ) β (πΊβπ))β2)) β β) |
44 | 41 | absge0d 15330 |
. . . . . 6
β’ (((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β 0 β€ (absβ((πΉβπ΄) β (πΊβπ΄)))) |
45 | 36, 37 | sqrtge0d 15306 |
. . . . . 6
β’ (((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β 0 β€ (ββΞ£π β ((πΉ supp 0) βͺ (πΊ supp 0))(((πΉβπ) β (πΊβπ))β2))) |
46 | 42, 43, 44, 45 | le2sqd 14161 |
. . . . 5
β’ (((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β ((absβ((πΉβπ΄) β (πΊβπ΄))) β€ (ββΞ£π β ((πΉ supp 0) βͺ (πΊ supp 0))(((πΉβπ) β (πΊβπ))β2)) β ((absβ((πΉβπ΄) β (πΊβπ΄)))β2) β€
((ββΞ£π
β ((πΉ supp 0) βͺ
(πΊ supp 0))(((πΉβπ) β (πΊβπ))β2))β2))) |
47 | 40, 46 | mpbird 257 |
. . . 4
β’ (((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β (absβ((πΉβπ΄) β (πΊβπ΄))) β€ (ββΞ£π β ((πΉ supp 0) βͺ (πΊ supp 0))(((πΉβπ) β (πΊβπ))β2))) |
48 | | rrxdstprj1.1 |
. . . . . 6
β’ π = ((abs β β )
βΎ (β Γ β)) |
49 | 48 | remetdval 24155 |
. . . . 5
β’ (((πΉβπ΄) β β β§ (πΊβπ΄) β β) β ((πΉβπ΄)π(πΊβπ΄)) = (absβ((πΉβπ΄) β (πΊβπ΄)))) |
50 | 31, 32, 49 | syl2anc 585 |
. . . 4
β’ (((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β ((πΉβπ΄)π(πΊβπ΄)) = (absβ((πΉβπ΄) β (πΊβπ΄)))) |
51 | | rrxmval.d |
. . . . . . 7
β’ π· =
(distβ(β^βπΌ)) |
52 | 4, 51 | rrxmval 24772 |
. . . . . 6
β’ ((πΌ β π β§ πΉ β π β§ πΊ β π) β (πΉπ·πΊ) = (ββΞ£π β ((πΉ supp 0) βͺ (πΊ supp 0))(((πΉβπ) β (πΊβπ))β2))) |
53 | 52 | 3expb 1121 |
. . . . 5
β’ ((πΌ β π β§ (πΉ β π β§ πΊ β π)) β (πΉπ·πΊ) = (ββΞ£π β ((πΉ supp 0) βͺ (πΊ supp 0))(((πΉβπ) β (πΊβπ))β2))) |
54 | 53 | adantlr 714 |
. . . 4
β’ (((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β (πΉπ·πΊ) = (ββΞ£π β ((πΉ supp 0) βͺ (πΊ supp 0))(((πΉβπ) β (πΊβπ))β2))) |
55 | 47, 50, 54 | 3brtr4d 5138 |
. . 3
β’ (((πΌ β π β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β§ (πΉ β π β§ πΊ β π)) β ((πΉβπ΄)π(πΊβπ΄)) β€ (πΉπ·πΊ)) |
56 | 1, 2, 3, 55 | syl21anc 837 |
. 2
β’ ((((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β§ π΄ β ((πΉ supp 0) βͺ (πΊ supp 0))) β ((πΉβπ΄)π(πΊβπ΄)) β€ (πΉπ·πΊ)) |
57 | | simplll 774 |
. . . . . . 7
β’ ((((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β§ π΄ β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0)))) β πΌ β π) |
58 | | simplrl 776 |
. . . . . . 7
β’ ((((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β§ π΄ β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0)))) β πΉ β π) |
59 | | ssun1 4133 |
. . . . . . . . . 10
β’ (πΉ supp 0) β ((πΉ supp 0) βͺ (πΊ supp 0)) |
60 | 59 | a1i 11 |
. . . . . . . . 9
β’ (((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β (πΉ supp 0) β ((πΉ supp 0) βͺ (πΊ supp 0))) |
61 | 60 | sscond 4102 |
. . . . . . . 8
β’ (((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0))) β (πΌ β (πΉ supp 0))) |
62 | 61 | sselda 3945 |
. . . . . . 7
β’ ((((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β§ π΄ β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0)))) β π΄ β (πΌ β (πΉ supp 0))) |
63 | | simpr 486 |
. . . . . . . . 9
β’ ((πΌ β π β§ πΉ β π) β πΉ β π) |
64 | 4, 63 | rrxf 24768 |
. . . . . . . 8
β’ ((πΌ β π β§ πΉ β π) β πΉ:πΌβΆβ) |
65 | | ssidd 3968 |
. . . . . . . 8
β’ ((πΌ β π β§ πΉ β π) β (πΉ supp 0) β (πΉ supp 0)) |
66 | | simpl 484 |
. . . . . . . 8
β’ ((πΌ β π β§ πΉ β π) β πΌ β π) |
67 | | 0red 11159 |
. . . . . . . 8
β’ ((πΌ β π β§ πΉ β π) β 0 β β) |
68 | 64, 65, 66, 67 | suppssr 8128 |
. . . . . . 7
β’ (((πΌ β π β§ πΉ β π) β§ π΄ β (πΌ β (πΉ supp 0))) β (πΉβπ΄) = 0) |
69 | 57, 58, 62, 68 | syl21anc 837 |
. . . . . 6
β’ ((((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β§ π΄ β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0)))) β (πΉβπ΄) = 0) |
70 | | 0red 11159 |
. . . . . 6
β’ ((((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β§ π΄ β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0)))) β 0 β
β) |
71 | 69, 70 | eqeltrd 2838 |
. . . . 5
β’ ((((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β§ π΄ β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0)))) β (πΉβπ΄) β β) |
72 | | simplrr 777 |
. . . . . . 7
β’ ((((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β§ π΄ β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0)))) β πΊ β π) |
73 | | ssun2 4134 |
. . . . . . . . . 10
β’ (πΊ supp 0) β ((πΉ supp 0) βͺ (πΊ supp 0)) |
74 | 73 | a1i 11 |
. . . . . . . . 9
β’ (((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β (πΊ supp 0) β ((πΉ supp 0) βͺ (πΊ supp 0))) |
75 | 74 | sscond 4102 |
. . . . . . . 8
β’ (((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0))) β (πΌ β (πΊ supp 0))) |
76 | 75 | sselda 3945 |
. . . . . . 7
β’ ((((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β§ π΄ β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0)))) β π΄ β (πΌ β (πΊ supp 0))) |
77 | | simpr 486 |
. . . . . . . . 9
β’ ((πΌ β π β§ πΊ β π) β πΊ β π) |
78 | 4, 77 | rrxf 24768 |
. . . . . . . 8
β’ ((πΌ β π β§ πΊ β π) β πΊ:πΌβΆβ) |
79 | | ssidd 3968 |
. . . . . . . 8
β’ ((πΌ β π β§ πΊ β π) β (πΊ supp 0) β (πΊ supp 0)) |
80 | | simpl 484 |
. . . . . . . 8
β’ ((πΌ β π β§ πΊ β π) β πΌ β π) |
81 | | 0red 11159 |
. . . . . . . 8
β’ ((πΌ β π β§ πΊ β π) β 0 β β) |
82 | 78, 79, 80, 81 | suppssr 8128 |
. . . . . . 7
β’ (((πΌ β π β§ πΊ β π) β§ π΄ β (πΌ β (πΊ supp 0))) β (πΊβπ΄) = 0) |
83 | 57, 72, 76, 82 | syl21anc 837 |
. . . . . 6
β’ ((((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β§ π΄ β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0)))) β (πΊβπ΄) = 0) |
84 | 83, 70 | eqeltrd 2838 |
. . . . 5
β’ ((((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β§ π΄ β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0)))) β (πΊβπ΄) β β) |
85 | 71, 84, 49 | syl2anc 585 |
. . . 4
β’ ((((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β§ π΄ β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0)))) β ((πΉβπ΄)π(πΊβπ΄)) = (absβ((πΉβπ΄) β (πΊβπ΄)))) |
86 | 69, 83 | oveq12d 7376 |
. . . . . 6
β’ ((((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β§ π΄ β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0)))) β ((πΉβπ΄) β (πΊβπ΄)) = (0 β 0)) |
87 | | 0m0e0 12274 |
. . . . . 6
β’ (0
β 0) = 0 |
88 | 86, 87 | eqtrdi 2793 |
. . . . 5
β’ ((((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β§ π΄ β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0)))) β ((πΉβπ΄) β (πΊβπ΄)) = 0) |
89 | 88 | abs00bd 15177 |
. . . 4
β’ ((((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β§ π΄ β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0)))) β (absβ((πΉβπ΄) β (πΊβπ΄))) = 0) |
90 | 85, 89 | eqtrd 2777 |
. . 3
β’ ((((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β§ π΄ β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0)))) β ((πΉβπ΄)π(πΊβπ΄)) = 0) |
91 | 4, 51 | rrxmet 24775 |
. . . . 5
β’ (πΌ β π β π· β (Metβπ)) |
92 | 91 | ad3antrrr 729 |
. . . 4
β’ ((((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β§ π΄ β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0)))) β π· β (Metβπ)) |
93 | | metge0 23701 |
. . . 4
β’ ((π· β (Metβπ) β§ πΉ β π β§ πΊ β π) β 0 β€ (πΉπ·πΊ)) |
94 | 92, 58, 72, 93 | syl3anc 1372 |
. . 3
β’ ((((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β§ π΄ β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0)))) β 0 β€ (πΉπ·πΊ)) |
95 | 90, 94 | eqbrtrd 5128 |
. 2
β’ ((((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β§ π΄ β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0)))) β ((πΉβπ΄)π(πΊβπ΄)) β€ (πΉπ·πΊ)) |
96 | | simplr 768 |
. . . 4
β’ (((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β π΄ β πΌ) |
97 | | simprl 770 |
. . . . . . 7
β’ (((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β πΉ β π) |
98 | 4, 97 | rrxsuppss 24770 |
. . . . . 6
β’ (((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β (πΉ supp 0) β πΌ) |
99 | | simprr 772 |
. . . . . . 7
β’ (((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β πΊ β π) |
100 | 4, 99 | rrxsuppss 24770 |
. . . . . 6
β’ (((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β (πΊ supp 0) β πΌ) |
101 | 98, 100 | unssd 4147 |
. . . . 5
β’ (((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β ((πΉ supp 0) βͺ (πΊ supp 0)) β πΌ) |
102 | | undif 4442 |
. . . . 5
β’ (((πΉ supp 0) βͺ (πΊ supp 0)) β πΌ β (((πΉ supp 0) βͺ (πΊ supp 0)) βͺ (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0)))) = πΌ) |
103 | 101, 102 | sylib 217 |
. . . 4
β’ (((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β (((πΉ supp 0) βͺ (πΊ supp 0)) βͺ (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0)))) = πΌ) |
104 | 96, 103 | eleqtrrd 2841 |
. . 3
β’ (((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β π΄ β (((πΉ supp 0) βͺ (πΊ supp 0)) βͺ (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0))))) |
105 | | elun 4109 |
. . 3
β’ (π΄ β (((πΉ supp 0) βͺ (πΊ supp 0)) βͺ (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0)))) β (π΄ β ((πΉ supp 0) βͺ (πΊ supp 0)) β¨ π΄ β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0))))) |
106 | 104, 105 | sylib 217 |
. 2
β’ (((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β (π΄ β ((πΉ supp 0) βͺ (πΊ supp 0)) β¨ π΄ β (πΌ β ((πΉ supp 0) βͺ (πΊ supp 0))))) |
107 | 56, 95, 106 | mpjaodan 958 |
1
β’ (((πΌ β π β§ π΄ β πΌ) β§ (πΉ β π β§ πΊ β π)) β ((πΉβπ΄)π(πΊβπ΄)) β€ (πΉπ·πΊ)) |