Step | Hyp | Ref
| Expression |
1 | | ajfval.5 |
. 2
β’ π΄ = (πadjπ) |
2 | | fveq2 6846 |
. . . . . . 7
β’ (π’ = π β (BaseSetβπ’) = (BaseSetβπ)) |
3 | | ajfval.1 |
. . . . . . 7
β’ π = (BaseSetβπ) |
4 | 2, 3 | eqtr4di 2791 |
. . . . . 6
β’ (π’ = π β (BaseSetβπ’) = π) |
5 | 4 | feq2d 6658 |
. . . . 5
β’ (π’ = π β (π‘:(BaseSetβπ’)βΆ(BaseSetβπ€) β π‘:πβΆ(BaseSetβπ€))) |
6 | 4 | feq3d 6659 |
. . . . 5
β’ (π’ = π β (π :(BaseSetβπ€)βΆ(BaseSetβπ’) β π :(BaseSetβπ€)βΆπ)) |
7 | | fveq2 6846 |
. . . . . . . . . 10
β’ (π’ = π β
(Β·πOLDβπ’) =
(Β·πOLDβπ)) |
8 | | ajfval.3 |
. . . . . . . . . 10
β’ π =
(Β·πOLDβπ) |
9 | 7, 8 | eqtr4di 2791 |
. . . . . . . . 9
β’ (π’ = π β
(Β·πOLDβπ’) = π) |
10 | 9 | oveqd 7378 |
. . . . . . . 8
β’ (π’ = π β (π₯(Β·πOLDβπ’)(π βπ¦)) = (π₯π(π βπ¦))) |
11 | 10 | eqeq2d 2744 |
. . . . . . 7
β’ (π’ = π β (((π‘βπ₯)(Β·πOLDβπ€)π¦) = (π₯(Β·πOLDβπ’)(π βπ¦)) β ((π‘βπ₯)(Β·πOLDβπ€)π¦) = (π₯π(π βπ¦)))) |
12 | 11 | ralbidv 3171 |
. . . . . 6
β’ (π’ = π β (βπ¦ β (BaseSetβπ€)((π‘βπ₯)(Β·πOLDβπ€)π¦) = (π₯(Β·πOLDβπ’)(π βπ¦)) β βπ¦ β (BaseSetβπ€)((π‘βπ₯)(Β·πOLDβπ€)π¦) = (π₯π(π βπ¦)))) |
13 | 4, 12 | raleqbidv 3318 |
. . . . 5
β’ (π’ = π β (βπ₯ β (BaseSetβπ’)βπ¦ β (BaseSetβπ€)((π‘βπ₯)(Β·πOLDβπ€)π¦) = (π₯(Β·πOLDβπ’)(π βπ¦)) β βπ₯ β π βπ¦ β (BaseSetβπ€)((π‘βπ₯)(Β·πOLDβπ€)π¦) = (π₯π(π βπ¦)))) |
14 | 5, 6, 13 | 3anbi123d 1437 |
. . . 4
β’ (π’ = π β ((π‘:(BaseSetβπ’)βΆ(BaseSetβπ€) β§ π :(BaseSetβπ€)βΆ(BaseSetβπ’) β§ βπ₯ β (BaseSetβπ’)βπ¦ β (BaseSetβπ€)((π‘βπ₯)(Β·πOLDβπ€)π¦) = (π₯(Β·πOLDβπ’)(π βπ¦))) β (π‘:πβΆ(BaseSetβπ€) β§ π :(BaseSetβπ€)βΆπ β§ βπ₯ β π βπ¦ β (BaseSetβπ€)((π‘βπ₯)(Β·πOLDβπ€)π¦) = (π₯π(π βπ¦))))) |
15 | 14 | opabbidv 5175 |
. . 3
β’ (π’ = π β {β¨π‘, π β© β£ (π‘:(BaseSetβπ’)βΆ(BaseSetβπ€) β§ π :(BaseSetβπ€)βΆ(BaseSetβπ’) β§ βπ₯ β (BaseSetβπ’)βπ¦ β (BaseSetβπ€)((π‘βπ₯)(Β·πOLDβπ€)π¦) = (π₯(Β·πOLDβπ’)(π βπ¦)))} = {β¨π‘, π β© β£ (π‘:πβΆ(BaseSetβπ€) β§ π :(BaseSetβπ€)βΆπ β§ βπ₯ β π βπ¦ β (BaseSetβπ€)((π‘βπ₯)(Β·πOLDβπ€)π¦) = (π₯π(π βπ¦)))}) |
16 | | fveq2 6846 |
. . . . . . 7
β’ (π€ = π β (BaseSetβπ€) = (BaseSetβπ)) |
17 | | ajfval.2 |
. . . . . . 7
β’ π = (BaseSetβπ) |
18 | 16, 17 | eqtr4di 2791 |
. . . . . 6
β’ (π€ = π β (BaseSetβπ€) = π) |
19 | 18 | feq3d 6659 |
. . . . 5
β’ (π€ = π β (π‘:πβΆ(BaseSetβπ€) β π‘:πβΆπ)) |
20 | 18 | feq2d 6658 |
. . . . 5
β’ (π€ = π β (π :(BaseSetβπ€)βΆπ β π :πβΆπ)) |
21 | | fveq2 6846 |
. . . . . . . . . 10
β’ (π€ = π β
(Β·πOLDβπ€) =
(Β·πOLDβπ)) |
22 | | ajfval.4 |
. . . . . . . . . 10
β’ π =
(Β·πOLDβπ) |
23 | 21, 22 | eqtr4di 2791 |
. . . . . . . . 9
β’ (π€ = π β
(Β·πOLDβπ€) = π) |
24 | 23 | oveqd 7378 |
. . . . . . . 8
β’ (π€ = π β ((π‘βπ₯)(Β·πOLDβπ€)π¦) = ((π‘βπ₯)ππ¦)) |
25 | 24 | eqeq1d 2735 |
. . . . . . 7
β’ (π€ = π β (((π‘βπ₯)(Β·πOLDβπ€)π¦) = (π₯π(π βπ¦)) β ((π‘βπ₯)ππ¦) = (π₯π(π βπ¦)))) |
26 | 18, 25 | raleqbidv 3318 |
. . . . . 6
β’ (π€ = π β (βπ¦ β (BaseSetβπ€)((π‘βπ₯)(Β·πOLDβπ€)π¦) = (π₯π(π βπ¦)) β βπ¦ β π ((π‘βπ₯)ππ¦) = (π₯π(π βπ¦)))) |
27 | 26 | ralbidv 3171 |
. . . . 5
β’ (π€ = π β (βπ₯ β π βπ¦ β (BaseSetβπ€)((π‘βπ₯)(Β·πOLDβπ€)π¦) = (π₯π(π βπ¦)) β βπ₯ β π βπ¦ β π ((π‘βπ₯)ππ¦) = (π₯π(π βπ¦)))) |
28 | 19, 20, 27 | 3anbi123d 1437 |
. . . 4
β’ (π€ = π β ((π‘:πβΆ(BaseSetβπ€) β§ π :(BaseSetβπ€)βΆπ β§ βπ₯ β π βπ¦ β (BaseSetβπ€)((π‘βπ₯)(Β·πOLDβπ€)π¦) = (π₯π(π βπ¦))) β (π‘:πβΆπ β§ π :πβΆπ β§ βπ₯ β π βπ¦ β π ((π‘βπ₯)ππ¦) = (π₯π(π βπ¦))))) |
29 | 28 | opabbidv 5175 |
. . 3
β’ (π€ = π β {β¨π‘, π β© β£ (π‘:πβΆ(BaseSetβπ€) β§ π :(BaseSetβπ€)βΆπ β§ βπ₯ β π βπ¦ β (BaseSetβπ€)((π‘βπ₯)(Β·πOLDβπ€)π¦) = (π₯π(π βπ¦)))} = {β¨π‘, π β© β£ (π‘:πβΆπ β§ π :πβΆπ β§ βπ₯ β π βπ¦ β π ((π‘βπ₯)ππ¦) = (π₯π(π βπ¦)))}) |
30 | | df-aj 29741 |
. . 3
β’ adj =
(π’ β NrmCVec, π€ β NrmCVec β¦
{β¨π‘, π β© β£ (π‘:(BaseSetβπ’)βΆ(BaseSetβπ€) β§ π :(BaseSetβπ€)βΆ(BaseSetβπ’) β§ βπ₯ β (BaseSetβπ’)βπ¦ β (BaseSetβπ€)((π‘βπ₯)(Β·πOLDβπ€)π¦) = (π₯(Β·πOLDβπ’)(π βπ¦)))}) |
31 | | ovex 7394 |
. . . . 5
β’ (π βm π) β V |
32 | | ovex 7394 |
. . . . 5
β’ (π βm π) β V |
33 | 31, 32 | xpex 7691 |
. . . 4
β’ ((π βm π) Γ (π βm π)) β V |
34 | 17 | fvexi 6860 |
. . . . . . . . . 10
β’ π β V |
35 | 3 | fvexi 6860 |
. . . . . . . . . 10
β’ π β V |
36 | 34, 35 | elmap 8815 |
. . . . . . . . 9
β’ (π‘ β (π βm π) β π‘:πβΆπ) |
37 | 35, 34 | elmap 8815 |
. . . . . . . . 9
β’ (π β (π βm π) β π :πβΆπ) |
38 | 36, 37 | anbi12i 628 |
. . . . . . . 8
β’ ((π‘ β (π βm π) β§ π β (π βm π)) β (π‘:πβΆπ β§ π :πβΆπ)) |
39 | 38 | biimpri 227 |
. . . . . . 7
β’ ((π‘:πβΆπ β§ π :πβΆπ) β (π‘ β (π βm π) β§ π β (π βm π))) |
40 | 39 | 3adant3 1133 |
. . . . . 6
β’ ((π‘:πβΆπ β§ π :πβΆπ β§ βπ₯ β π βπ¦ β π ((π‘βπ₯)ππ¦) = (π₯π(π βπ¦))) β (π‘ β (π βm π) β§ π β (π βm π))) |
41 | 40 | ssopab2i 5511 |
. . . . 5
β’
{β¨π‘, π β© β£ (π‘:πβΆπ β§ π :πβΆπ β§ βπ₯ β π βπ¦ β π ((π‘βπ₯)ππ¦) = (π₯π(π βπ¦)))} β {β¨π‘, π β© β£ (π‘ β (π βm π) β§ π β (π βm π))} |
42 | | df-xp 5643 |
. . . . 5
β’ ((π βm π) Γ (π βm π)) = {β¨π‘, π β© β£ (π‘ β (π βm π) β§ π β (π βm π))} |
43 | 41, 42 | sseqtrri 3985 |
. . . 4
β’
{β¨π‘, π β© β£ (π‘:πβΆπ β§ π :πβΆπ β§ βπ₯ β π βπ¦ β π ((π‘βπ₯)ππ¦) = (π₯π(π βπ¦)))} β ((π βm π) Γ (π βm π)) |
44 | 33, 43 | ssexi 5283 |
. . 3
β’
{β¨π‘, π β© β£ (π‘:πβΆπ β§ π :πβΆπ β§ βπ₯ β π βπ¦ β π ((π‘βπ₯)ππ¦) = (π₯π(π βπ¦)))} β V |
45 | 15, 29, 30, 44 | ovmpo 7519 |
. 2
β’ ((π β NrmCVec β§ π β NrmCVec) β (πadjπ) = {β¨π‘, π β© β£ (π‘:πβΆπ β§ π :πβΆπ β§ βπ₯ β π βπ¦ β π ((π‘βπ₯)ππ¦) = (π₯π(π βπ¦)))}) |
46 | 1, 45 | eqtrid 2785 |
1
β’ ((π β NrmCVec β§ π β NrmCVec) β π΄ = {β¨π‘, π β© β£ (π‘:πβΆπ β§ π :πβΆπ β§ βπ₯ β π βπ¦ β π ((π‘βπ₯)ππ¦) = (π₯π(π βπ¦)))}) |