Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . . . . . . . 11
β’
(BaseSetβπ) =
(BaseSetβπ) |
2 | | ssps.s |
. . . . . . . . . . 11
β’ π = (
Β·π OLD βπ) |
3 | 1, 2 | nvsf 29603 |
. . . . . . . . . 10
β’ (π β NrmCVec β π:(β Γ
(BaseSetβπ))βΆ(BaseSetβπ)) |
4 | 3 | ffund 6677 |
. . . . . . . . 9
β’ (π β NrmCVec β Fun π) |
5 | 4 | funresd 6549 |
. . . . . . . 8
β’ (π β NrmCVec β Fun
(π βΎ (β Γ
π))) |
6 | 5 | adantr 482 |
. . . . . . 7
β’ ((π β NrmCVec β§ π β π») β Fun (π βΎ (β Γ π))) |
7 | | ssps.h |
. . . . . . . . . 10
β’ π» = (SubSpβπ) |
8 | 7 | sspnv 29710 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ π β π») β π β NrmCVec) |
9 | | ssps.y |
. . . . . . . . . 10
β’ π = (BaseSetβπ) |
10 | | ssps.r |
. . . . . . . . . 10
β’ π
= (
Β·π OLD βπ) |
11 | 9, 10 | nvsf 29603 |
. . . . . . . . 9
β’ (π β NrmCVec β π
:(β Γ π)βΆπ) |
12 | 8, 11 | syl 17 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π β π») β π
:(β Γ π)βΆπ) |
13 | 12 | ffnd 6674 |
. . . . . . 7
β’ ((π β NrmCVec β§ π β π») β π
Fn (β Γ π)) |
14 | | fnresdm 6625 |
. . . . . . . . 9
β’ (π
Fn (β Γ π) β (π
βΎ (β Γ π)) = π
) |
15 | 13, 14 | syl 17 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π β π») β (π
βΎ (β Γ π)) = π
) |
16 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (
+π£ βπ) = ( +π£ βπ) |
17 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (
+π£ βπ) = ( +π£ βπ) |
18 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(normCVβπ) = (normCVβπ) |
19 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(normCVβπ) = (normCVβπ) |
20 | 16, 17, 2, 10, 18, 19, 7 | isssp 29708 |
. . . . . . . . . . 11
β’ (π β NrmCVec β (π β π» β (π β NrmCVec β§ ((
+π£ βπ) β ( +π£
βπ) β§ π
β π β§ (normCVβπ) β
(normCVβπ))))) |
21 | 20 | simplbda 501 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ π β π») β (( +π£
βπ) β (
+π£ βπ) β§ π
β π β§ (normCVβπ) β
(normCVβπ))) |
22 | 21 | simp2d 1144 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ π β π») β π
β π) |
23 | | ssres 5969 |
. . . . . . . . 9
β’ (π
β π β (π
βΎ (β Γ π)) β (π βΎ (β Γ π))) |
24 | 22, 23 | syl 17 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π β π») β (π
βΎ (β Γ π)) β (π βΎ (β Γ π))) |
25 | 15, 24 | eqsstrrd 3988 |
. . . . . . 7
β’ ((π β NrmCVec β§ π β π») β π
β (π βΎ (β Γ π))) |
26 | 6, 13, 25 | 3jca 1129 |
. . . . . 6
β’ ((π β NrmCVec β§ π β π») β (Fun (π βΎ (β Γ π)) β§ π
Fn (β Γ π) β§ π
β (π βΎ (β Γ π)))) |
27 | | oprssov 7528 |
. . . . . 6
β’ (((Fun
(π βΎ (β Γ
π)) β§ π
Fn (β Γ π) β§ π
β (π βΎ (β Γ π))) β§ (π₯ β β β§ π¦ β π)) β (π₯(π βΎ (β Γ π))π¦) = (π₯π
π¦)) |
28 | 26, 27 | sylan 581 |
. . . . 5
β’ (((π β NrmCVec β§ π β π») β§ (π₯ β β β§ π¦ β π)) β (π₯(π βΎ (β Γ π))π¦) = (π₯π
π¦)) |
29 | 28 | eqcomd 2743 |
. . . 4
β’ (((π β NrmCVec β§ π β π») β§ (π₯ β β β§ π¦ β π)) β (π₯π
π¦) = (π₯(π βΎ (β Γ π))π¦)) |
30 | 29 | ralrimivva 3198 |
. . 3
β’ ((π β NrmCVec β§ π β π») β βπ₯ β β βπ¦ β π (π₯π
π¦) = (π₯(π βΎ (β Γ π))π¦)) |
31 | | eqid 2737 |
. . 3
β’ (β
Γ π) = (β
Γ π) |
32 | 30, 31 | jctil 521 |
. 2
β’ ((π β NrmCVec β§ π β π») β ((β Γ π) = (β Γ π) β§ βπ₯ β β βπ¦ β π (π₯π
π¦) = (π₯(π βΎ (β Γ π))π¦))) |
33 | 3 | ffnd 6674 |
. . . . 5
β’ (π β NrmCVec β π Fn (β Γ
(BaseSetβπ))) |
34 | 33 | adantr 482 |
. . . 4
β’ ((π β NrmCVec β§ π β π») β π Fn (β Γ (BaseSetβπ))) |
35 | | ssid 3971 |
. . . . 5
β’ β
β β |
36 | 1, 9, 7 | sspba 29711 |
. . . . 5
β’ ((π β NrmCVec β§ π β π») β π β (BaseSetβπ)) |
37 | | xpss12 5653 |
. . . . 5
β’ ((β
β β β§ π
β (BaseSetβπ))
β (β Γ π)
β (β Γ (BaseSetβπ))) |
38 | 35, 36, 37 | sylancr 588 |
. . . 4
β’ ((π β NrmCVec β§ π β π») β (β Γ π) β (β Γ
(BaseSetβπ))) |
39 | | fnssres 6629 |
. . . 4
β’ ((π Fn (β Γ
(BaseSetβπ)) β§
(β Γ π) β
(β Γ (BaseSetβπ))) β (π βΎ (β Γ π)) Fn (β Γ π)) |
40 | 34, 38, 39 | syl2anc 585 |
. . 3
β’ ((π β NrmCVec β§ π β π») β (π βΎ (β Γ π)) Fn (β Γ π)) |
41 | | eqfnov 7490 |
. . 3
β’ ((π
Fn (β Γ π) β§ (π βΎ (β Γ π)) Fn (β Γ π)) β (π
= (π βΎ (β Γ π)) β ((β Γ π) = (β Γ π) β§ βπ₯ β β βπ¦ β π (π₯π
π¦) = (π₯(π βΎ (β Γ π))π¦)))) |
42 | 13, 40, 41 | syl2anc 585 |
. 2
β’ ((π β NrmCVec β§ π β π») β (π
= (π βΎ (β Γ π)) β ((β Γ π) = (β Γ π) β§ βπ₯ β β βπ¦ β π (π₯π
π¦) = (π₯(π βΎ (β Γ π))π¦)))) |
43 | 32, 42 | mpbird 257 |
1
β’ ((π β NrmCVec β§ π β π») β π
= (π βΎ (β Γ π))) |