Step | Hyp | Ref
| Expression |
1 | | difssd 4133 |
. . 3
β’ (π β (π β π΄) β π) |
2 | | indif2 4271 |
. . . . . . . 8
β’ (π β© (π β π΄)) = ((π β© π) β π΄) |
3 | | elpwi 4610 |
. . . . . . . . . . 11
β’ (π β π« π β π β π) |
4 | 3 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β π« π) β π β π) |
5 | | df-ss 3966 |
. . . . . . . . . 10
β’ (π β π β (π β© π) = π) |
6 | 4, 5 | sylib 217 |
. . . . . . . . 9
β’ ((π β§ π β π« π) β (π β© π) = π) |
7 | 6 | difeq1d 4122 |
. . . . . . . 8
β’ ((π β§ π β π« π) β ((π β© π) β π΄) = (π β π΄)) |
8 | 2, 7 | eqtrid 2785 |
. . . . . . 7
β’ ((π β§ π β π« π) β (π β© (π β π΄)) = (π β π΄)) |
9 | 8 | fveq2d 6896 |
. . . . . 6
β’ ((π β§ π β π« π) β (πβ(π β© (π β π΄))) = (πβ(π β π΄))) |
10 | | difdif2 4287 |
. . . . . . . 8
β’ (π β (π β π΄)) = ((π β π) βͺ (π β© π΄)) |
11 | | ssdif0 4364 |
. . . . . . . . . . 11
β’ (π β π β (π β π) = β
) |
12 | 4, 11 | sylib 217 |
. . . . . . . . . 10
β’ ((π β§ π β π« π) β (π β π) = β
) |
13 | 12 | uneq1d 4163 |
. . . . . . . . 9
β’ ((π β§ π β π« π) β ((π β π) βͺ (π β© π΄)) = (β
βͺ (π β© π΄))) |
14 | | uncom 4154 |
. . . . . . . . . 10
β’ ((π β© π΄) βͺ β
) = (β
βͺ (π β© π΄)) |
15 | | un0 4391 |
. . . . . . . . . 10
β’ ((π β© π΄) βͺ β
) = (π β© π΄) |
16 | 14, 15 | eqtr3i 2763 |
. . . . . . . . 9
β’ (β
βͺ (π β© π΄)) = (π β© π΄) |
17 | 13, 16 | eqtrdi 2789 |
. . . . . . . 8
β’ ((π β§ π β π« π) β ((π β π) βͺ (π β© π΄)) = (π β© π΄)) |
18 | 10, 17 | eqtrid 2785 |
. . . . . . 7
β’ ((π β§ π β π« π) β (π β (π β π΄)) = (π β© π΄)) |
19 | 18 | fveq2d 6896 |
. . . . . 6
β’ ((π β§ π β π« π) β (πβ(π β (π β π΄))) = (πβ(π β© π΄))) |
20 | 9, 19 | oveq12d 7427 |
. . . . 5
β’ ((π β§ π β π« π) β ((πβ(π β© (π β π΄))) +π (πβ(π β (π β π΄)))) = ((πβ(π β π΄)) +π (πβ(π β© π΄)))) |
21 | | iccssxr 13407 |
. . . . . . 7
β’
(0[,]+β) β β* |
22 | | carsgval.2 |
. . . . . . . . 9
β’ (π β π:π« πβΆ(0[,]+β)) |
23 | 22 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β π« π) β π:π« πβΆ(0[,]+β)) |
24 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π β π« π) β π β π« π) |
25 | 24 | elpwdifcl 31764 |
. . . . . . . 8
β’ ((π β§ π β π« π) β (π β π΄) β π« π) |
26 | 23, 25 | ffvelcdmd 7088 |
. . . . . . 7
β’ ((π β§ π β π« π) β (πβ(π β π΄)) β (0[,]+β)) |
27 | 21, 26 | sselid 3981 |
. . . . . 6
β’ ((π β§ π β π« π) β (πβ(π β π΄)) β
β*) |
28 | 24 | elpwincl1 31763 |
. . . . . . . 8
β’ ((π β§ π β π« π) β (π β© π΄) β π« π) |
29 | 23, 28 | ffvelcdmd 7088 |
. . . . . . 7
β’ ((π β§ π β π« π) β (πβ(π β© π΄)) β (0[,]+β)) |
30 | 21, 29 | sselid 3981 |
. . . . . 6
β’ ((π β§ π β π« π) β (πβ(π β© π΄)) β
β*) |
31 | | xaddcom 13219 |
. . . . . 6
β’ (((πβ(π β π΄)) β β* β§ (πβ(π β© π΄)) β β*) β
((πβ(π β π΄)) +π (πβ(π β© π΄))) = ((πβ(π β© π΄)) +π (πβ(π β π΄)))) |
32 | 27, 30, 31 | syl2anc 585 |
. . . . 5
β’ ((π β§ π β π« π) β ((πβ(π β π΄)) +π (πβ(π β© π΄))) = ((πβ(π β© π΄)) +π (πβ(π β π΄)))) |
33 | | difelcarsg.1 |
. . . . . . . 8
β’ (π β π΄ β (toCaraSigaβπ)) |
34 | | carsgval.1 |
. . . . . . . . 9
β’ (π β π β π) |
35 | 34, 22 | elcarsg 33304 |
. . . . . . . 8
β’ (π β (π΄ β (toCaraSigaβπ) β (π΄ β π β§ βπ β π« π((πβ(π β© π΄)) +π (πβ(π β π΄))) = (πβπ)))) |
36 | 33, 35 | mpbid 231 |
. . . . . . 7
β’ (π β (π΄ β π β§ βπ β π« π((πβ(π β© π΄)) +π (πβ(π β π΄))) = (πβπ))) |
37 | 36 | simprd 497 |
. . . . . 6
β’ (π β βπ β π« π((πβ(π β© π΄)) +π (πβ(π β π΄))) = (πβπ)) |
38 | 37 | r19.21bi 3249 |
. . . . 5
β’ ((π β§ π β π« π) β ((πβ(π β© π΄)) +π (πβ(π β π΄))) = (πβπ)) |
39 | 20, 32, 38 | 3eqtrd 2777 |
. . . 4
β’ ((π β§ π β π« π) β ((πβ(π β© (π β π΄))) +π (πβ(π β (π β π΄)))) = (πβπ)) |
40 | 39 | ralrimiva 3147 |
. . 3
β’ (π β βπ β π« π((πβ(π β© (π β π΄))) +π (πβ(π β (π β π΄)))) = (πβπ)) |
41 | 1, 40 | jca 513 |
. 2
β’ (π β ((π β π΄) β π β§ βπ β π« π((πβ(π β© (π β π΄))) +π (πβ(π β (π β π΄)))) = (πβπ))) |
42 | 34, 22 | elcarsg 33304 |
. 2
β’ (π β ((π β π΄) β (toCaraSigaβπ) β ((π β π΄) β π β§ βπ β π« π((πβ(π β© (π β π΄))) +π (πβ(π β (π β π΄)))) = (πβπ)))) |
43 | 41, 42 | mpbird 257 |
1
β’ (π β (π β π΄) β (toCaraSigaβπ)) |