Step | Hyp | Ref
| Expression |
1 | | carsgclctun.2 |
. . . 4
β’ (π β π΄ β (toCaraSigaβπ)) |
2 | 1 | unissd 4918 |
. . 3
β’ (π β βͺ π΄
β βͺ (toCaraSigaβπ)) |
3 | | carsgval.1 |
. . . 4
β’ (π β π β π) |
4 | | carsgval.2 |
. . . 4
β’ (π β π:π« πβΆ(0[,]+β)) |
5 | | carsgsiga.1 |
. . . 4
β’ (π β (πββ
) = 0) |
6 | 3, 4, 5 | carsguni 33376 |
. . 3
β’ (π β βͺ (toCaraSigaβπ) = π) |
7 | 2, 6 | sseqtrd 4022 |
. 2
β’ (π β βͺ π΄
β π) |
8 | 3 | adantr 481 |
. . . . . 6
β’ ((π β§ π β π« π) β π β π) |
9 | 4 | adantr 481 |
. . . . . 6
β’ ((π β§ π β π« π) β π:π« πβΆ(0[,]+β)) |
10 | 5 | adantr 481 |
. . . . . 6
β’ ((π β§ π β π« π) β (πββ
) = 0) |
11 | | carsgsiga.2 |
. . . . . . 7
β’ ((π β§ π₯ βΌ Ο β§ π₯ β π« π) β (πββͺ π₯) β€ Ξ£*π¦ β π₯(πβπ¦)) |
12 | 11 | 3adant1r 1177 |
. . . . . 6
β’ (((π β§ π β π« π) β§ π₯ βΌ Ο β§ π₯ β π« π) β (πββͺ π₯) β€ Ξ£*π¦ β π₯(πβπ¦)) |
13 | | carsgsiga.3 |
. . . . . . 7
β’ ((π β§ π₯ β π¦ β§ π¦ β π« π) β (πβπ₯) β€ (πβπ¦)) |
14 | 13 | 3adant1r 1177 |
. . . . . 6
β’ (((π β§ π β π« π) β§ π₯ β π¦ β§ π¦ β π« π) β (πβπ₯) β€ (πβπ¦)) |
15 | | carsgclctun.1 |
. . . . . . 7
β’ (π β π΄ βΌ Ο) |
16 | 15 | adantr 481 |
. . . . . 6
β’ ((π β§ π β π« π) β π΄ βΌ Ο) |
17 | 1 | adantr 481 |
. . . . . 6
β’ ((π β§ π β π« π) β π΄ β (toCaraSigaβπ)) |
18 | | simpr 485 |
. . . . . 6
β’ ((π β§ π β π« π) β π β π« π) |
19 | 8, 9, 10, 12, 14, 16, 17, 18 | carsgclctunlem3 33388 |
. . . . 5
β’ ((π β§ π β π« π) β ((πβ(π β© βͺ π΄)) +π (πβ(π β βͺ π΄))) β€ (πβπ)) |
20 | | inex1g 5319 |
. . . . . . . . 9
β’ (π β π« π β (π β© βͺ π΄) β V) |
21 | 20 | adantl 482 |
. . . . . . . 8
β’ ((π β§ π β π« π) β (π β© βͺ π΄) β V) |
22 | | difexg 5327 |
. . . . . . . . 9
β’ (π β π« π β (π β βͺ π΄) β V) |
23 | 22 | adantl 482 |
. . . . . . . 8
β’ ((π β§ π β π« π) β (π β βͺ π΄) β V) |
24 | | prct 31977 |
. . . . . . . 8
β’ (((π β© βͺ π΄)
β V β§ (π β
βͺ π΄) β V) β {(π β© βͺ π΄), (π β βͺ π΄)} βΌ
Ο) |
25 | 21, 23, 24 | syl2anc 584 |
. . . . . . 7
β’ ((π β§ π β π« π) β {(π β© βͺ π΄), (π β βͺ π΄)} βΌ
Ο) |
26 | 18 | elpwincl1 31801 |
. . . . . . . 8
β’ ((π β§ π β π« π) β (π β© βͺ π΄) β π« π) |
27 | 18 | elpwdifcl 31802 |
. . . . . . . 8
β’ ((π β§ π β π« π) β (π β βͺ π΄) β π« π) |
28 | | prssi 4824 |
. . . . . . . 8
β’ (((π β© βͺ π΄)
β π« π β§
(π β βͺ π΄)
β π« π) β
{(π β© βͺ π΄),
(π β βͺ π΄)}
β π« π) |
29 | 26, 27, 28 | syl2anc 584 |
. . . . . . 7
β’ ((π β§ π β π« π) β {(π β© βͺ π΄), (π β βͺ π΄)} β π« π) |
30 | | prex 5432 |
. . . . . . . . 9
β’ {(π β© βͺ π΄),
(π β βͺ π΄)}
β V |
31 | | breq1 5151 |
. . . . . . . . . . . 12
β’ (π₯ = {(π β© βͺ π΄), (π β βͺ π΄)} β (π₯ βΌ Ο β {(π β© βͺ π΄), (π β βͺ π΄)} βΌ
Ο)) |
32 | | sseq1 4007 |
. . . . . . . . . . . 12
β’ (π₯ = {(π β© βͺ π΄), (π β βͺ π΄)} β (π₯ β π« π β {(π β© βͺ π΄), (π β βͺ π΄)} β π« π)) |
33 | 31, 32 | 3anbi23d 1439 |
. . . . . . . . . . 11
β’ (π₯ = {(π β© βͺ π΄), (π β βͺ π΄)} β ((π β§ π₯ βΌ Ο β§ π₯ β π« π) β (π β§ {(π β© βͺ π΄), (π β βͺ π΄)} βΌ Ο β§ {(π β© βͺ π΄),
(π β βͺ π΄)}
β π« π))) |
34 | | unieq 4919 |
. . . . . . . . . . . . 13
β’ (π₯ = {(π β© βͺ π΄), (π β βͺ π΄)} β βͺ π₯ =
βͺ {(π β© βͺ π΄), (π β βͺ π΄)}) |
35 | 34 | fveq2d 6895 |
. . . . . . . . . . . 12
β’ (π₯ = {(π β© βͺ π΄), (π β βͺ π΄)} β (πββͺ π₯) = (πββͺ {(π β© βͺ π΄),
(π β βͺ π΄)})) |
36 | | esumeq1 33101 |
. . . . . . . . . . . 12
β’ (π₯ = {(π β© βͺ π΄), (π β βͺ π΄)} β
Ξ£*π¦ β
π₯(πβπ¦) = Ξ£*π¦ β {(π β© βͺ π΄), (π β βͺ π΄)} (πβπ¦)) |
37 | 35, 36 | breq12d 5161 |
. . . . . . . . . . 11
β’ (π₯ = {(π β© βͺ π΄), (π β βͺ π΄)} β ((πββͺ π₯) β€ Ξ£*π¦ β π₯(πβπ¦) β (πββͺ {(π β© βͺ π΄),
(π β βͺ π΄)})
β€ Ξ£*π¦
β {(π β© βͺ π΄),
(π β βͺ π΄)}
(πβπ¦))) |
38 | 33, 37 | imbi12d 344 |
. . . . . . . . . 10
β’ (π₯ = {(π β© βͺ π΄), (π β βͺ π΄)} β (((π β§ π₯ βΌ Ο β§ π₯ β π« π) β (πββͺ π₯) β€ Ξ£*π¦ β π₯(πβπ¦)) β ((π β§ {(π β© βͺ π΄), (π β βͺ π΄)} βΌ Ο β§ {(π β© βͺ π΄),
(π β βͺ π΄)}
β π« π) β
(πββͺ {(π
β© βͺ π΄), (π β βͺ π΄)}) β€
Ξ£*π¦ β
{(π β© βͺ π΄),
(π β βͺ π΄)}
(πβπ¦)))) |
39 | 38, 11 | vtoclg 3556 |
. . . . . . . . 9
β’ ({(π β© βͺ π΄),
(π β βͺ π΄)}
β V β ((π β§
{(π β© βͺ π΄),
(π β βͺ π΄)}
βΌ Ο β§ {(π
β© βͺ π΄), (π β βͺ π΄)} β π« π) β (πββͺ {(π β© βͺ π΄),
(π β βͺ π΄)})
β€ Ξ£*π¦
β {(π β© βͺ π΄),
(π β βͺ π΄)}
(πβπ¦))) |
40 | 30, 39 | ax-mp 5 |
. . . . . . . 8
β’ ((π β§ {(π β© βͺ π΄), (π β βͺ π΄)} βΌ Ο β§ {(π β© βͺ π΄),
(π β βͺ π΄)}
β π« π) β
(πββͺ {(π
β© βͺ π΄), (π β βͺ π΄)}) β€
Ξ£*π¦ β
{(π β© βͺ π΄),
(π β βͺ π΄)}
(πβπ¦)) |
41 | 40 | 3adant1r 1177 |
. . . . . . 7
β’ (((π β§ π β π« π) β§ {(π β© βͺ π΄), (π β βͺ π΄)} βΌ Ο β§ {(π β© βͺ π΄),
(π β βͺ π΄)}
β π« π) β
(πββͺ {(π
β© βͺ π΄), (π β βͺ π΄)}) β€
Ξ£*π¦ β
{(π β© βͺ π΄),
(π β βͺ π΄)}
(πβπ¦)) |
42 | 25, 29, 41 | mpd3an23 1463 |
. . . . . 6
β’ ((π β§ π β π« π) β (πββͺ {(π β© βͺ π΄),
(π β βͺ π΄)})
β€ Ξ£*π¦
β {(π β© βͺ π΄),
(π β βͺ π΄)}
(πβπ¦)) |
43 | | uniprg 4925 |
. . . . . . . . 9
β’ (((π β© βͺ π΄)
β π« π β§
(π β βͺ π΄)
β π« π) β
βͺ {(π β© βͺ π΄), (π β βͺ π΄)} = ((π β© βͺ π΄) βͺ (π β βͺ π΄))) |
44 | 26, 27, 43 | syl2anc 584 |
. . . . . . . 8
β’ ((π β§ π β π« π) β βͺ
{(π β© βͺ π΄),
(π β βͺ π΄)}
= ((π β© βͺ π΄)
βͺ (π β βͺ π΄))) |
45 | | inundif 4478 |
. . . . . . . 8
β’ ((π β© βͺ π΄)
βͺ (π β βͺ π΄))
= π |
46 | 44, 45 | eqtrdi 2788 |
. . . . . . 7
β’ ((π β§ π β π« π) β βͺ
{(π β© βͺ π΄),
(π β βͺ π΄)}
= π) |
47 | 46 | fveq2d 6895 |
. . . . . 6
β’ ((π β§ π β π« π) β (πββͺ {(π β© βͺ π΄),
(π β βͺ π΄)})
= (πβπ)) |
48 | | simpr 485 |
. . . . . . . 8
β’ (((π β§ π β π« π) β§ π¦ = (π β© βͺ π΄)) β π¦ = (π β© βͺ π΄)) |
49 | 48 | fveq2d 6895 |
. . . . . . 7
β’ (((π β§ π β π« π) β§ π¦ = (π β© βͺ π΄)) β (πβπ¦) = (πβ(π β© βͺ π΄))) |
50 | | simpr 485 |
. . . . . . . 8
β’ (((π β§ π β π« π) β§ π¦ = (π β βͺ π΄)) β π¦ = (π β βͺ π΄)) |
51 | 50 | fveq2d 6895 |
. . . . . . 7
β’ (((π β§ π β π« π) β§ π¦ = (π β βͺ π΄)) β (πβπ¦) = (πβ(π β βͺ π΄))) |
52 | 9, 26 | ffvelcdmd 7087 |
. . . . . . 7
β’ ((π β§ π β π« π) β (πβ(π β© βͺ π΄)) β
(0[,]+β)) |
53 | 9, 27 | ffvelcdmd 7087 |
. . . . . . 7
β’ ((π β§ π β π« π) β (πβ(π β βͺ π΄)) β
(0[,]+β)) |
54 | | ineq2 4206 |
. . . . . . . . . . . . 13
β’ ((π β© βͺ π΄) =
(π β βͺ π΄)
β ((π β© βͺ π΄)
β© (π β© βͺ π΄))
= ((π β© βͺ π΄)
β© (π β βͺ π΄))) |
55 | | inidm 4218 |
. . . . . . . . . . . . 13
β’ ((π β© βͺ π΄)
β© (π β© βͺ π΄))
= (π β© βͺ π΄) |
56 | | inindif 31792 |
. . . . . . . . . . . . 13
β’ ((π β© βͺ π΄)
β© (π β βͺ π΄))
= β
|
57 | 54, 55, 56 | 3eqtr3g 2795 |
. . . . . . . . . . . 12
β’ ((π β© βͺ π΄) =
(π β βͺ π΄)
β (π β© βͺ π΄) =
β
) |
58 | 57 | adantl 482 |
. . . . . . . . . . 11
β’ (((π β§ π β π« π) β§ (π β© βͺ π΄) = (π β βͺ π΄)) β (π β© βͺ π΄) = β
) |
59 | 58 | fveq2d 6895 |
. . . . . . . . . 10
β’ (((π β§ π β π« π) β§ (π β© βͺ π΄) = (π β βͺ π΄)) β (πβ(π β© βͺ π΄)) = (πββ
)) |
60 | 5 | ad2antrr 724 |
. . . . . . . . . 10
β’ (((π β§ π β π« π) β§ (π β© βͺ π΄) = (π β βͺ π΄)) β (πββ
) = 0) |
61 | 59, 60 | eqtrd 2772 |
. . . . . . . . 9
β’ (((π β§ π β π« π) β§ (π β© βͺ π΄) = (π β βͺ π΄)) β (πβ(π β© βͺ π΄)) = 0) |
62 | 61 | orcd 871 |
. . . . . . . 8
β’ (((π β§ π β π« π) β§ (π β© βͺ π΄) = (π β βͺ π΄)) β ((πβ(π β© βͺ π΄)) = 0 β¨ (πβ(π β© βͺ π΄)) = +β)) |
63 | 62 | ex 413 |
. . . . . . 7
β’ ((π β§ π β π« π) β ((π β© βͺ π΄) = (π β βͺ π΄) β ((πβ(π β© βͺ π΄)) = 0 β¨ (πβ(π β© βͺ π΄)) =
+β))) |
64 | 49, 51, 26, 27, 52, 53, 63 | esumpr2 33134 |
. . . . . 6
β’ ((π β§ π β π« π) β Ξ£*π¦ β {(π β© βͺ π΄), (π β βͺ π΄)} (πβπ¦) = ((πβ(π β© βͺ π΄)) +π (πβ(π β βͺ π΄)))) |
65 | 42, 47, 64 | 3brtr3d 5179 |
. . . . 5
β’ ((π β§ π β π« π) β (πβπ) β€ ((πβ(π β© βͺ π΄)) +π (πβ(π β βͺ π΄)))) |
66 | 19, 65 | jca 512 |
. . . 4
β’ ((π β§ π β π« π) β (((πβ(π β© βͺ π΄)) +π (πβ(π β βͺ π΄))) β€ (πβπ) β§ (πβπ) β€ ((πβ(π β© βͺ π΄)) +π (πβ(π β βͺ π΄))))) |
67 | | iccssxr 13409 |
. . . . . . 7
β’
(0[,]+β) β β* |
68 | 67, 52 | sselid 3980 |
. . . . . 6
β’ ((π β§ π β π« π) β (πβ(π β© βͺ π΄)) β
β*) |
69 | 67, 53 | sselid 3980 |
. . . . . 6
β’ ((π β§ π β π« π) β (πβ(π β βͺ π΄)) β
β*) |
70 | 68, 69 | xaddcld 13282 |
. . . . 5
β’ ((π β§ π β π« π) β ((πβ(π β© βͺ π΄)) +π (πβ(π β βͺ π΄))) β
β*) |
71 | 4 | ffvelcdmda 7086 |
. . . . . 6
β’ ((π β§ π β π« π) β (πβπ) β (0[,]+β)) |
72 | 67, 71 | sselid 3980 |
. . . . 5
β’ ((π β§ π β π« π) β (πβπ) β
β*) |
73 | | xrletri3 13135 |
. . . . 5
β’ ((((πβ(π β© βͺ π΄)) +π (πβ(π β βͺ π΄))) β β*
β§ (πβπ) β β*)
β (((πβ(π β© βͺ π΄))
+π (πβ(π β βͺ π΄))) = (πβπ) β (((πβ(π β© βͺ π΄)) +π (πβ(π β βͺ π΄))) β€ (πβπ) β§ (πβπ) β€ ((πβ(π β© βͺ π΄)) +π (πβ(π β βͺ π΄)))))) |
74 | 70, 72, 73 | syl2anc 584 |
. . . 4
β’ ((π β§ π β π« π) β (((πβ(π β© βͺ π΄)) +π (πβ(π β βͺ π΄))) = (πβπ) β (((πβ(π β© βͺ π΄)) +π (πβ(π β βͺ π΄))) β€ (πβπ) β§ (πβπ) β€ ((πβ(π β© βͺ π΄)) +π (πβ(π β βͺ π΄)))))) |
75 | 66, 74 | mpbird 256 |
. . 3
β’ ((π β§ π β π« π) β ((πβ(π β© βͺ π΄)) +π (πβ(π β βͺ π΄))) = (πβπ)) |
76 | 75 | ralrimiva 3146 |
. 2
β’ (π β βπ β π« π((πβ(π β© βͺ π΄)) +π (πβ(π β βͺ π΄))) = (πβπ)) |
77 | 3, 4 | elcarsg 33373 |
. 2
β’ (π β (βͺ π΄
β (toCaraSigaβπ)
β (βͺ π΄ β π β§ βπ β π« π((πβ(π β© βͺ π΄)) +π (πβ(π β βͺ π΄))) = (πβπ)))) |
78 | 7, 76, 77 | mpbir2and 711 |
1
β’ (π β βͺ π΄
β (toCaraSigaβπ)) |