Step | Hyp | Ref
| Expression |
1 | | ip2eqi.u |
. . . . . 6
β’ π β
CPreHilOLD |
2 | 1 | phnvi 30334 |
. . . . 5
β’ π β NrmCVec |
3 | | ip2eqi.1 |
. . . . . 6
β’ π = (BaseSetβπ) |
4 | | eqid 2730 |
. . . . . 6
β’ (
βπ£ βπ) = ( βπ£
βπ) |
5 | 3, 4 | nvmcl 30164 |
. . . . 5
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄( βπ£ βπ)π΅) β π) |
6 | 2, 5 | mp3an1 1446 |
. . . 4
β’ ((π΄ β π β§ π΅ β π) β (π΄( βπ£ βπ)π΅) β π) |
7 | | oveq1 7420 |
. . . . . 6
β’ (π₯ = (π΄( βπ£ βπ)π΅) β (π₯ππ΄) = ((π΄( βπ£ βπ)π΅)ππ΄)) |
8 | | oveq1 7420 |
. . . . . 6
β’ (π₯ = (π΄( βπ£ βπ)π΅) β (π₯ππ΅) = ((π΄( βπ£ βπ)π΅)ππ΅)) |
9 | 7, 8 | eqeq12d 2746 |
. . . . 5
β’ (π₯ = (π΄( βπ£ βπ)π΅) β ((π₯ππ΄) = (π₯ππ΅) β ((π΄( βπ£ βπ)π΅)ππ΄) = ((π΄( βπ£ βπ)π΅)ππ΅))) |
10 | 9 | rspcv 3609 |
. . . 4
β’ ((π΄( βπ£
βπ)π΅) β π β (βπ₯ β π (π₯ππ΄) = (π₯ππ΅) β ((π΄( βπ£ βπ)π΅)ππ΄) = ((π΄( βπ£ βπ)π΅)ππ΅))) |
11 | 6, 10 | syl 17 |
. . 3
β’ ((π΄ β π β§ π΅ β π) β (βπ₯ β π (π₯ππ΄) = (π₯ππ΅) β ((π΄( βπ£ βπ)π΅)ππ΄) = ((π΄( βπ£ βπ)π΅)ππ΅))) |
12 | | simpl 481 |
. . . . . . 7
β’ ((π΄ β π β§ π΅ β π) β π΄ β π) |
13 | | simpr 483 |
. . . . . . 7
β’ ((π΄ β π β§ π΅ β π) β π΅ β π) |
14 | | ip2eqi.7 |
. . . . . . . . 9
β’ π =
(Β·πOLDβπ) |
15 | 3, 4, 14 | dipsubdi 30367 |
. . . . . . . 8
β’ ((π β CPreHilOLD
β§ ((π΄(
βπ£ βπ)π΅) β π β§ π΄ β π β§ π΅ β π)) β ((π΄( βπ£ βπ)π΅)π(π΄( βπ£ βπ)π΅)) = (((π΄( βπ£ βπ)π΅)ππ΄) β ((π΄( βπ£ βπ)π΅)ππ΅))) |
16 | 1, 15 | mpan 686 |
. . . . . . 7
β’ (((π΄( βπ£
βπ)π΅) β π β§ π΄ β π β§ π΅ β π) β ((π΄( βπ£ βπ)π΅)π(π΄( βπ£ βπ)π΅)) = (((π΄( βπ£ βπ)π΅)ππ΄) β ((π΄( βπ£ βπ)π΅)ππ΅))) |
17 | 6, 12, 13, 16 | syl3anc 1369 |
. . . . . 6
β’ ((π΄ β π β§ π΅ β π) β ((π΄( βπ£ βπ)π΅)π(π΄( βπ£ βπ)π΅)) = (((π΄( βπ£ βπ)π΅)ππ΄) β ((π΄( βπ£ βπ)π΅)ππ΅))) |
18 | 17 | eqeq1d 2732 |
. . . . 5
β’ ((π΄ β π β§ π΅ β π) β (((π΄( βπ£ βπ)π΅)π(π΄( βπ£ βπ)π΅)) = 0 β (((π΄( βπ£ βπ)π΅)ππ΄) β ((π΄( βπ£ βπ)π΅)ππ΅)) = 0)) |
19 | | eqid 2730 |
. . . . . . . 8
β’
(0vecβπ) = (0vecβπ) |
20 | 3, 19, 14 | ipz 30237 |
. . . . . . 7
β’ ((π β NrmCVec β§ (π΄( βπ£
βπ)π΅) β π) β (((π΄( βπ£ βπ)π΅)π(π΄( βπ£ βπ)π΅)) = 0 β (π΄( βπ£ βπ)π΅) = (0vecβπ))) |
21 | 2, 20 | mpan 686 |
. . . . . 6
β’ ((π΄( βπ£
βπ)π΅) β π β (((π΄( βπ£ βπ)π΅)π(π΄( βπ£ βπ)π΅)) = 0 β (π΄( βπ£ βπ)π΅) = (0vecβπ))) |
22 | 6, 21 | syl 17 |
. . . . 5
β’ ((π΄ β π β§ π΅ β π) β (((π΄( βπ£ βπ)π΅)π(π΄( βπ£ βπ)π΅)) = 0 β (π΄( βπ£ βπ)π΅) = (0vecβπ))) |
23 | 18, 22 | bitr3d 280 |
. . . 4
β’ ((π΄ β π β§ π΅ β π) β ((((π΄( βπ£ βπ)π΅)ππ΄) β ((π΄( βπ£ βπ)π΅)ππ΅)) = 0 β (π΄( βπ£ βπ)π΅) = (0vecβπ))) |
24 | 3, 14 | dipcl 30230 |
. . . . . . 7
β’ ((π β NrmCVec β§ (π΄( βπ£
βπ)π΅) β π β§ π΄ β π) β ((π΄( βπ£ βπ)π΅)ππ΄) β β) |
25 | 2, 24 | mp3an1 1446 |
. . . . . 6
β’ (((π΄( βπ£
βπ)π΅) β π β§ π΄ β π) β ((π΄( βπ£ βπ)π΅)ππ΄) β β) |
26 | 6, 12, 25 | syl2anc 582 |
. . . . 5
β’ ((π΄ β π β§ π΅ β π) β ((π΄( βπ£ βπ)π΅)ππ΄) β β) |
27 | 3, 14 | dipcl 30230 |
. . . . . . 7
β’ ((π β NrmCVec β§ (π΄( βπ£
βπ)π΅) β π β§ π΅ β π) β ((π΄( βπ£ βπ)π΅)ππ΅) β β) |
28 | 2, 27 | mp3an1 1446 |
. . . . . 6
β’ (((π΄( βπ£
βπ)π΅) β π β§ π΅ β π) β ((π΄( βπ£ βπ)π΅)ππ΅) β β) |
29 | 6, 28 | sylancom 586 |
. . . . 5
β’ ((π΄ β π β§ π΅ β π) β ((π΄( βπ£ βπ)π΅)ππ΅) β β) |
30 | 26, 29 | subeq0ad 11587 |
. . . 4
β’ ((π΄ β π β§ π΅ β π) β ((((π΄( βπ£ βπ)π΅)ππ΄) β ((π΄( βπ£ βπ)π΅)ππ΅)) = 0 β ((π΄( βπ£ βπ)π΅)ππ΄) = ((π΄( βπ£ βπ)π΅)ππ΅))) |
31 | 3, 4, 19 | nvmeq0 30176 |
. . . . 5
β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((π΄( βπ£ βπ)π΅) = (0vecβπ) β π΄ = π΅)) |
32 | 2, 31 | mp3an1 1446 |
. . . 4
β’ ((π΄ β π β§ π΅ β π) β ((π΄( βπ£ βπ)π΅) = (0vecβπ) β π΄ = π΅)) |
33 | 23, 30, 32 | 3bitr3d 308 |
. . 3
β’ ((π΄ β π β§ π΅ β π) β (((π΄( βπ£ βπ)π΅)ππ΄) = ((π΄( βπ£ βπ)π΅)ππ΅) β π΄ = π΅)) |
34 | 11, 33 | sylibd 238 |
. 2
β’ ((π΄ β π β§ π΅ β π) β (βπ₯ β π (π₯ππ΄) = (π₯ππ΅) β π΄ = π΅)) |
35 | | oveq2 7421 |
. . 3
β’ (π΄ = π΅ β (π₯ππ΄) = (π₯ππ΅)) |
36 | 35 | ralrimivw 3148 |
. 2
β’ (π΄ = π΅ β βπ₯ β π (π₯ππ΄) = (π₯ππ΅)) |
37 | 34, 36 | impbid1 224 |
1
β’ ((π΄ β π β§ π΅ β π) β (βπ₯ β π (π₯ππ΄) = (π₯ππ΅) β π΄ = π΅)) |