Step | Hyp | Ref
| Expression |
1 | | sspims.h |
. . . . . 6
β’ π» = (SubSpβπ) |
2 | 1 | sspnv 29133 |
. . . . 5
β’ ((π β NrmCVec β§ π β π») β π β NrmCVec) |
3 | | sspims.y |
. . . . . . 7
β’ π = (BaseSetβπ) |
4 | | eqid 2736 |
. . . . . . 7
β’ (
βπ£ βπ) = ( βπ£
βπ) |
5 | 3, 4 | nvmcl 29053 |
. . . . . 6
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄( βπ£ βπ)π΅) β π) |
6 | 5 | 3expb 1120 |
. . . . 5
β’ ((π β NrmCVec β§ (π΄ β π β§ π΅ β π)) β (π΄( βπ£ βπ)π΅) β π) |
7 | 2, 6 | sylan 581 |
. . . 4
β’ (((π β NrmCVec β§ π β π») β§ (π΄ β π β§ π΅ β π)) β (π΄( βπ£ βπ)π΅) β π) |
8 | | eqid 2736 |
. . . . . 6
β’
(normCVβπ) = (normCVβπ) |
9 | | eqid 2736 |
. . . . . 6
β’
(normCVβπ) = (normCVβπ) |
10 | 3, 8, 9, 1 | sspnval 29144 |
. . . . 5
β’ ((π β NrmCVec β§ π β π» β§ (π΄( βπ£ βπ)π΅) β π) β ((normCVβπ)β(π΄( βπ£ βπ)π΅)) = ((normCVβπ)β(π΄( βπ£ βπ)π΅))) |
11 | 10 | 3expa 1118 |
. . . 4
β’ (((π β NrmCVec β§ π β π») β§ (π΄( βπ£ βπ)π΅) β π) β ((normCVβπ)β(π΄( βπ£ βπ)π΅)) = ((normCVβπ)β(π΄( βπ£ βπ)π΅))) |
12 | 7, 11 | syldan 592 |
. . 3
β’ (((π β NrmCVec β§ π β π») β§ (π΄ β π β§ π΅ β π)) β ((normCVβπ)β(π΄( βπ£ βπ)π΅)) = ((normCVβπ)β(π΄( βπ£ βπ)π΅))) |
13 | | eqid 2736 |
. . . . 5
β’ (
βπ£ βπ) = ( βπ£
βπ) |
14 | 3, 13, 4, 1 | sspmval 29140 |
. . . 4
β’ (((π β NrmCVec β§ π β π») β§ (π΄ β π β§ π΅ β π)) β (π΄( βπ£ βπ)π΅) = (π΄( βπ£ βπ)π΅)) |
15 | 14 | fveq2d 6808 |
. . 3
β’ (((π β NrmCVec β§ π β π») β§ (π΄ β π β§ π΅ β π)) β ((normCVβπ)β(π΄( βπ£ βπ)π΅)) = ((normCVβπ)β(π΄( βπ£ βπ)π΅))) |
16 | 12, 15 | eqtrd 2776 |
. 2
β’ (((π β NrmCVec β§ π β π») β§ (π΄ β π β§ π΅ β π)) β ((normCVβπ)β(π΄( βπ£ βπ)π΅)) = ((normCVβπ)β(π΄( βπ£ βπ)π΅))) |
17 | | sspims.c |
. . . . 5
β’ πΆ = (IndMetβπ) |
18 | 3, 4, 9, 17 | imsdval 29093 |
. . . 4
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄πΆπ΅) = ((normCVβπ)β(π΄( βπ£ βπ)π΅))) |
19 | 18 | 3expb 1120 |
. . 3
β’ ((π β NrmCVec β§ (π΄ β π β§ π΅ β π)) β (π΄πΆπ΅) = ((normCVβπ)β(π΄( βπ£ βπ)π΅))) |
20 | 2, 19 | sylan 581 |
. 2
β’ (((π β NrmCVec β§ π β π») β§ (π΄ β π β§ π΅ β π)) β (π΄πΆπ΅) = ((normCVβπ)β(π΄( βπ£ βπ)π΅))) |
21 | | eqid 2736 |
. . . . . . 7
β’
(BaseSetβπ) =
(BaseSetβπ) |
22 | 21, 3, 1 | sspba 29134 |
. . . . . 6
β’ ((π β NrmCVec β§ π β π») β π β (BaseSetβπ)) |
23 | 22 | sseld 3925 |
. . . . 5
β’ ((π β NrmCVec β§ π β π») β (π΄ β π β π΄ β (BaseSetβπ))) |
24 | 22 | sseld 3925 |
. . . . 5
β’ ((π β NrmCVec β§ π β π») β (π΅ β π β π΅ β (BaseSetβπ))) |
25 | 23, 24 | anim12d 610 |
. . . 4
β’ ((π β NrmCVec β§ π β π») β ((π΄ β π β§ π΅ β π) β (π΄ β (BaseSetβπ) β§ π΅ β (BaseSetβπ)))) |
26 | 25 | imp 408 |
. . 3
β’ (((π β NrmCVec β§ π β π») β§ (π΄ β π β§ π΅ β π)) β (π΄ β (BaseSetβπ) β§ π΅ β (BaseSetβπ))) |
27 | | sspims.d |
. . . . . 6
β’ π· = (IndMetβπ) |
28 | 21, 13, 8, 27 | imsdval 29093 |
. . . . 5
β’ ((π β NrmCVec β§ π΄ β (BaseSetβπ) β§ π΅ β (BaseSetβπ)) β (π΄π·π΅) = ((normCVβπ)β(π΄( βπ£ βπ)π΅))) |
29 | 28 | 3expb 1120 |
. . . 4
β’ ((π β NrmCVec β§ (π΄ β (BaseSetβπ) β§ π΅ β (BaseSetβπ))) β (π΄π·π΅) = ((normCVβπ)β(π΄( βπ£ βπ)π΅))) |
30 | 29 | adantlr 713 |
. . 3
β’ (((π β NrmCVec β§ π β π») β§ (π΄ β (BaseSetβπ) β§ π΅ β (BaseSetβπ))) β (π΄π·π΅) = ((normCVβπ)β(π΄( βπ£ βπ)π΅))) |
31 | 26, 30 | syldan 592 |
. 2
β’ (((π β NrmCVec β§ π β π») β§ (π΄ β π β§ π΅ β π)) β (π΄π·π΅) = ((normCVβπ)β(π΄( βπ£ βπ)π΅))) |
32 | 16, 20, 31 | 3eqtr4d 2786 |
1
β’ (((π β NrmCVec β§ π β π») β§ (π΄ β π β§ π΅ β π)) β (π΄πΆπ΅) = (π΄π·π΅)) |