Step | Hyp | Ref
| Expression |
1 | | difssd 4132 |
. . 3
β’ (π β (π β π΄) β π) |
2 | | indif2 4270 |
. . . . . . . 8
β’ (π β© (π β π΄)) = ((π β© π) β π΄) |
3 | | elpwi 4609 |
. . . . . . . . . . 11
β’ (π β π« π β π β π) |
4 | 3 | adantl 482 |
. . . . . . . . . 10
β’ ((π β§ π β π« π) β π β π) |
5 | | df-ss 3965 |
. . . . . . . . . 10
β’ (π β π β (π β© π) = π) |
6 | 4, 5 | sylib 217 |
. . . . . . . . 9
β’ ((π β§ π β π« π) β (π β© π) = π) |
7 | 6 | difeq1d 4121 |
. . . . . . . 8
β’ ((π β§ π β π« π) β ((π β© π) β π΄) = (π β π΄)) |
8 | 2, 7 | eqtrid 2784 |
. . . . . . 7
β’ ((π β§ π β π« π) β (π β© (π β π΄)) = (π β π΄)) |
9 | 8 | fveq2d 6895 |
. . . . . 6
β’ ((π β§ π β π« π) β (πβ(π β© (π β π΄))) = (πβ(π β π΄))) |
10 | | difdif2 4286 |
. . . . . . . 8
β’ (π β (π β π΄)) = ((π β π) βͺ (π β© π΄)) |
11 | | ssdif0 4363 |
. . . . . . . . . . 11
β’ (π β π β (π β π) = β
) |
12 | 4, 11 | sylib 217 |
. . . . . . . . . 10
β’ ((π β§ π β π« π) β (π β π) = β
) |
13 | 12 | uneq1d 4162 |
. . . . . . . . 9
β’ ((π β§ π β π« π) β ((π β π) βͺ (π β© π΄)) = (β
βͺ (π β© π΄))) |
14 | | uncom 4153 |
. . . . . . . . . 10
β’ ((π β© π΄) βͺ β
) = (β
βͺ (π β© π΄)) |
15 | | un0 4390 |
. . . . . . . . . 10
β’ ((π β© π΄) βͺ β
) = (π β© π΄) |
16 | 14, 15 | eqtr3i 2762 |
. . . . . . . . 9
β’ (β
βͺ (π β© π΄)) = (π β© π΄) |
17 | 13, 16 | eqtrdi 2788 |
. . . . . . . 8
β’ ((π β§ π β π« π) β ((π β π) βͺ (π β© π΄)) = (π β© π΄)) |
18 | 10, 17 | eqtrid 2784 |
. . . . . . 7
β’ ((π β§ π β π« π) β (π β (π β π΄)) = (π β© π΄)) |
19 | 18 | fveq2d 6895 |
. . . . . 6
β’ ((π β§ π β π« π) β (πβ(π β (π β π΄))) = (πβ(π β© π΄))) |
20 | 9, 19 | oveq12d 7429 |
. . . . 5
β’ ((π β§ π β π« π) β ((πβ(π β© (π β π΄))) +π (πβ(π β (π β π΄)))) = ((πβ(π β π΄)) +π (πβ(π β© π΄)))) |
21 | | iccssxr 13409 |
. . . . . . 7
β’
(0[,]+β) β β* |
22 | | carsgval.2 |
. . . . . . . . 9
β’ (π β π:π« πβΆ(0[,]+β)) |
23 | 22 | adantr 481 |
. . . . . . . 8
β’ ((π β§ π β π« π) β π:π« πβΆ(0[,]+β)) |
24 | | simpr 485 |
. . . . . . . . 9
β’ ((π β§ π β π« π) β π β π« π) |
25 | 24 | elpwdifcl 31802 |
. . . . . . . 8
β’ ((π β§ π β π« π) β (π β π΄) β π« π) |
26 | 23, 25 | ffvelcdmd 7087 |
. . . . . . 7
β’ ((π β§ π β π« π) β (πβ(π β π΄)) β (0[,]+β)) |
27 | 21, 26 | sselid 3980 |
. . . . . 6
β’ ((π β§ π β π« π) β (πβ(π β π΄)) β
β*) |
28 | 24 | elpwincl1 31801 |
. . . . . . . 8
β’ ((π β§ π β π« π) β (π β© π΄) β π« π) |
29 | 23, 28 | ffvelcdmd 7087 |
. . . . . . 7
β’ ((π β§ π β π« π) β (πβ(π β© π΄)) β (0[,]+β)) |
30 | 21, 29 | sselid 3980 |
. . . . . 6
β’ ((π β§ π β π« π) β (πβ(π β© π΄)) β
β*) |
31 | | xaddcom 13221 |
. . . . . 6
β’ (((πβ(π β π΄)) β β* β§ (πβ(π β© π΄)) β β*) β
((πβ(π β π΄)) +π (πβ(π β© π΄))) = ((πβ(π β© π΄)) +π (πβ(π β π΄)))) |
32 | 27, 30, 31 | syl2anc 584 |
. . . . 5
β’ ((π β§ π β π« π) β ((πβ(π β π΄)) +π (πβ(π β© π΄))) = ((πβ(π β© π΄)) +π (πβ(π β π΄)))) |
33 | | difelcarsg.1 |
. . . . . . . 8
β’ (π β π΄ β (toCaraSigaβπ)) |
34 | | carsgval.1 |
. . . . . . . . 9
β’ (π β π β π) |
35 | 34, 22 | elcarsg 33373 |
. . . . . . . 8
β’ (π β (π΄ β (toCaraSigaβπ) β (π΄ β π β§ βπ β π« π((πβ(π β© π΄)) +π (πβ(π β π΄))) = (πβπ)))) |
36 | 33, 35 | mpbid 231 |
. . . . . . 7
β’ (π β (π΄ β π β§ βπ β π« π((πβ(π β© π΄)) +π (πβ(π β π΄))) = (πβπ))) |
37 | 36 | simprd 496 |
. . . . . 6
β’ (π β βπ β π« π((πβ(π β© π΄)) +π (πβ(π β π΄))) = (πβπ)) |
38 | 37 | r19.21bi 3248 |
. . . . 5
β’ ((π β§ π β π« π) β ((πβ(π β© π΄)) +π (πβ(π β π΄))) = (πβπ)) |
39 | 20, 32, 38 | 3eqtrd 2776 |
. . . 4
β’ ((π β§ π β π« π) β ((πβ(π β© (π β π΄))) +π (πβ(π β (π β π΄)))) = (πβπ)) |
40 | 39 | ralrimiva 3146 |
. . 3
β’ (π β βπ β π« π((πβ(π β© (π β π΄))) +π (πβ(π β (π β π΄)))) = (πβπ)) |
41 | 1, 40 | jca 512 |
. 2
β’ (π β ((π β π΄) β π β§ βπ β π« π((πβ(π β© (π β π΄))) +π (πβ(π β (π β π΄)))) = (πβπ))) |
42 | 34, 22 | elcarsg 33373 |
. 2
β’ (π β ((π β π΄) β (toCaraSigaβπ) β ((π β π΄) β π β§ βπ β π« π((πβ(π β© (π β π΄))) +π (πβ(π β (π β π΄)))) = (πβπ)))) |
43 | 41, 42 | mpbird 256 |
1
β’ (π β (π β π΄) β (toCaraSigaβπ)) |