Step | Hyp | Ref
| Expression |
1 | | biid 261 |
. 2
β’ (πΎ β π΅ β πΎ β π΅) |
2 | | paddfval.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
3 | 2 | fvexi 6861 |
. . 3
β’ π΄ β V |
4 | 3 | elpw2 5307 |
. 2
β’ (π β π« π΄ β π β π΄) |
5 | 3 | elpw2 5307 |
. 2
β’ (π β π« π΄ β π β π΄) |
6 | | paddfval.l |
. . . . . 6
β’ β€ =
(leβπΎ) |
7 | | paddfval.j |
. . . . . 6
β’ β¨ =
(joinβπΎ) |
8 | | paddfval.p |
. . . . . 6
β’ + =
(+πβπΎ) |
9 | 6, 7, 2, 8 | paddfval 38289 |
. . . . 5
β’ (πΎ β π΅ β + = (π β π« π΄, π β π« π΄ β¦ ((π βͺ π) βͺ {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)}))) |
10 | 9 | oveqd 7379 |
. . . 4
β’ (πΎ β π΅ β (π + π) = (π(π β π« π΄, π β π« π΄ β¦ ((π βͺ π) βͺ {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)}))π)) |
11 | 10 | 3ad2ant1 1134 |
. . 3
β’ ((πΎ β π΅ β§ π β π« π΄ β§ π β π« π΄) β (π + π) = (π(π β π« π΄, π β π« π΄ β¦ ((π βͺ π) βͺ {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)}))π)) |
12 | | simpl 484 |
. . . . . 6
β’ ((π β π« π΄ β§ π β π« π΄) β π β π« π΄) |
13 | | simpr 486 |
. . . . . 6
β’ ((π β π« π΄ β§ π β π« π΄) β π β π« π΄) |
14 | | unexg 7688 |
. . . . . . 7
β’ ((π β π« π΄ β§ π β π« π΄) β (π βͺ π) β V) |
15 | 3 | rabex 5294 |
. . . . . . 7
β’ {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)} β V |
16 | | unexg 7688 |
. . . . . . 7
β’ (((π βͺ π) β V β§ {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)} β V) β ((π βͺ π) βͺ {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)}) β V) |
17 | 14, 15, 16 | sylancl 587 |
. . . . . 6
β’ ((π β π« π΄ β§ π β π« π΄) β ((π βͺ π) βͺ {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)}) β V) |
18 | 12, 13, 17 | 3jca 1129 |
. . . . 5
β’ ((π β π« π΄ β§ π β π« π΄) β (π β π« π΄ β§ π β π« π΄ β§ ((π βͺ π) βͺ {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)}) β V)) |
19 | 18 | 3adant1 1131 |
. . . 4
β’ ((πΎ β π΅ β§ π β π« π΄ β§ π β π« π΄) β (π β π« π΄ β§ π β π« π΄ β§ ((π βͺ π) βͺ {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)}) β V)) |
20 | | uneq1 4121 |
. . . . . 6
β’ (π = π β (π βͺ π) = (π βͺ π)) |
21 | | rexeq 3313 |
. . . . . . 7
β’ (π = π β (βπ β π βπ β π π β€ (π β¨ π) β βπ β π βπ β π π β€ (π β¨ π))) |
22 | 21 | rabbidv 3418 |
. . . . . 6
β’ (π = π β {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)} = {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)}) |
23 | 20, 22 | uneq12d 4129 |
. . . . 5
β’ (π = π β ((π βͺ π) βͺ {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)}) = ((π βͺ π) βͺ {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)})) |
24 | | uneq2 4122 |
. . . . . 6
β’ (π = π β (π βͺ π) = (π βͺ π)) |
25 | | rexeq 3313 |
. . . . . . . 8
β’ (π = π β (βπ β π π β€ (π β¨ π) β βπ β π π β€ (π β¨ π))) |
26 | 25 | rexbidv 3176 |
. . . . . . 7
β’ (π = π β (βπ β π βπ β π π β€ (π β¨ π) β βπ β π βπ β π π β€ (π β¨ π))) |
27 | 26 | rabbidv 3418 |
. . . . . 6
β’ (π = π β {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)} = {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)}) |
28 | 24, 27 | uneq12d 4129 |
. . . . 5
β’ (π = π β ((π βͺ π) βͺ {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)}) = ((π βͺ π) βͺ {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)})) |
29 | | eqid 2737 |
. . . . 5
β’ (π β π« π΄, π β π« π΄ β¦ ((π βͺ π) βͺ {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)})) = (π β π« π΄, π β π« π΄ β¦ ((π βͺ π) βͺ {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)})) |
30 | 23, 28, 29 | ovmpog 7519 |
. . . 4
β’ ((π β π« π΄ β§ π β π« π΄ β§ ((π βͺ π) βͺ {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)}) β V) β (π(π β π« π΄, π β π« π΄ β¦ ((π βͺ π) βͺ {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)}))π) = ((π βͺ π) βͺ {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)})) |
31 | 19, 30 | syl 17 |
. . 3
β’ ((πΎ β π΅ β§ π β π« π΄ β§ π β π« π΄) β (π(π β π« π΄, π β π« π΄ β¦ ((π βͺ π) βͺ {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)}))π) = ((π βͺ π) βͺ {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)})) |
32 | 11, 31 | eqtrd 2777 |
. 2
β’ ((πΎ β π΅ β§ π β π« π΄ β§ π β π« π΄) β (π + π) = ((π βͺ π) βͺ {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)})) |
33 | 1, 4, 5, 32 | syl3anbr 1163 |
1
β’ ((πΎ β π΅ β§ π β π΄ β§ π β π΄) β (π + π) = ((π βͺ π) βͺ {π β π΄ β£ βπ β π βπ β π π β€ (π β¨ π)})) |