Step | Hyp | Ref
| Expression |
1 | | nnrecre 12250 |
. . . . 5
β’ (π β β β (1 /
π) β
β) |
2 | 1 | recnd 11238 |
. . . 4
β’ (π β β β (1 /
π) β
β) |
3 | | ip1i.9 |
. . . . . 6
β’ π β
CPreHilOLD |
4 | 3 | phnvi 30056 |
. . . . 5
β’ π β NrmCVec |
5 | | ip1i.1 |
. . . . . 6
β’ π = (BaseSetβπ) |
6 | | ip1i.4 |
. . . . . 6
β’ π = (
Β·π OLD βπ) |
7 | 5, 6 | nvscl 29866 |
. . . . 5
β’ ((π β NrmCVec β§ (1 / π) β β β§ π΄ β π) β ((1 / π)ππ΄) β π) |
8 | 4, 7 | mp3an1 1448 |
. . . 4
β’ (((1 /
π) β β β§
π΄ β π) β ((1 / π)ππ΄) β π) |
9 | 2, 8 | sylan 580 |
. . 3
β’ ((π β β β§ π΄ β π) β ((1 / π)ππ΄) β π) |
10 | | ipasslem1.b |
. . . 4
β’ π΅ β π |
11 | | ip1i.7 |
. . . . 5
β’ π =
(Β·πOLDβπ) |
12 | 5, 11 | dipcl 29952 |
. . . 4
β’ ((π β NrmCVec β§ ((1 /
π)ππ΄) β π β§ π΅ β π) β (((1 / π)ππ΄)ππ΅) β β) |
13 | 4, 10, 12 | mp3an13 1452 |
. . 3
β’ (((1 /
π)ππ΄) β π β (((1 / π)ππ΄)ππ΅) β β) |
14 | 9, 13 | syl 17 |
. 2
β’ ((π β β β§ π΄ β π) β (((1 / π)ππ΄)ππ΅) β β) |
15 | 5, 11 | dipcl 29952 |
. . . 4
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄ππ΅) β β) |
16 | 4, 10, 15 | mp3an13 1452 |
. . 3
β’ (π΄ β π β (π΄ππ΅) β β) |
17 | | mulcl 11190 |
. . 3
β’ (((1 /
π) β β β§
(π΄ππ΅) β β) β ((1 / π) Β· (π΄ππ΅)) β β) |
18 | 2, 16, 17 | syl2an 596 |
. 2
β’ ((π β β β§ π΄ β π) β ((1 / π) Β· (π΄ππ΅)) β β) |
19 | | nncn 12216 |
. . 3
β’ (π β β β π β
β) |
20 | 19 | adantr 481 |
. 2
β’ ((π β β β§ π΄ β π) β π β β) |
21 | | nnne0 12242 |
. . 3
β’ (π β β β π β 0) |
22 | 21 | adantr 481 |
. 2
β’ ((π β β β§ π΄ β π) β π β 0) |
23 | 19, 21 | recidd 11981 |
. . . . . 6
β’ (π β β β (π Β· (1 / π)) = 1) |
24 | 23 | oveq1d 7420 |
. . . . 5
β’ (π β β β ((π Β· (1 / π)) Β· (π΄ππ΅)) = (1 Β· (π΄ππ΅))) |
25 | 16 | mullidd 11228 |
. . . . 5
β’ (π΄ β π β (1 Β· (π΄ππ΅)) = (π΄ππ΅)) |
26 | 24, 25 | sylan9eq 2792 |
. . . 4
β’ ((π β β β§ π΄ β π) β ((π Β· (1 / π)) Β· (π΄ππ΅)) = (π΄ππ΅)) |
27 | 23 | oveq1d 7420 |
. . . . . . 7
β’ (π β β β ((π Β· (1 / π))ππ΄) = (1ππ΄)) |
28 | 5, 6 | nvsid 29867 |
. . . . . . . 8
β’ ((π β NrmCVec β§ π΄ β π) β (1ππ΄) = π΄) |
29 | 4, 28 | mpan 688 |
. . . . . . 7
β’ (π΄ β π β (1ππ΄) = π΄) |
30 | 27, 29 | sylan9eq 2792 |
. . . . . 6
β’ ((π β β β§ π΄ β π) β ((π Β· (1 / π))ππ΄) = π΄) |
31 | 2 | adantr 481 |
. . . . . . 7
β’ ((π β β β§ π΄ β π) β (1 / π) β β) |
32 | | simpr 485 |
. . . . . . 7
β’ ((π β β β§ π΄ β π) β π΄ β π) |
33 | 5, 6 | nvsass 29868 |
. . . . . . . 8
β’ ((π β NrmCVec β§ (π β β β§ (1 / π) β β β§ π΄ β π)) β ((π Β· (1 / π))ππ΄) = (ππ((1 / π)ππ΄))) |
34 | 4, 33 | mpan 688 |
. . . . . . 7
β’ ((π β β β§ (1 / π) β β β§ π΄ β π) β ((π Β· (1 / π))ππ΄) = (ππ((1 / π)ππ΄))) |
35 | 20, 31, 32, 34 | syl3anc 1371 |
. . . . . 6
β’ ((π β β β§ π΄ β π) β ((π Β· (1 / π))ππ΄) = (ππ((1 / π)ππ΄))) |
36 | 30, 35 | eqtr3d 2774 |
. . . . 5
β’ ((π β β β§ π΄ β π) β π΄ = (ππ((1 / π)ππ΄))) |
37 | 36 | oveq1d 7420 |
. . . 4
β’ ((π β β β§ π΄ β π) β (π΄ππ΅) = ((ππ((1 / π)ππ΄))ππ΅)) |
38 | | nnnn0 12475 |
. . . . . 6
β’ (π β β β π β
β0) |
39 | 38 | adantr 481 |
. . . . 5
β’ ((π β β β§ π΄ β π) β π β
β0) |
40 | | ip1i.2 |
. . . . . 6
β’ πΊ = ( +π£
βπ) |
41 | 5, 40, 6, 11, 3, 10 | ipasslem1 30071 |
. . . . 5
β’ ((π β β0
β§ ((1 / π)ππ΄) β π) β ((ππ((1 / π)ππ΄))ππ΅) = (π Β· (((1 / π)ππ΄)ππ΅))) |
42 | 39, 9, 41 | syl2anc 584 |
. . . 4
β’ ((π β β β§ π΄ β π) β ((ππ((1 / π)ππ΄))ππ΅) = (π Β· (((1 / π)ππ΄)ππ΅))) |
43 | 26, 37, 42 | 3eqtrd 2776 |
. . 3
β’ ((π β β β§ π΄ β π) β ((π Β· (1 / π)) Β· (π΄ππ΅)) = (π Β· (((1 / π)ππ΄)ππ΅))) |
44 | 16 | adantl 482 |
. . . 4
β’ ((π β β β§ π΄ β π) β (π΄ππ΅) β β) |
45 | 20, 31, 44 | mulassd 11233 |
. . 3
β’ ((π β β β§ π΄ β π) β ((π Β· (1 / π)) Β· (π΄ππ΅)) = (π Β· ((1 / π) Β· (π΄ππ΅)))) |
46 | 43, 45 | eqtr3d 2774 |
. 2
β’ ((π β β β§ π΄ β π) β (π Β· (((1 / π)ππ΄)ππ΅)) = (π Β· ((1 / π) Β· (π΄ππ΅)))) |
47 | 14, 18, 20, 22, 46 | mulcanad 11845 |
1
β’ ((π β β β§ π΄ β π) β (((1 / π)ππ΄)ππ΅) = ((1 / π) Β· (π΄ππ΅))) |