Step | Hyp | Ref
| Expression |
1 | | ax-1cn 11114 |
. . 3
β’ 1 β
β |
2 | | lnoadd.1 |
. . . 4
β’ π = (BaseSetβπ) |
3 | | eqid 2733 |
. . . 4
β’
(BaseSetβπ) =
(BaseSetβπ) |
4 | | lnoadd.5 |
. . . 4
β’ πΊ = ( +π£
βπ) |
5 | | lnoadd.6 |
. . . 4
β’ π» = ( +π£
βπ) |
6 | | eqid 2733 |
. . . 4
β’ (
Β·π OLD βπ) = ( Β·π OLD
βπ) |
7 | | eqid 2733 |
. . . 4
β’ (
Β·π OLD βπ) = ( Β·π OLD
βπ) |
8 | | lnoadd.7 |
. . . 4
β’ πΏ = (π LnOp π) |
9 | 2, 3, 4, 5, 6, 7, 8 | lnolin 29738 |
. . 3
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (1 β β β§ π΄ β π β§ π΅ β π)) β (πβ((1(
Β·π OLD βπ)π΄)πΊπ΅)) = ((1(
Β·π OLD βπ)(πβπ΄))π»(πβπ΅))) |
10 | 1, 9 | mp3anr1 1459 |
. 2
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β π β§ π΅ β π)) β (πβ((1(
Β·π OLD βπ)π΄)πΊπ΅)) = ((1(
Β·π OLD βπ)(πβπ΄))π»(πβπ΅))) |
11 | | simp1 1137 |
. . . 4
β’ ((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β π β NrmCVec) |
12 | | simpl 484 |
. . . 4
β’ ((π΄ β π β§ π΅ β π) β π΄ β π) |
13 | 2, 6 | nvsid 29611 |
. . . 4
β’ ((π β NrmCVec β§ π΄ β π) β (1(
Β·π OLD βπ)π΄) = π΄) |
14 | 11, 12, 13 | syl2an 597 |
. . 3
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β π β§ π΅ β π)) β (1(
Β·π OLD βπ)π΄) = π΄) |
15 | 14 | fvoveq1d 7380 |
. 2
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β π β§ π΅ β π)) β (πβ((1(
Β·π OLD βπ)π΄)πΊπ΅)) = (πβ(π΄πΊπ΅))) |
16 | | simpl2 1193 |
. . . 4
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β π β§ π΅ β π)) β π β NrmCVec) |
17 | 2, 3, 8 | lnof 29739 |
. . . . 5
β’ ((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β π:πβΆ(BaseSetβπ)) |
18 | | ffvelcdm 7033 |
. . . . 5
β’ ((π:πβΆ(BaseSetβπ) β§ π΄ β π) β (πβπ΄) β (BaseSetβπ)) |
19 | 17, 12, 18 | syl2an 597 |
. . . 4
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β π β§ π΅ β π)) β (πβπ΄) β (BaseSetβπ)) |
20 | 3, 7 | nvsid 29611 |
. . . 4
β’ ((π β NrmCVec β§ (πβπ΄) β (BaseSetβπ)) β (1(
Β·π OLD βπ)(πβπ΄)) = (πβπ΄)) |
21 | 16, 19, 20 | syl2anc 585 |
. . 3
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β π β§ π΅ β π)) β (1(
Β·π OLD βπ)(πβπ΄)) = (πβπ΄)) |
22 | 21 | oveq1d 7373 |
. 2
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β π β§ π΅ β π)) β ((1(
Β·π OLD βπ)(πβπ΄))π»(πβπ΅)) = ((πβπ΄)π»(πβπ΅))) |
23 | 10, 15, 22 | 3eqtr3d 2781 |
1
β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ (π΄ β π β§ π΅ β π)) β (πβ(π΄πΊπ΅)) = ((πβπ΄)π»(πβπ΅))) |