Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . 3
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β β β§ π΅ β π)) β (π β NrmCVec β§ π β NrmCVec β§ π β πΏ)) |
2 | | simprl 770 |
. . 3
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β β β§ π΅ β π)) β π΄ β β) |
3 | | simprr 772 |
. . 3
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β β β§ π΅ β π)) β π΅ β π) |
4 | | simpl1 1192 |
. . . 4
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β β β§ π΅ β π)) β π β NrmCVec) |
5 | | lnomul.1 |
. . . . 5
β’ π = (BaseSetβπ) |
6 | | eqid 2733 |
. . . . 5
β’
(0vecβπ) = (0vecβπ) |
7 | 5, 6 | nvzcl 29618 |
. . . 4
β’ (π β NrmCVec β
(0vecβπ)
β π) |
8 | 4, 7 | syl 17 |
. . 3
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β β β§ π΅ β π)) β (0vecβπ) β π) |
9 | | eqid 2733 |
. . . 4
β’
(BaseSetβπ) =
(BaseSetβπ) |
10 | | eqid 2733 |
. . . 4
β’ (
+π£ βπ) = ( +π£ βπ) |
11 | | eqid 2733 |
. . . 4
β’ (
+π£ βπ) = ( +π£ βπ) |
12 | | lnomul.5 |
. . . 4
β’ π
= (
Β·π OLD βπ) |
13 | | lnomul.6 |
. . . 4
β’ π = (
Β·π OLD βπ) |
14 | | lnomul.7 |
. . . 4
β’ πΏ = (π LnOp π) |
15 | 5, 9, 10, 11, 12, 13, 14 | lnolin 29738 |
. . 3
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β β β§ π΅ β π β§ (0vecβπ) β π)) β (πβ((π΄π
π΅)( +π£ βπ)(0vecβπ))) = ((π΄π(πβπ΅))( +π£ βπ)(πβ(0vecβπ)))) |
16 | 1, 2, 3, 8, 15 | syl13anc 1373 |
. 2
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β β β§ π΅ β π)) β (πβ((π΄π
π΅)( +π£ βπ)(0vecβπ))) = ((π΄π(πβπ΅))( +π£ βπ)(πβ(0vecβπ)))) |
17 | 5, 12 | nvscl 29610 |
. . . . 5
β’ ((π β NrmCVec β§ π΄ β β β§ π΅ β π) β (π΄π
π΅) β π) |
18 | 4, 2, 3, 17 | syl3anc 1372 |
. . . 4
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β β β§ π΅ β π)) β (π΄π
π΅) β π) |
19 | 5, 10, 6 | nv0rid 29619 |
. . . 4
β’ ((π β NrmCVec β§ (π΄π
π΅) β π) β ((π΄π
π΅)( +π£ βπ)(0vecβπ)) = (π΄π
π΅)) |
20 | 4, 18, 19 | syl2anc 585 |
. . 3
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β β β§ π΅ β π)) β ((π΄π
π΅)( +π£ βπ)(0vecβπ)) = (π΄π
π΅)) |
21 | 20 | fveq2d 6847 |
. 2
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β β β§ π΅ β π)) β (πβ((π΄π
π΅)( +π£ βπ)(0vecβπ))) = (πβ(π΄π
π΅))) |
22 | | eqid 2733 |
. . . . . 6
β’
(0vecβπ) = (0vecβπ) |
23 | 5, 9, 6, 22, 14 | lno0 29740 |
. . . . 5
β’ ((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β (πβ(0vecβπ)) =
(0vecβπ)) |
24 | 23 | oveq2d 7374 |
. . . 4
β’ ((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β ((π΄π(πβπ΅))( +π£ βπ)(πβ(0vecβπ))) = ((π΄π(πβπ΅))( +π£ βπ)(0vecβπ))) |
25 | 24 | adantr 482 |
. . 3
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β β β§ π΅ β π)) β ((π΄π(πβπ΅))( +π£ βπ)(πβ(0vecβπ))) = ((π΄π(πβπ΅))( +π£ βπ)(0vecβπ))) |
26 | | simpl2 1193 |
. . . 4
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β β β§ π΅ β π)) β π β NrmCVec) |
27 | 5, 9, 14 | lnof 29739 |
. . . . . . 7
β’ ((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β π:πβΆ(BaseSetβπ)) |
28 | 27 | adantr 482 |
. . . . . 6
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β β β§ π΅ β π)) β π:πβΆ(BaseSetβπ)) |
29 | 28, 3 | ffvelcdmd 7037 |
. . . . 5
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β β β§ π΅ β π)) β (πβπ΅) β (BaseSetβπ)) |
30 | 9, 13 | nvscl 29610 |
. . . . 5
β’ ((π β NrmCVec β§ π΄ β β β§ (πβπ΅) β (BaseSetβπ)) β (π΄π(πβπ΅)) β (BaseSetβπ)) |
31 | 26, 2, 29, 30 | syl3anc 1372 |
. . . 4
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β β β§ π΅ β π)) β (π΄π(πβπ΅)) β (BaseSetβπ)) |
32 | 9, 11, 22 | nv0rid 29619 |
. . . 4
β’ ((π β NrmCVec β§ (π΄π(πβπ΅)) β (BaseSetβπ)) β ((π΄π(πβπ΅))( +π£ βπ)(0vecβπ)) = (π΄π(πβπ΅))) |
33 | 26, 31, 32 | syl2anc 585 |
. . 3
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β β β§ π΅ β π)) β ((π΄π(πβπ΅))( +π£ βπ)(0vecβπ)) = (π΄π(πβπ΅))) |
34 | 25, 33 | eqtrd 2773 |
. 2
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β β β§ π΅ β π)) β ((π΄π(πβπ΅))( +π£ βπ)(πβ(0vecβπ))) = (π΄π(πβπ΅))) |
35 | 16, 21, 34 | 3eqtr3d 2781 |
1
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β β β§ π΅ β π)) β (πβ(π΄π
π΅)) = (π΄π(πβπ΅))) |