Step | Hyp | Ref
| Expression |
1 | | o1f 15417 |
. . . 4
β’ (πΉ β π(1) β
πΉ:dom πΉβΆβ) |
2 | | o1bdd 15419 |
. . . 4
β’ ((πΉ β π(1) β§ πΉ:dom πΉβΆβ) β βπ β β βπ β β βπ§ β dom πΉ(π β€ π§ β (absβ(πΉβπ§)) β€ π)) |
3 | 1, 2 | mpdan 686 |
. . 3
β’ (πΉ β π(1) β
βπ β β
βπ β β
βπ§ β dom πΉ(π β€ π§ β (absβ(πΉβπ§)) β€ π)) |
4 | 3 | adantr 482 |
. 2
β’ ((πΉ β π(1) β§ πΊ β π(1)) β
βπ β β
βπ β β
βπ§ β dom πΉ(π β€ π§ β (absβ(πΉβπ§)) β€ π)) |
5 | | o1f 15417 |
. . . 4
β’ (πΊ β π(1) β
πΊ:dom πΊβΆβ) |
6 | | o1bdd 15419 |
. . . 4
β’ ((πΊ β π(1) β§ πΊ:dom πΊβΆβ) β βπ β β βπ β β βπ§ β dom πΊ(π β€ π§ β (absβ(πΊβπ§)) β€ π)) |
7 | 5, 6 | mpdan 686 |
. . 3
β’ (πΊ β π(1) β
βπ β β
βπ β β
βπ§ β dom πΊ(π β€ π§ β (absβ(πΊβπ§)) β€ π)) |
8 | 7 | adantl 483 |
. 2
β’ ((πΉ β π(1) β§ πΊ β π(1)) β
βπ β β
βπ β β
βπ§ β dom πΊ(π β€ π§ β (absβ(πΊβπ§)) β€ π)) |
9 | | reeanv 3216 |
. . 3
β’
(βπ β
β βπ β
β (βπ β
β βπ§ β
dom πΉ(π β€ π§ β (absβ(πΉβπ§)) β€ π) β§ βπ β β βπ§ β dom πΊ(π β€ π§ β (absβ(πΊβπ§)) β€ π)) β (βπ β β βπ β β βπ§ β dom πΉ(π β€ π§ β (absβ(πΉβπ§)) β€ π) β§ βπ β β βπ β β βπ§ β dom πΊ(π β€ π§ β (absβ(πΊβπ§)) β€ π))) |
10 | | reeanv 3216 |
. . . . 5
β’
(βπ β
β βπ β
β (βπ§ β
dom πΉ(π β€ π§ β (absβ(πΉβπ§)) β€ π) β§ βπ§ β dom πΊ(π β€ π§ β (absβ(πΊβπ§)) β€ π)) β (βπ β β βπ§ β dom πΉ(π β€ π§ β (absβ(πΉβπ§)) β€ π) β§ βπ β β βπ§ β dom πΊ(π β€ π§ β (absβ(πΊβπ§)) β€ π))) |
11 | | inss1 4189 |
. . . . . . . . . 10
β’ (dom
πΉ β© dom πΊ) β dom πΉ |
12 | | ssralv 4011 |
. . . . . . . . . 10
β’ ((dom
πΉ β© dom πΊ) β dom πΉ β (βπ§ β dom πΉ(π β€ π§ β (absβ(πΉβπ§)) β€ π) β βπ§ β (dom πΉ β© dom πΊ)(π β€ π§ β (absβ(πΉβπ§)) β€ π))) |
13 | 11, 12 | ax-mp 5 |
. . . . . . . . 9
β’
(βπ§ β
dom πΉ(π β€ π§ β (absβ(πΉβπ§)) β€ π) β βπ§ β (dom πΉ β© dom πΊ)(π β€ π§ β (absβ(πΉβπ§)) β€ π)) |
14 | | inss2 4190 |
. . . . . . . . . 10
β’ (dom
πΉ β© dom πΊ) β dom πΊ |
15 | | ssralv 4011 |
. . . . . . . . . 10
β’ ((dom
πΉ β© dom πΊ) β dom πΊ β (βπ§ β dom πΊ(π β€ π§ β (absβ(πΊβπ§)) β€ π) β βπ§ β (dom πΉ β© dom πΊ)(π β€ π§ β (absβ(πΊβπ§)) β€ π))) |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . 9
β’
(βπ§ β
dom πΊ(π β€ π§ β (absβ(πΊβπ§)) β€ π) β βπ§ β (dom πΉ β© dom πΊ)(π β€ π§ β (absβ(πΊβπ§)) β€ π)) |
17 | 13, 16 | anim12i 614 |
. . . . . . . 8
β’
((βπ§ β
dom πΉ(π β€ π§ β (absβ(πΉβπ§)) β€ π) β§ βπ§ β dom πΊ(π β€ π§ β (absβ(πΊβπ§)) β€ π)) β (βπ§ β (dom πΉ β© dom πΊ)(π β€ π§ β (absβ(πΉβπ§)) β€ π) β§ βπ§ β (dom πΉ β© dom πΊ)(π β€ π§ β (absβ(πΊβπ§)) β€ π))) |
18 | | r19.26 3111 |
. . . . . . . 8
β’
(βπ§ β
(dom πΉ β© dom πΊ)((π β€ π§ β (absβ(πΉβπ§)) β€ π) β§ (π β€ π§ β (absβ(πΊβπ§)) β€ π)) β (βπ§ β (dom πΉ β© dom πΊ)(π β€ π§ β (absβ(πΉβπ§)) β€ π) β§ βπ§ β (dom πΉ β© dom πΊ)(π β€ π§ β (absβ(πΊβπ§)) β€ π))) |
19 | 17, 18 | sylibr 233 |
. . . . . . 7
β’
((βπ§ β
dom πΉ(π β€ π§ β (absβ(πΉβπ§)) β€ π) β§ βπ§ β dom πΊ(π β€ π§ β (absβ(πΊβπ§)) β€ π)) β βπ§ β (dom πΉ β© dom πΊ)((π β€ π§ β (absβ(πΉβπ§)) β€ π) β§ (π β€ π§ β (absβ(πΊβπ§)) β€ π))) |
20 | | anim12 808 |
. . . . . . . . . 10
β’ (((π β€ π§ β (absβ(πΉβπ§)) β€ π) β§ (π β€ π§ β (absβ(πΊβπ§)) β€ π)) β ((π β€ π§ β§ π β€ π§) β ((absβ(πΉβπ§)) β€ π β§ (absβ(πΊβπ§)) β€ π))) |
21 | | simplrl 776 |
. . . . . . . . . . . . . 14
β’ ((((πΉ β π(1) β§ πΊ β π(1)) β§
(π β β β§
π β β)) β§
(π β β β§
π β β)) β
π β
β) |
22 | 21 | adantr 482 |
. . . . . . . . . . . . 13
β’
(((((πΉ β
π(1) β§ πΊ β
π(1)) β§ (π
β β β§ π
β β)) β§ (π
β β β§ π
β β)) β§ π§
β (dom πΉ β© dom
πΊ)) β π β
β) |
23 | | simplrr 777 |
. . . . . . . . . . . . . 14
β’ ((((πΉ β π(1) β§ πΊ β π(1)) β§
(π β β β§
π β β)) β§
(π β β β§
π β β)) β
π β
β) |
24 | 23 | adantr 482 |
. . . . . . . . . . . . 13
β’
(((((πΉ β
π(1) β§ πΊ β
π(1)) β§ (π
β β β§ π
β β)) β§ (π
β β β§ π
β β)) β§ π§
β (dom πΉ β© dom
πΊ)) β π β
β) |
25 | | o1dm 15418 |
. . . . . . . . . . . . . . . 16
β’ (πΉ β π(1) β dom
πΉ β
β) |
26 | 25 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
β’ ((((πΉ β π(1) β§ πΊ β π(1)) β§
(π β β β§
π β β)) β§
(π β β β§
π β β)) β
dom πΉ β
β) |
27 | 11, 26 | sstrid 3956 |
. . . . . . . . . . . . . 14
β’ ((((πΉ β π(1) β§ πΊ β π(1)) β§
(π β β β§
π β β)) β§
(π β β β§
π β β)) β
(dom πΉ β© dom πΊ) β
β) |
28 | 27 | sselda 3945 |
. . . . . . . . . . . . 13
β’
(((((πΉ β
π(1) β§ πΊ β
π(1)) β§ (π
β β β§ π
β β)) β§ (π
β β β§ π
β β)) β§ π§
β (dom πΉ β© dom
πΊ)) β π§ β
β) |
29 | | maxle 13116 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π β β β§ π§ β β) β
(if(π β€ π, π, π) β€ π§ β (π β€ π§ β§ π β€ π§))) |
30 | 22, 24, 28, 29 | syl3anc 1372 |
. . . . . . . . . . . 12
β’
(((((πΉ β
π(1) β§ πΊ β
π(1)) β§ (π
β β β§ π
β β)) β§ (π
β β β§ π
β β)) β§ π§
β (dom πΉ β© dom
πΊ)) β (if(π β€ π, π, π) β€ π§ β (π β€ π§ β§ π β€ π§))) |
31 | 30 | biimpd 228 |
. . . . . . . . . . 11
β’
(((((πΉ β
π(1) β§ πΊ β
π(1)) β§ (π
β β β§ π
β β)) β§ (π
β β β§ π
β β)) β§ π§
β (dom πΉ β© dom
πΊ)) β (if(π β€ π, π, π) β€ π§ β (π β€ π§ β§ π β€ π§))) |
32 | 1 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
β’ ((((πΉ β π(1) β§ πΊ β π(1)) β§
(π β β β§
π β β)) β§
(π β β β§
π β β)) β
πΉ:dom πΉβΆβ) |
33 | 11 | sseli 3941 |
. . . . . . . . . . . . . 14
β’ (π§ β (dom πΉ β© dom πΊ) β π§ β dom πΉ) |
34 | | ffvelcdm 7033 |
. . . . . . . . . . . . . 14
β’ ((πΉ:dom πΉβΆβ β§ π§ β dom πΉ) β (πΉβπ§) β β) |
35 | 32, 33, 34 | syl2an 597 |
. . . . . . . . . . . . 13
β’
(((((πΉ β
π(1) β§ πΊ β
π(1)) β§ (π
β β β§ π
β β)) β§ (π
β β β§ π
β β)) β§ π§
β (dom πΉ β© dom
πΊ)) β (πΉβπ§) β β) |
36 | 5 | ad3antlr 730 |
. . . . . . . . . . . . . 14
β’ ((((πΉ β π(1) β§ πΊ β π(1)) β§
(π β β β§
π β β)) β§
(π β β β§
π β β)) β
πΊ:dom πΊβΆβ) |
37 | 14 | sseli 3941 |
. . . . . . . . . . . . . 14
β’ (π§ β (dom πΉ β© dom πΊ) β π§ β dom πΊ) |
38 | | ffvelcdm 7033 |
. . . . . . . . . . . . . 14
β’ ((πΊ:dom πΊβΆβ β§ π§ β dom πΊ) β (πΊβπ§) β β) |
39 | 36, 37, 38 | syl2an 597 |
. . . . . . . . . . . . 13
β’
(((((πΉ β
π(1) β§ πΊ β
π(1)) β§ (π
β β β§ π
β β)) β§ (π
β β β§ π
β β)) β§ π§
β (dom πΉ β© dom
πΊ)) β (πΊβπ§) β β) |
40 | | o1of2.3 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ π β β) β§ (π₯ β β β§ π¦ β β)) β
(((absβπ₯) β€ π β§ (absβπ¦) β€ π) β (absβ(π₯π
π¦)) β€ π)) |
41 | 40 | ralrimivva 3194 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β β) β
βπ₯ β β
βπ¦ β β
(((absβπ₯) β€ π β§ (absβπ¦) β€ π) β (absβ(π₯π
π¦)) β€ π)) |
42 | 41 | ad2antlr 726 |
. . . . . . . . . . . . 13
β’
(((((πΉ β
π(1) β§ πΊ β
π(1)) β§ (π
β β β§ π
β β)) β§ (π
β β β§ π
β β)) β§ π§
β (dom πΉ β© dom
πΊ)) β βπ₯ β β βπ¦ β β
(((absβπ₯) β€ π β§ (absβπ¦) β€ π) β (absβ(π₯π
π¦)) β€ π)) |
43 | | fveq2 6843 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = (πΉβπ§) β (absβπ₯) = (absβ(πΉβπ§))) |
44 | 43 | breq1d 5116 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = (πΉβπ§) β ((absβπ₯) β€ π β (absβ(πΉβπ§)) β€ π)) |
45 | 44 | anbi1d 631 |
. . . . . . . . . . . . . . 15
β’ (π₯ = (πΉβπ§) β (((absβπ₯) β€ π β§ (absβπ¦) β€ π) β ((absβ(πΉβπ§)) β€ π β§ (absβπ¦) β€ π))) |
46 | | fvoveq1 7381 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = (πΉβπ§) β (absβ(π₯π
π¦)) = (absβ((πΉβπ§)π
π¦))) |
47 | 46 | breq1d 5116 |
. . . . . . . . . . . . . . 15
β’ (π₯ = (πΉβπ§) β ((absβ(π₯π
π¦)) β€ π β (absβ((πΉβπ§)π
π¦)) β€ π)) |
48 | 45, 47 | imbi12d 345 |
. . . . . . . . . . . . . 14
β’ (π₯ = (πΉβπ§) β ((((absβπ₯) β€ π β§ (absβπ¦) β€ π) β (absβ(π₯π
π¦)) β€ π) β (((absβ(πΉβπ§)) β€ π β§ (absβπ¦) β€ π) β (absβ((πΉβπ§)π
π¦)) β€ π))) |
49 | | fveq2 6843 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = (πΊβπ§) β (absβπ¦) = (absβ(πΊβπ§))) |
50 | 49 | breq1d 5116 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = (πΊβπ§) β ((absβπ¦) β€ π β (absβ(πΊβπ§)) β€ π)) |
51 | 50 | anbi2d 630 |
. . . . . . . . . . . . . . 15
β’ (π¦ = (πΊβπ§) β (((absβ(πΉβπ§)) β€ π β§ (absβπ¦) β€ π) β ((absβ(πΉβπ§)) β€ π β§ (absβ(πΊβπ§)) β€ π))) |
52 | | oveq2 7366 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = (πΊβπ§) β ((πΉβπ§)π
π¦) = ((πΉβπ§)π
(πΊβπ§))) |
53 | 52 | fveq2d 6847 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = (πΊβπ§) β (absβ((πΉβπ§)π
π¦)) = (absβ((πΉβπ§)π
(πΊβπ§)))) |
54 | 53 | breq1d 5116 |
. . . . . . . . . . . . . . 15
β’ (π¦ = (πΊβπ§) β ((absβ((πΉβπ§)π
π¦)) β€ π β (absβ((πΉβπ§)π
(πΊβπ§))) β€ π)) |
55 | 51, 54 | imbi12d 345 |
. . . . . . . . . . . . . 14
β’ (π¦ = (πΊβπ§) β ((((absβ(πΉβπ§)) β€ π β§ (absβπ¦) β€ π) β (absβ((πΉβπ§)π
π¦)) β€ π) β (((absβ(πΉβπ§)) β€ π β§ (absβ(πΊβπ§)) β€ π) β (absβ((πΉβπ§)π
(πΊβπ§))) β€ π))) |
56 | 48, 55 | rspc2va 3590 |
. . . . . . . . . . . . 13
β’ ((((πΉβπ§) β β β§ (πΊβπ§) β β) β§ βπ₯ β β βπ¦ β β
(((absβπ₯) β€ π β§ (absβπ¦) β€ π) β (absβ(π₯π
π¦)) β€ π)) β (((absβ(πΉβπ§)) β€ π β§ (absβ(πΊβπ§)) β€ π) β (absβ((πΉβπ§)π
(πΊβπ§))) β€ π)) |
57 | 35, 39, 42, 56 | syl21anc 837 |
. . . . . . . . . . . 12
β’
(((((πΉ β
π(1) β§ πΊ β
π(1)) β§ (π
β β β§ π
β β)) β§ (π
β β β§ π
β β)) β§ π§
β (dom πΉ β© dom
πΊ)) β
(((absβ(πΉβπ§)) β€ π β§ (absβ(πΊβπ§)) β€ π) β (absβ((πΉβπ§)π
(πΊβπ§))) β€ π)) |
58 | 32 | ffnd 6670 |
. . . . . . . . . . . . . . 15
β’ ((((πΉ β π(1) β§ πΊ β π(1)) β§
(π β β β§
π β β)) β§
(π β β β§
π β β)) β
πΉ Fn dom πΉ) |
59 | 36 | ffnd 6670 |
. . . . . . . . . . . . . . 15
β’ ((((πΉ β π(1) β§ πΊ β π(1)) β§
(π β β β§
π β β)) β§
(π β β β§
π β β)) β
πΊ Fn dom πΊ) |
60 | | reex 11147 |
. . . . . . . . . . . . . . . 16
β’ β
β V |
61 | | ssexg 5281 |
. . . . . . . . . . . . . . . 16
β’ ((dom
πΉ β β β§
β β V) β dom πΉ β V) |
62 | 26, 60, 61 | sylancl 587 |
. . . . . . . . . . . . . . 15
β’ ((((πΉ β π(1) β§ πΊ β π(1)) β§
(π β β β§
π β β)) β§
(π β β β§
π β β)) β
dom πΉ β
V) |
63 | | dmexg 7841 |
. . . . . . . . . . . . . . . 16
β’ (πΊ β π(1) β dom
πΊ β
V) |
64 | 63 | ad3antlr 730 |
. . . . . . . . . . . . . . 15
β’ ((((πΉ β π(1) β§ πΊ β π(1)) β§
(π β β β§
π β β)) β§
(π β β β§
π β β)) β
dom πΊ β
V) |
65 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’ (dom
πΉ β© dom πΊ) = (dom πΉ β© dom πΊ) |
66 | | eqidd 2734 |
. . . . . . . . . . . . . . 15
β’
(((((πΉ β
π(1) β§ πΊ β
π(1)) β§ (π
β β β§ π
β β)) β§ (π
β β β§ π
β β)) β§ π§
β dom πΉ) β (πΉβπ§) = (πΉβπ§)) |
67 | | eqidd 2734 |
. . . . . . . . . . . . . . 15
β’
(((((πΉ β
π(1) β§ πΊ β
π(1)) β§ (π
β β β§ π
β β)) β§ (π
β β β§ π
β β)) β§ π§
β dom πΊ) β (πΊβπ§) = (πΊβπ§)) |
68 | 58, 59, 62, 64, 65, 66, 67 | ofval 7629 |
. . . . . . . . . . . . . 14
β’
(((((πΉ β
π(1) β§ πΊ β
π(1)) β§ (π
β β β§ π
β β)) β§ (π
β β β§ π
β β)) β§ π§
β (dom πΉ β© dom
πΊ)) β ((πΉ βf π
πΊ)βπ§) = ((πΉβπ§)π
(πΊβπ§))) |
69 | 68 | fveq2d 6847 |
. . . . . . . . . . . . 13
β’
(((((πΉ β
π(1) β§ πΊ β
π(1)) β§ (π
β β β§ π
β β)) β§ (π
β β β§ π
β β)) β§ π§
β (dom πΉ β© dom
πΊ)) β
(absβ((πΉ
βf π
πΊ)βπ§)) = (absβ((πΉβπ§)π
(πΊβπ§)))) |
70 | 69 | breq1d 5116 |
. . . . . . . . . . . 12
β’
(((((πΉ β
π(1) β§ πΊ β
π(1)) β§ (π
β β β§ π
β β)) β§ (π
β β β§ π
β β)) β§ π§
β (dom πΉ β© dom
πΊ)) β
((absβ((πΉ
βf π
πΊ)βπ§)) β€ π β (absβ((πΉβπ§)π
(πΊβπ§))) β€ π)) |
71 | 57, 70 | sylibrd 259 |
. . . . . . . . . . 11
β’
(((((πΉ β
π(1) β§ πΊ β
π(1)) β§ (π
β β β§ π
β β)) β§ (π
β β β§ π
β β)) β§ π§
β (dom πΉ β© dom
πΊ)) β
(((absβ(πΉβπ§)) β€ π β§ (absβ(πΊβπ§)) β€ π) β (absβ((πΉ βf π
πΊ)βπ§)) β€ π)) |
72 | 31, 71 | imim12d 81 |
. . . . . . . . . 10
β’
(((((πΉ β
π(1) β§ πΊ β
π(1)) β§ (π
β β β§ π
β β)) β§ (π
β β β§ π
β β)) β§ π§
β (dom πΉ β© dom
πΊ)) β (((π β€ π§ β§ π β€ π§) β ((absβ(πΉβπ§)) β€ π β§ (absβ(πΊβπ§)) β€ π)) β (if(π β€ π, π, π) β€ π§ β (absβ((πΉ βf π
πΊ)βπ§)) β€ π))) |
73 | 20, 72 | syl5 34 |
. . . . . . . . 9
β’
(((((πΉ β
π(1) β§ πΊ β
π(1)) β§ (π
β β β§ π
β β)) β§ (π
β β β§ π
β β)) β§ π§
β (dom πΉ β© dom
πΊ)) β (((π β€ π§ β (absβ(πΉβπ§)) β€ π) β§ (π β€ π§ β (absβ(πΊβπ§)) β€ π)) β (if(π β€ π, π, π) β€ π§ β (absβ((πΉ βf π
πΊ)βπ§)) β€ π))) |
74 | 73 | ralimdva 3161 |
. . . . . . . 8
β’ ((((πΉ β π(1) β§ πΊ β π(1)) β§
(π β β β§
π β β)) β§
(π β β β§
π β β)) β
(βπ§ β (dom
πΉ β© dom πΊ)((π β€ π§ β (absβ(πΉβπ§)) β€ π) β§ (π β€ π§ β (absβ(πΊβπ§)) β€ π)) β βπ§ β (dom πΉ β© dom πΊ)(if(π β€ π, π, π) β€ π§ β (absβ((πΉ βf π
πΊ)βπ§)) β€ π))) |
75 | | o1of2.2 |
. . . . . . . . . . 11
β’ ((π₯ β β β§ π¦ β β) β (π₯π
π¦) β β) |
76 | 75 | adantl 483 |
. . . . . . . . . 10
β’
(((((πΉ β
π(1) β§ πΊ β
π(1)) β§ (π
β β β§ π
β β)) β§ (π
β β β§ π
β β)) β§ (π₯
β β β§ π¦
β β)) β (π₯π
π¦) β β) |
77 | 76, 32, 36, 62, 64, 65 | off 7636 |
. . . . . . . . 9
β’ ((((πΉ β π(1) β§ πΊ β π(1)) β§
(π β β β§
π β β)) β§
(π β β β§
π β β)) β
(πΉ βf
π
πΊ):(dom πΉ β© dom πΊ)βΆβ) |
78 | 23, 21 | ifcld 4533 |
. . . . . . . . 9
β’ ((((πΉ β π(1) β§ πΊ β π(1)) β§
(π β β β§
π β β)) β§
(π β β β§
π β β)) β
if(π β€ π, π, π) β β) |
79 | | o1of2.1 |
. . . . . . . . . 10
β’ ((π β β β§ π β β) β π β
β) |
80 | 79 | adantl 483 |
. . . . . . . . 9
β’ ((((πΉ β π(1) β§ πΊ β π(1)) β§
(π β β β§
π β β)) β§
(π β β β§
π β β)) β
π β
β) |
81 | | elo12r 15416 |
. . . . . . . . . 10
β’ ((((πΉ βf π
πΊ):(dom πΉ β© dom πΊ)βΆβ β§ (dom πΉ β© dom πΊ) β β) β§ (if(π β€ π, π, π) β β β§ π β β) β§ βπ§ β (dom πΉ β© dom πΊ)(if(π β€ π, π, π) β€ π§ β (absβ((πΉ βf π
πΊ)βπ§)) β€ π)) β (πΉ βf π
πΊ) β π(1)) |
82 | 81 | 3expia 1122 |
. . . . . . . . 9
β’ ((((πΉ βf π
πΊ):(dom πΉ β© dom πΊ)βΆβ β§ (dom πΉ β© dom πΊ) β β) β§ (if(π β€ π, π, π) β β β§ π β β)) β (βπ§ β (dom πΉ β© dom πΊ)(if(π β€ π, π, π) β€ π§ β (absβ((πΉ βf π
πΊ)βπ§)) β€ π) β (πΉ βf π
πΊ) β π(1))) |
83 | 77, 27, 78, 80, 82 | syl22anc 838 |
. . . . . . . 8
β’ ((((πΉ β π(1) β§ πΊ β π(1)) β§
(π β β β§
π β β)) β§
(π β β β§
π β β)) β
(βπ§ β (dom
πΉ β© dom πΊ)(if(π β€ π, π, π) β€ π§ β (absβ((πΉ βf π
πΊ)βπ§)) β€ π) β (πΉ βf π
πΊ) β π(1))) |
84 | 74, 83 | syld 47 |
. . . . . . 7
β’ ((((πΉ β π(1) β§ πΊ β π(1)) β§
(π β β β§
π β β)) β§
(π β β β§
π β β)) β
(βπ§ β (dom
πΉ β© dom πΊ)((π β€ π§ β (absβ(πΉβπ§)) β€ π) β§ (π β€ π§ β (absβ(πΊβπ§)) β€ π)) β (πΉ βf π
πΊ) β π(1))) |
85 | 19, 84 | syl5 34 |
. . . . . 6
β’ ((((πΉ β π(1) β§ πΊ β π(1)) β§
(π β β β§
π β β)) β§
(π β β β§
π β β)) β
((βπ§ β dom
πΉ(π β€ π§ β (absβ(πΉβπ§)) β€ π) β§ βπ§ β dom πΊ(π β€ π§ β (absβ(πΊβπ§)) β€ π)) β (πΉ βf π
πΊ) β π(1))) |
86 | 85 | rexlimdvva 3202 |
. . . . 5
β’ (((πΉ β π(1) β§ πΊ β π(1)) β§
(π β β β§
π β β)) β
(βπ β β
βπ β β
(βπ§ β dom πΉ(π β€ π§ β (absβ(πΉβπ§)) β€ π) β§ βπ§ β dom πΊ(π β€ π§ β (absβ(πΊβπ§)) β€ π)) β (πΉ βf π
πΊ) β π(1))) |
87 | 10, 86 | biimtrrid 242 |
. . . 4
β’ (((πΉ β π(1) β§ πΊ β π(1)) β§
(π β β β§
π β β)) β
((βπ β β
βπ§ β dom πΉ(π β€ π§ β (absβ(πΉβπ§)) β€ π) β§ βπ β β βπ§ β dom πΊ(π β€ π§ β (absβ(πΊβπ§)) β€ π)) β (πΉ βf π
πΊ) β π(1))) |
88 | 87 | rexlimdvva 3202 |
. . 3
β’ ((πΉ β π(1) β§ πΊ β π(1)) β
(βπ β β
βπ β β
(βπ β β
βπ§ β dom πΉ(π β€ π§ β (absβ(πΉβπ§)) β€ π) β§ βπ β β βπ§ β dom πΊ(π β€ π§ β (absβ(πΊβπ§)) β€ π)) β (πΉ βf π
πΊ) β π(1))) |
89 | 9, 88 | biimtrrid 242 |
. 2
β’ ((πΉ β π(1) β§ πΊ β π(1)) β
((βπ β β
βπ β β
βπ§ β dom πΉ(π β€ π§ β (absβ(πΉβπ§)) β€ π) β§ βπ β β βπ β β βπ§ β dom πΊ(π β€ π§ β (absβ(πΊβπ§)) β€ π)) β (πΉ βf π
πΊ) β π(1))) |
90 | 4, 8, 89 | mp2and 698 |
1
β’ ((πΉ β π(1) β§ πΊ β π(1)) β
(πΉ βf
π
πΊ) β π(1)) |