Step | Hyp | Ref
| Expression |
1 | | trnset.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
2 | | trnset.s |
. . . 4
β’ π = (PSubSpβπΎ) |
3 | | trnset.p |
. . . 4
β’ + =
(+πβπΎ) |
4 | | trnset.o |
. . . 4
β’ β₯ =
(β₯πβπΎ) |
5 | | trnset.w |
. . . 4
β’ π = (WAtomsβπΎ) |
6 | | trnset.m |
. . . 4
β’ π = (PAutβπΎ) |
7 | | trnset.l |
. . . 4
β’ πΏ = (DilβπΎ) |
8 | | trnset.t |
. . . 4
β’ π = (TrnβπΎ) |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | trnsetN 38622 |
. . 3
β’ ((πΎ β π΅ β§ π· β π΄) β (πβπ·) = {π β (πΏβπ·) β£ βπ β (πβπ·)βπ β (πβπ·)((π + (πβπ)) β© ( β₯ β{π·})) = ((π + (πβπ)) β© ( β₯ β{π·}))}) |
10 | 9 | eleq2d 2824 |
. 2
β’ ((πΎ β π΅ β§ π· β π΄) β (πΉ β (πβπ·) β πΉ β {π β (πΏβπ·) β£ βπ β (πβπ·)βπ β (πβπ·)((π + (πβπ)) β© ( β₯ β{π·})) = ((π + (πβπ)) β© ( β₯ β{π·}))})) |
11 | | fveq1 6842 |
. . . . . . 7
β’ (π = πΉ β (πβπ) = (πΉβπ)) |
12 | 11 | oveq2d 7374 |
. . . . . 6
β’ (π = πΉ β (π + (πβπ)) = (π + (πΉβπ))) |
13 | 12 | ineq1d 4172 |
. . . . 5
β’ (π = πΉ β ((π + (πβπ)) β© ( β₯ β{π·})) = ((π + (πΉβπ)) β© ( β₯ β{π·}))) |
14 | | fveq1 6842 |
. . . . . . 7
β’ (π = πΉ β (πβπ) = (πΉβπ)) |
15 | 14 | oveq2d 7374 |
. . . . . 6
β’ (π = πΉ β (π + (πβπ)) = (π + (πΉβπ))) |
16 | 15 | ineq1d 4172 |
. . . . 5
β’ (π = πΉ β ((π + (πβπ)) β© ( β₯ β{π·})) = ((π + (πΉβπ)) β© ( β₯ β{π·}))) |
17 | 13, 16 | eqeq12d 2753 |
. . . 4
β’ (π = πΉ β (((π + (πβπ)) β© ( β₯ β{π·})) = ((π + (πβπ)) β© ( β₯ β{π·})) β ((π + (πΉβπ)) β© ( β₯ β{π·})) = ((π + (πΉβπ)) β© ( β₯ β{π·})))) |
18 | 17 | 2ralbidv 3213 |
. . 3
β’ (π = πΉ β (βπ β (πβπ·)βπ β (πβπ·)((π + (πβπ)) β© ( β₯ β{π·})) = ((π + (πβπ)) β© ( β₯ β{π·})) β βπ β (πβπ·)βπ β (πβπ·)((π + (πΉβπ)) β© ( β₯ β{π·})) = ((π + (πΉβπ)) β© ( β₯ β{π·})))) |
19 | 18 | elrab 3646 |
. 2
β’ (πΉ β {π β (πΏβπ·) β£ βπ β (πβπ·)βπ β (πβπ·)((π + (πβπ)) β© ( β₯ β{π·})) = ((π + (πβπ)) β© ( β₯ β{π·}))} β (πΉ β (πΏβπ·) β§ βπ β (πβπ·)βπ β (πβπ·)((π + (πΉβπ)) β© ( β₯ β{π·})) = ((π + (πΉβπ)) β© ( β₯ β{π·})))) |
20 | 10, 19 | bitrdi 287 |
1
β’ ((πΎ β π΅ β§ π· β π΄) β (πΉ β (πβπ·) β (πΉ β (πΏβπ·) β§ βπ β (πβπ·)βπ β (πβπ·)((π + (πΉβπ)) β© ( β₯ β{π·})) = ((π + (πΉβπ)) β© ( β₯ β{π·}))))) |