Step | Hyp | Ref
| Expression |
1 | | sspmlem.1 |
. . . . 5
β’ (((π β NrmCVec β§ π β π») β§ (π₯ β π β§ π¦ β π)) β (π₯πΉπ¦) = (π₯πΊπ¦)) |
2 | | ovres 7573 |
. . . . . 6
β’ ((π₯ β π β§ π¦ β π) β (π₯(πΊ βΎ (π Γ π))π¦) = (π₯πΊπ¦)) |
3 | 2 | adantl 483 |
. . . . 5
β’ (((π β NrmCVec β§ π β π») β§ (π₯ β π β§ π¦ β π)) β (π₯(πΊ βΎ (π Γ π))π¦) = (π₯πΊπ¦)) |
4 | 1, 3 | eqtr4d 2776 |
. . . 4
β’ (((π β NrmCVec β§ π β π») β§ (π₯ β π β§ π¦ β π)) β (π₯πΉπ¦) = (π₯(πΊ βΎ (π Γ π))π¦)) |
5 | 4 | ralrimivva 3201 |
. . 3
β’ ((π β NrmCVec β§ π β π») β βπ₯ β π βπ¦ β π (π₯πΉπ¦) = (π₯(πΊ βΎ (π Γ π))π¦)) |
6 | | eqid 2733 |
. . 3
β’ (π Γ π) = (π Γ π) |
7 | 5, 6 | jctil 521 |
. 2
β’ ((π β NrmCVec β§ π β π») β ((π Γ π) = (π Γ π) β§ βπ₯ β π βπ¦ β π (π₯πΉπ¦) = (π₯(πΊ βΎ (π Γ π))π¦))) |
8 | | sspmlem.h |
. . . . 5
β’ π» = (SubSpβπ) |
9 | 8 | sspnv 29979 |
. . . 4
β’ ((π β NrmCVec β§ π β π») β π β NrmCVec) |
10 | | sspmlem.2 |
. . . 4
β’ (π β NrmCVec β πΉ:(π Γ π)βΆπ
) |
11 | | ffn 6718 |
. . . 4
β’ (πΉ:(π Γ π)βΆπ
β πΉ Fn (π Γ π)) |
12 | 9, 10, 11 | 3syl 18 |
. . 3
β’ ((π β NrmCVec β§ π β π») β πΉ Fn (π Γ π)) |
13 | | sspmlem.3 |
. . . . . 6
β’ (π β NrmCVec β πΊ:((BaseSetβπ) Γ (BaseSetβπ))βΆπ) |
14 | 13 | ffnd 6719 |
. . . . 5
β’ (π β NrmCVec β πΊ Fn ((BaseSetβπ) Γ (BaseSetβπ))) |
15 | 14 | adantr 482 |
. . . 4
β’ ((π β NrmCVec β§ π β π») β πΊ Fn ((BaseSetβπ) Γ (BaseSetβπ))) |
16 | | eqid 2733 |
. . . . . 6
β’
(BaseSetβπ) =
(BaseSetβπ) |
17 | | sspmlem.y |
. . . . . 6
β’ π = (BaseSetβπ) |
18 | 16, 17, 8 | sspba 29980 |
. . . . 5
β’ ((π β NrmCVec β§ π β π») β π β (BaseSetβπ)) |
19 | | xpss12 5692 |
. . . . 5
β’ ((π β (BaseSetβπ) β§ π β (BaseSetβπ)) β (π Γ π) β ((BaseSetβπ) Γ (BaseSetβπ))) |
20 | 18, 18, 19 | syl2anc 585 |
. . . 4
β’ ((π β NrmCVec β§ π β π») β (π Γ π) β ((BaseSetβπ) Γ (BaseSetβπ))) |
21 | | fnssres 6674 |
. . . 4
β’ ((πΊ Fn ((BaseSetβπ) Γ (BaseSetβπ)) β§ (π Γ π) β ((BaseSetβπ) Γ (BaseSetβπ))) β (πΊ βΎ (π Γ π)) Fn (π Γ π)) |
22 | 15, 20, 21 | syl2anc 585 |
. . 3
β’ ((π β NrmCVec β§ π β π») β (πΊ βΎ (π Γ π)) Fn (π Γ π)) |
23 | | eqfnov 7538 |
. . 3
β’ ((πΉ Fn (π Γ π) β§ (πΊ βΎ (π Γ π)) Fn (π Γ π)) β (πΉ = (πΊ βΎ (π Γ π)) β ((π Γ π) = (π Γ π) β§ βπ₯ β π βπ¦ β π (π₯πΉπ¦) = (π₯(πΊ βΎ (π Γ π))π¦)))) |
24 | 12, 22, 23 | syl2anc 585 |
. 2
β’ ((π β NrmCVec β§ π β π») β (πΉ = (πΊ βΎ (π Γ π)) β ((π Γ π) = (π Γ π) β§ βπ₯ β π βπ¦ β π (π₯πΉπ¦) = (π₯(πΊ βΎ (π Γ π))π¦)))) |
25 | 7, 24 | mpbird 257 |
1
β’ ((π β NrmCVec β§ π β π») β πΉ = (πΊ βΎ (π Γ π))) |