Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . . . . . . . . 11
β’
(BaseSetβπ) =
(BaseSetβπ) |
2 | | sspg.g |
. . . . . . . . . . 11
β’ πΊ = ( +π£
βπ) |
3 | 1, 2 | nvgf 29602 |
. . . . . . . . . 10
β’ (π β NrmCVec β πΊ:((BaseSetβπ) Γ (BaseSetβπ))βΆ(BaseSetβπ)) |
4 | 3 | ffund 6677 |
. . . . . . . . 9
β’ (π β NrmCVec β Fun πΊ) |
5 | 4 | funresd 6549 |
. . . . . . . 8
β’ (π β NrmCVec β Fun
(πΊ βΎ (π Γ π))) |
6 | 5 | adantr 482 |
. . . . . . 7
β’ ((π β NrmCVec β§ π β π») β Fun (πΊ βΎ (π Γ π))) |
7 | | sspg.h |
. . . . . . . . . 10
β’ π» = (SubSpβπ) |
8 | 7 | sspnv 29710 |
. . . . . . . . 9
β’ ((π β NrmCVec β§ π β π») β π β NrmCVec) |
9 | | sspg.y |
. . . . . . . . . 10
β’ π = (BaseSetβπ) |
10 | | sspg.f |
. . . . . . . . . 10
β’ πΉ = ( +π£
βπ) |
11 | 9, 10 | nvgf 29602 |
. . . . . . . . 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
β’ (
Β·π OLD βπ) = ( Β·π OLD
βπ) |
17 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (
Β·π OLD βπ) = ( Β·π OLD
βπ) |
18 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(normCVβπ) = (normCVβπ) |
19 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(normCVβπ) = (normCVβπ) |
20 | 2, 10, 16, 17, 18, 19, 7 | isssp 29708 |
. . . . . . . . . . 11
β’ (π β NrmCVec β (π β π» β (π β NrmCVec β§ (πΉ β πΊ β§ (
Β·π OLD βπ) β (
Β·π OLD βπ) β§ (normCVβπ) β
(normCVβπ))))) |
21 | 20 | simplbda 501 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ π β π») β (πΉ β πΊ β§ (
Β·π OLD βπ) β (
Β·π OLD βπ) β§ (normCVβπ) β
(normCVβπ))) |
22 | 21 | simp1d 1143 |
. . . . . . . . 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βπ) Γ (BaseSetβπ))) |
34 | 33 | adantr 482 |
. . . 4
β’ ((π β NrmCVec β§ π β π») β πΊ Fn ((BaseSetβπ) Γ (BaseSetβπ))) |
35 | 1, 9, 7 | sspba 29711 |
. . . . 5
β’ ((π β NrmCVec β§ π β π») β π β (BaseSetβπ)) |
36 | | xpss12 5653 |
. . . . 5
β’ ((π β (BaseSetβπ) β§ π β (BaseSetβπ)) β (π Γ π) β ((BaseSetβπ) Γ (BaseSetβπ))) |
37 | 35, 35, 36 | syl2anc 585 |
. . . 4
β’ ((π β NrmCVec β§ π β π») β (π Γ π) β ((BaseSetβπ) Γ (BaseSetβπ))) |
38 | | fnssres 6629 |
. . . 4
β’ ((πΊ Fn ((BaseSetβπ) Γ (BaseSetβπ)) β§ (π Γ π) β ((BaseSetβπ) Γ (BaseSetβπ))) β (πΊ βΎ (π Γ π)) Fn (π Γ π)) |
39 | 34, 37, 38 | syl2anc 585 |
. . 3
β’ ((π β NrmCVec β§ π β π») β (πΊ βΎ (π Γ π)) Fn (π Γ π)) |
40 | | eqfnov 7490 |
. . 3
β’ ((πΉ Fn (π Γ π) β§ (πΊ βΎ (π Γ π)) Fn (π Γ π)) β (πΉ = (πΊ βΎ (π Γ π)) β ((π Γ π) = (π Γ π) β§ βπ₯ β π βπ¦ β π (π₯πΉπ¦) = (π₯(πΊ βΎ (π Γ π))π¦)))) |
41 | 13, 39, 40 | syl2anc 585 |
. 2
β’ ((π β NrmCVec β§ π β π») β (πΉ = (πΊ βΎ (π Γ π)) β ((π Γ π) = (π Γ π) β§ βπ₯ β π βπ¦ β π (π₯πΉπ¦) = (π₯(πΊ βΎ (π Γ π))π¦)))) |
42 | 32, 41 | mpbird 257 |
1
β’ ((π β NrmCVec β§ π β π») β πΉ = (πΊ βΎ (π Γ π))) |