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 | trnfsetN 38621 |
. . 3
β’ (πΎ β π΅ β π = (π β π΄ β¦ {π β (πΏβπ) β£ βπ β (πβπ)βπ β (πβπ)((π + (πβπ)) β© ( β₯ β{π})) = ((π + (πβπ)) β© ( β₯ β{π}))})) |
10 | 9 | fveq1d 6845 |
. 2
β’ (πΎ β π΅ β (πβπ·) = ((π β π΄ β¦ {π β (πΏβπ) β£ βπ β (πβπ)βπ β (πβπ)((π + (πβπ)) β© ( β₯ β{π})) = ((π + (πβπ)) β© ( β₯ β{π}))})βπ·)) |
11 | | fveq2 6843 |
. . . 4
β’ (π = π· β (πΏβπ) = (πΏβπ·)) |
12 | | fveq2 6843 |
. . . . 5
β’ (π = π· β (πβπ) = (πβπ·)) |
13 | | sneq 4597 |
. . . . . . . . 9
β’ (π = π· β {π} = {π·}) |
14 | 13 | fveq2d 6847 |
. . . . . . . 8
β’ (π = π· β ( β₯ β{π}) = ( β₯ β{π·})) |
15 | 14 | ineq2d 4173 |
. . . . . . 7
β’ (π = π· β ((π + (πβπ)) β© ( β₯ β{π})) = ((π + (πβπ)) β© ( β₯ β{π·}))) |
16 | 14 | ineq2d 4173 |
. . . . . . 7
β’ (π = π· β ((π + (πβπ)) β© ( β₯ β{π})) = ((π + (πβπ)) β© ( β₯ β{π·}))) |
17 | 15, 16 | eqeq12d 2753 |
. . . . . 6
β’ (π = π· β (((π + (πβπ)) β© ( β₯ β{π})) = ((π + (πβπ)) β© ( β₯ β{π})) β ((π + (πβπ)) β© ( β₯ β{π·})) = ((π + (πβπ)) β© ( β₯ β{π·})))) |
18 | 12, 17 | raleqbidv 3320 |
. . . . 5
β’ (π = π· β (βπ β (πβπ)((π + (πβπ)) β© ( β₯ β{π})) = ((π + (πβπ)) β© ( β₯ β{π})) β βπ β (πβπ·)((π + (πβπ)) β© ( β₯ β{π·})) = ((π + (πβπ)) β© ( β₯ β{π·})))) |
19 | 12, 18 | raleqbidv 3320 |
. . . 4
β’ (π = π· β (βπ β (πβπ)βπ β (πβπ)((π + (πβπ)) β© ( β₯ β{π})) = ((π + (πβπ)) β© ( β₯ β{π})) β βπ β (πβπ·)βπ β (πβπ·)((π + (πβπ)) β© ( β₯ β{π·})) = ((π + (πβπ)) β© ( β₯ β{π·})))) |
20 | 11, 19 | rabeqbidv 3425 |
. . 3
β’ (π = π· β {π β (πΏβπ) β£ βπ β (πβπ)βπ β (πβπ)((π + (πβπ)) β© ( β₯ β{π})) = ((π + (πβπ)) β© ( β₯ β{π}))} = {π β (πΏβπ·) β£ βπ β (πβπ·)βπ β (πβπ·)((π + (πβπ)) β© ( β₯ β{π·})) = ((π + (πβπ)) β© ( β₯ β{π·}))}) |
21 | | eqid 2737 |
. . 3
β’ (π β π΄ β¦ {π β (πΏβπ) β£ βπ β (πβπ)βπ β (πβπ)((π + (πβπ)) β© ( β₯ β{π})) = ((π + (πβπ)) β© ( β₯ β{π}))}) = (π β π΄ β¦ {π β (πΏβπ) β£ βπ β (πβπ)βπ β (πβπ)((π + (πβπ)) β© ( β₯ β{π})) = ((π + (πβπ)) β© ( β₯ β{π}))}) |
22 | | fvex 6856 |
. . . 4
β’ (πΏβπ·) β V |
23 | 22 | rabex 5290 |
. . 3
β’ {π β (πΏβπ·) β£ βπ β (πβπ·)βπ β (πβπ·)((π + (πβπ)) β© ( β₯ β{π·})) = ((π + (πβπ)) β© ( β₯ β{π·}))} β V |
24 | 20, 21, 23 | fvmpt 6949 |
. 2
β’ (π· β π΄ β ((π β π΄ β¦ {π β (πΏβπ) β£ βπ β (πβπ)βπ β (πβπ)((π + (πβπ)) β© ( β₯ β{π})) = ((π + (πβπ)) β© ( β₯ β{π}))})βπ·) = {π β (πΏβπ·) β£ βπ β (πβπ·)βπ β (πβπ·)((π + (πβπ)) β© ( β₯ β{π·})) = ((π + (πβπ)) β© ( β₯ β{π·}))}) |
25 | 10, 24 | sylan9eq 2797 |
1
β’ ((πΎ β π΅ β§ π· β π΄) β (πβπ·) = {π β (πΏβπ·) β£ βπ β (πβπ·)βπ β (πβπ·)((π + (πβπ)) β© ( β₯ β{π·})) = ((π + (πβπ)) β© ( β₯ β{π·}))}) |