Step | Hyp | Ref
| Expression |
1 | | phnv 29798 |
. . . . 5
β’ (π β CPreHilOLD
β π β
NrmCVec) |
2 | | ajval.1 |
. . . . . 6
β’ π = (BaseSetβπ) |
3 | | ajval.2 |
. . . . . 6
β’ π = (BaseSetβπ) |
4 | | ajval.3 |
. . . . . 6
β’ π =
(Β·πOLDβπ) |
5 | | ajval.4 |
. . . . . 6
β’ π =
(Β·πOLDβπ) |
6 | | ajval.5 |
. . . . . 6
β’ π΄ = (πadjπ) |
7 | 2, 3, 4, 5, 6 | ajfval 29793 |
. . . . 5
β’ ((π β NrmCVec β§ π β NrmCVec) β π΄ = {β¨π‘, π β© β£ (π‘:πβΆπ β§ π :πβΆπ β§ βπ₯ β π βπ¦ β π ((π‘βπ₯)ππ¦) = (π₯π(π βπ¦)))}) |
8 | 1, 7 | sylan 581 |
. . . 4
β’ ((π β CPreHilOLD
β§ π β NrmCVec)
β π΄ = {β¨π‘, π β© β£ (π‘:πβΆπ β§ π :πβΆπ β§ βπ₯ β π βπ¦ β π ((π‘βπ₯)ππ¦) = (π₯π(π βπ¦)))}) |
9 | 8 | fveq1d 6849 |
. . 3
β’ ((π β CPreHilOLD
β§ π β NrmCVec)
β (π΄βπ) = ({β¨π‘, π β© β£ (π‘:πβΆπ β§ π :πβΆπ β§ βπ₯ β π βπ¦ β π ((π‘βπ₯)ππ¦) = (π₯π(π βπ¦)))}βπ)) |
10 | 9 | 3adant3 1133 |
. 2
β’ ((π β CPreHilOLD
β§ π β NrmCVec
β§ π:πβΆπ) β (π΄βπ) = ({β¨π‘, π β© β£ (π‘:πβΆπ β§ π :πβΆπ β§ βπ₯ β π βπ¦ β π ((π‘βπ₯)ππ¦) = (π₯π(π βπ¦)))}βπ)) |
11 | 2 | fvexi 6861 |
. . . . . 6
β’ π β V |
12 | | fex 7181 |
. . . . . 6
β’ ((π:πβΆπ β§ π β V) β π β V) |
13 | 11, 12 | mpan2 690 |
. . . . 5
β’ (π:πβΆπ β π β V) |
14 | | eqid 2737 |
. . . . . 6
β’
{β¨π‘, π β© β£ (π‘:πβΆπ β§ π :πβΆπ β§ βπ₯ β π βπ¦ β π ((π‘βπ₯)ππ¦) = (π₯π(π βπ¦)))} = {β¨π‘, π β© β£ (π‘:πβΆπ β§ π :πβΆπ β§ βπ₯ β π βπ¦ β π ((π‘βπ₯)ππ¦) = (π₯π(π βπ¦)))} |
15 | | feq1 6654 |
. . . . . . 7
β’ (π‘ = π β (π‘:πβΆπ β π:πβΆπ)) |
16 | | fveq1 6846 |
. . . . . . . . . 10
β’ (π‘ = π β (π‘βπ₯) = (πβπ₯)) |
17 | 16 | oveq1d 7377 |
. . . . . . . . 9
β’ (π‘ = π β ((π‘βπ₯)ππ¦) = ((πβπ₯)ππ¦)) |
18 | 17 | eqeq1d 2739 |
. . . . . . . 8
β’ (π‘ = π β (((π‘βπ₯)ππ¦) = (π₯π(π βπ¦)) β ((πβπ₯)ππ¦) = (π₯π(π βπ¦)))) |
19 | 18 | 2ralbidv 3213 |
. . . . . . 7
β’ (π‘ = π β (βπ₯ β π βπ¦ β π ((π‘βπ₯)ππ¦) = (π₯π(π βπ¦)) β βπ₯ β π βπ¦ β π ((πβπ₯)ππ¦) = (π₯π(π βπ¦)))) |
20 | 15, 19 | 3anbi13d 1439 |
. . . . . 6
β’ (π‘ = π β ((π‘:πβΆπ β§ π :πβΆπ β§ βπ₯ β π βπ¦ β π ((π‘βπ₯)ππ¦) = (π₯π(π βπ¦))) β (π:πβΆπ β§ π :πβΆπ β§ βπ₯ β π βπ¦ β π ((πβπ₯)ππ¦) = (π₯π(π βπ¦))))) |
21 | 14, 20 | fvopab5 6985 |
. . . . 5
β’ (π β V β ({β¨π‘, π β© β£ (π‘:πβΆπ β§ π :πβΆπ β§ βπ₯ β π βπ¦ β π ((π‘βπ₯)ππ¦) = (π₯π(π βπ¦)))}βπ) = (β©π (π:πβΆπ β§ π :πβΆπ β§ βπ₯ β π βπ¦ β π ((πβπ₯)ππ¦) = (π₯π(π βπ¦))))) |
22 | 13, 21 | syl 17 |
. . . 4
β’ (π:πβΆπ β ({β¨π‘, π β© β£ (π‘:πβΆπ β§ π :πβΆπ β§ βπ₯ β π βπ¦ β π ((π‘βπ₯)ππ¦) = (π₯π(π βπ¦)))}βπ) = (β©π (π:πβΆπ β§ π :πβΆπ β§ βπ₯ β π βπ¦ β π ((πβπ₯)ππ¦) = (π₯π(π βπ¦))))) |
23 | | 3anass 1096 |
. . . . . 6
β’ ((π:πβΆπ β§ π :πβΆπ β§ βπ₯ β π βπ¦ β π ((πβπ₯)ππ¦) = (π₯π(π βπ¦))) β (π:πβΆπ β§ (π :πβΆπ β§ βπ₯ β π βπ¦ β π ((πβπ₯)ππ¦) = (π₯π(π βπ¦))))) |
24 | 23 | baib 537 |
. . . . 5
β’ (π:πβΆπ β ((π:πβΆπ β§ π :πβΆπ β§ βπ₯ β π βπ¦ β π ((πβπ₯)ππ¦) = (π₯π(π βπ¦))) β (π :πβΆπ β§ βπ₯ β π βπ¦ β π ((πβπ₯)ππ¦) = (π₯π(π βπ¦))))) |
25 | 24 | iotabidv 6485 |
. . . 4
β’ (π:πβΆπ β (β©π (π:πβΆπ β§ π :πβΆπ β§ βπ₯ β π βπ¦ β π ((πβπ₯)ππ¦) = (π₯π(π βπ¦)))) = (β©π (π :πβΆπ β§ βπ₯ β π βπ¦ β π ((πβπ₯)ππ¦) = (π₯π(π βπ¦))))) |
26 | 22, 25 | eqtrd 2777 |
. . 3
β’ (π:πβΆπ β ({β¨π‘, π β© β£ (π‘:πβΆπ β§ π :πβΆπ β§ βπ₯ β π βπ¦ β π ((π‘βπ₯)ππ¦) = (π₯π(π βπ¦)))}βπ) = (β©π (π :πβΆπ β§ βπ₯ β π βπ¦ β π ((πβπ₯)ππ¦) = (π₯π(π βπ¦))))) |
27 | 26 | 3ad2ant3 1136 |
. 2
β’ ((π β CPreHilOLD
β§ π β NrmCVec
β§ π:πβΆπ) β ({β¨π‘, π β© β£ (π‘:πβΆπ β§ π :πβΆπ β§ βπ₯ β π βπ¦ β π ((π‘βπ₯)ππ¦) = (π₯π(π βπ¦)))}βπ) = (β©π (π :πβΆπ β§ βπ₯ β π βπ¦ β π ((πβπ₯)ππ¦) = (π₯π(π βπ¦))))) |
28 | 10, 27 | eqtrd 2777 |
1
β’ ((π β CPreHilOLD
β§ π β NrmCVec
β§ π:πβΆπ) β (π΄βπ) = (β©π (π :πβΆπ β§ βπ₯ β π βπ¦ β π ((πβπ₯)ππ¦) = (π₯π(π βπ¦))))) |