Step | Hyp | Ref
| Expression |
1 | | elex 3464 |
. 2
β’ (πΎ β πΆ β πΎ β V) |
2 | | trnset.t |
. . 3
β’ π = (TrnβπΎ) |
3 | | fveq2 6843 |
. . . . . 6
β’ (π = πΎ β (Atomsβπ) = (AtomsβπΎ)) |
4 | | trnset.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
5 | 3, 4 | eqtr4di 2795 |
. . . . 5
β’ (π = πΎ β (Atomsβπ) = π΄) |
6 | | fveq2 6843 |
. . . . . . . 8
β’ (π = πΎ β (Dilβπ) = (DilβπΎ)) |
7 | | trnset.l |
. . . . . . . 8
β’ πΏ = (DilβπΎ) |
8 | 6, 7 | eqtr4di 2795 |
. . . . . . 7
β’ (π = πΎ β (Dilβπ) = πΏ) |
9 | 8 | fveq1d 6845 |
. . . . . 6
β’ (π = πΎ β ((Dilβπ)βπ) = (πΏβπ)) |
10 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = πΎ β (WAtomsβπ) = (WAtomsβπΎ)) |
11 | | trnset.w |
. . . . . . . . 9
β’ π = (WAtomsβπΎ) |
12 | 10, 11 | eqtr4di 2795 |
. . . . . . . 8
β’ (π = πΎ β (WAtomsβπ) = π) |
13 | 12 | fveq1d 6845 |
. . . . . . 7
β’ (π = πΎ β ((WAtomsβπ)βπ) = (πβπ)) |
14 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π = πΎ β (+πβπ) =
(+πβπΎ)) |
15 | | trnset.p |
. . . . . . . . . . . 12
β’ + =
(+πβπΎ) |
16 | 14, 15 | eqtr4di 2795 |
. . . . . . . . . . 11
β’ (π = πΎ β (+πβπ) = + ) |
17 | 16 | oveqd 7375 |
. . . . . . . . . 10
β’ (π = πΎ β (π(+πβπ)(πβπ)) = (π + (πβπ))) |
18 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π = πΎ β
(β₯πβπ) = (β₯πβπΎ)) |
19 | | trnset.o |
. . . . . . . . . . . 12
β’ β₯ =
(β₯πβπΎ) |
20 | 18, 19 | eqtr4di 2795 |
. . . . . . . . . . 11
β’ (π = πΎ β
(β₯πβπ) = β₯ ) |
21 | 20 | fveq1d 6845 |
. . . . . . . . . 10
β’ (π = πΎ β
((β₯πβπ)β{π}) = ( β₯ β{π})) |
22 | 17, 21 | ineq12d 4174 |
. . . . . . . . 9
β’ (π = πΎ β ((π(+πβπ)(πβπ)) β©
((β₯πβπ)β{π})) = ((π + (πβπ)) β© ( β₯ β{π}))) |
23 | 16 | oveqd 7375 |
. . . . . . . . . 10
β’ (π = πΎ β (π(+πβπ)(πβπ)) = (π + (πβπ))) |
24 | 23, 21 | ineq12d 4174 |
. . . . . . . . 9
β’ (π = πΎ β ((π(+πβπ)(πβπ)) β©
((β₯πβπ)β{π})) = ((π + (πβπ)) β© ( β₯ β{π}))) |
25 | 22, 24 | eqeq12d 2753 |
. . . . . . . 8
β’ (π = πΎ β (((π(+πβπ)(πβπ)) β©
((β₯πβπ)β{π})) = ((π(+πβπ)(πβπ)) β©
((β₯πβπ)β{π})) β ((π + (πβπ)) β© ( β₯ β{π})) = ((π + (πβπ)) β© ( β₯ β{π})))) |
26 | 13, 25 | raleqbidv 3320 |
. . . . . . 7
β’ (π = πΎ β (βπ β ((WAtomsβπ)βπ)((π(+πβπ)(πβπ)) β©
((β₯πβπ)β{π})) = ((π(+πβπ)(πβπ)) β©
((β₯πβπ)β{π})) β βπ β (πβπ)((π + (πβπ)) β© ( β₯ β{π})) = ((π + (πβπ)) β© ( β₯ β{π})))) |
27 | 13, 26 | raleqbidv 3320 |
. . . . . 6
β’ (π = πΎ β (βπ β ((WAtomsβπ)βπ)βπ β ((WAtomsβπ)βπ)((π(+πβπ)(πβπ)) β©
((β₯πβπ)β{π})) = ((π(+πβπ)(πβπ)) β©
((β₯πβπ)β{π})) β βπ β (πβπ)βπ β (πβπ)((π + (πβπ)) β© ( β₯ β{π})) = ((π + (πβπ)) β© ( β₯ β{π})))) |
28 | 9, 27 | rabeqbidv 3425 |
. . . . 5
β’ (π = πΎ β {π β ((Dilβπ)βπ) β£ βπ β ((WAtomsβπ)βπ)βπ β ((WAtomsβπ)βπ)((π(+πβπ)(πβπ)) β©
((β₯πβπ)β{π})) = ((π(+πβπ)(πβπ)) β©
((β₯πβπ)β{π}))} = {π β (πΏβπ) β£ βπ β (πβπ)βπ β (πβπ)((π + (πβπ)) β© ( β₯ β{π})) = ((π + (πβπ)) β© ( β₯ β{π}))}) |
29 | 5, 28 | mpteq12dv 5197 |
. . . 4
β’ (π = πΎ β (π β (Atomsβπ) β¦ {π β ((Dilβπ)βπ) β£ βπ β ((WAtomsβπ)βπ)βπ β ((WAtomsβπ)βπ)((π(+πβπ)(πβπ)) β©
((β₯πβπ)β{π})) = ((π(+πβπ)(πβπ)) β©
((β₯πβπ)β{π}))}) = (π β π΄ β¦ {π β (πΏβπ) β£ βπ β (πβπ)βπ β (πβπ)((π + (πβπ)) β© ( β₯ β{π})) = ((π + (πβπ)) β© ( β₯ β{π}))})) |
30 | | df-trnN 38573 |
. . . 4
β’ Trn =
(π β V β¦ (π β (Atomsβπ) β¦ {π β ((Dilβπ)βπ) β£ βπ β ((WAtomsβπ)βπ)βπ β ((WAtomsβπ)βπ)((π(+πβπ)(πβπ)) β©
((β₯πβπ)β{π})) = ((π(+πβπ)(πβπ)) β©
((β₯πβπ)β{π}))})) |
31 | 29, 30, 4 | mptfvmpt 7179 |
. . 3
β’ (πΎ β V β
(TrnβπΎ) = (π β π΄ β¦ {π β (πΏβπ) β£ βπ β (πβπ)βπ β (πβπ)((π + (πβπ)) β© ( β₯ β{π})) = ((π + (πβπ)) β© ( β₯ β{π}))})) |
32 | 2, 31 | eqtrid 2789 |
. 2
β’ (πΎ β V β π = (π β π΄ β¦ {π β (πΏβπ) β£ βπ β (πβπ)βπ β (πβπ)((π + (πβπ)) β© ( β₯ β{π})) = ((π + (πβπ)) β© ( β₯ β{π}))})) |
33 | 1, 32 | syl 17 |
1
β’ (πΎ β πΆ β π = (π β π΄ β¦ {π β (πΏβπ) β£ βπ β (πβπ)βπ β (πβπ)((π + (πβπ)) β© ( β₯ β{π})) = ((π + (πβπ)) β© ( β₯ β{π}))})) |