Step | Hyp | Ref
| Expression |
1 | | uncom 4093 |
. . . 4
β’ (π βͺ π) = (π βͺ π) |
2 | 1 | a1i 11 |
. . 3
β’ ((πΎ β Lat β§ π β π΄ β§ π β π΄) β (π βͺ π) = (π βͺ π)) |
3 | | simpl1 1191 |
. . . . . . . 8
β’ (((πΎ β Lat β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π)) β πΎ β Lat) |
4 | | simpl2 1192 |
. . . . . . . . . 10
β’ (((πΎ β Lat β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π)) β π β π΄) |
5 | | simprl 769 |
. . . . . . . . . 10
β’ (((πΎ β Lat β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π)) β π β π) |
6 | 4, 5 | sseldd 3927 |
. . . . . . . . 9
β’ (((πΎ β Lat β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π)) β π β π΄) |
7 | | eqid 2736 |
. . . . . . . . . 10
β’
(BaseβπΎ) =
(BaseβπΎ) |
8 | | padd0.a |
. . . . . . . . . 10
β’ π΄ = (AtomsβπΎ) |
9 | 7, 8 | atbase 37342 |
. . . . . . . . 9
β’ (π β π΄ β π β (BaseβπΎ)) |
10 | 6, 9 | syl 17 |
. . . . . . . 8
β’ (((πΎ β Lat β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π)) β π β (BaseβπΎ)) |
11 | | simpl3 1193 |
. . . . . . . . . 10
β’ (((πΎ β Lat β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π)) β π β π΄) |
12 | | simprr 771 |
. . . . . . . . . 10
β’ (((πΎ β Lat β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π)) β π β π) |
13 | 11, 12 | sseldd 3927 |
. . . . . . . . 9
β’ (((πΎ β Lat β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π)) β π β π΄) |
14 | 7, 8 | atbase 37342 |
. . . . . . . . 9
β’ (π β π΄ β π β (BaseβπΎ)) |
15 | 13, 14 | syl 17 |
. . . . . . . 8
β’ (((πΎ β Lat β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π)) β π β (BaseβπΎ)) |
16 | | eqid 2736 |
. . . . . . . . 9
β’
(joinβπΎ) =
(joinβπΎ) |
17 | 7, 16 | latjcom 18206 |
. . . . . . . 8
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ π β (BaseβπΎ)) β (π(joinβπΎ)π) = (π(joinβπΎ)π)) |
18 | 3, 10, 15, 17 | syl3anc 1371 |
. . . . . . 7
β’ (((πΎ β Lat β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π)) β (π(joinβπΎ)π) = (π(joinβπΎ)π)) |
19 | 18 | breq2d 5093 |
. . . . . 6
β’ (((πΎ β Lat β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π)) β (π(leβπΎ)(π(joinβπΎ)π) β π(leβπΎ)(π(joinβπΎ)π))) |
20 | 19 | 2rexbidva 3208 |
. . . . 5
β’ ((πΎ β Lat β§ π β π΄ β§ π β π΄) β (βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π) β βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π))) |
21 | | rexcom 3270 |
. . . . 5
β’
(βπ β
π βπ β π π(leβπΎ)(π(joinβπΎ)π) β βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π)) |
22 | 20, 21 | bitrdi 288 |
. . . 4
β’ ((πΎ β Lat β§ π β π΄ β§ π β π΄) β (βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π) β βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π))) |
23 | 22 | rabbidv 3421 |
. . 3
β’ ((πΎ β Lat β§ π β π΄ β§ π β π΄) β {π β π΄ β£ βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π)} = {π β π΄ β£ βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π)}) |
24 | 2, 23 | uneq12d 4104 |
. 2
β’ ((πΎ β Lat β§ π β π΄ β§ π β π΄) β ((π βͺ π) βͺ {π β π΄ β£ βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π)}) = ((π βͺ π) βͺ {π β π΄ β£ βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π)})) |
25 | | eqid 2736 |
. . 3
β’
(leβπΎ) =
(leβπΎ) |
26 | | padd0.p |
. . 3
β’ + =
(+πβπΎ) |
27 | 25, 16, 8, 26 | paddval 37851 |
. 2
β’ ((πΎ β Lat β§ π β π΄ β§ π β π΄) β (π + π) = ((π βͺ π) βͺ {π β π΄ β£ βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π)})) |
28 | 25, 16, 8, 26 | paddval 37851 |
. . 3
β’ ((πΎ β Lat β§ π β π΄ β§ π β π΄) β (π + π) = ((π βͺ π) βͺ {π β π΄ β£ βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π)})) |
29 | 28 | 3com23 1126 |
. 2
β’ ((πΎ β Lat β§ π β π΄ β§ π β π΄) β (π + π) = ((π βͺ π) βͺ {π β π΄ β£ βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π)})) |
30 | 24, 27, 29 | 3eqtr4d 2786 |
1
β’ ((πΎ β Lat β§ π β π΄ β§ π β π΄) β (π + π) = (π + π)) |