Step | Hyp | Ref
| Expression |
1 | | df-ne 2941 |
. . . . 5
β’ (π΄ β 0 β Β¬ π΄ = 0) |
2 | | oveq2 7369 |
. . . . . . . 8
β’ ((π΄ππ΅) = π β ((1 / π΄)π(π΄ππ΅)) = ((1 / π΄)ππ)) |
3 | 2 | ad2antlr 726 |
. . . . . . 7
β’ ((((π β NrmCVec β§ π΄ β β β§ π΅ β π) β§ (π΄ππ΅) = π) β§ π΄ β 0) β ((1 / π΄)π(π΄ππ΅)) = ((1 / π΄)ππ)) |
4 | | recid2 11836 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π΄ β 0) β ((1 / π΄) Β· π΄) = 1) |
5 | 4 | oveq1d 7376 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π΄ β 0) β (((1 / π΄) Β· π΄)ππ΅) = (1ππ΅)) |
6 | 5 | 3ad2antl2 1187 |
. . . . . . . . 9
β’ (((π β NrmCVec β§ π΄ β β β§ π΅ β π) β§ π΄ β 0) β (((1 / π΄) Β· π΄)ππ΅) = (1ππ΅)) |
7 | | simpl1 1192 |
. . . . . . . . . 10
β’ (((π β NrmCVec β§ π΄ β β β§ π΅ β π) β§ π΄ β 0) β π β NrmCVec) |
8 | | reccl 11828 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π΄ β 0) β (1 / π΄) β
β) |
9 | 8 | 3ad2antl2 1187 |
. . . . . . . . . 10
β’ (((π β NrmCVec β§ π΄ β β β§ π΅ β π) β§ π΄ β 0) β (1 / π΄) β β) |
10 | | simpl2 1193 |
. . . . . . . . . 10
β’ (((π β NrmCVec β§ π΄ β β β§ π΅ β π) β§ π΄ β 0) β π΄ β β) |
11 | | simpl3 1194 |
. . . . . . . . . 10
β’ (((π β NrmCVec β§ π΄ β β β§ π΅ β π) β§ π΄ β 0) β π΅ β π) |
12 | | nvmul0or.1 |
. . . . . . . . . . 11
β’ π = (BaseSetβπ) |
13 | | nvmul0or.4 |
. . . . . . . . . . 11
β’ π = (
Β·π OLD βπ) |
14 | 12, 13 | nvsass 29619 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ ((1 /
π΄) β β β§
π΄ β β β§
π΅ β π)) β (((1 / π΄) Β· π΄)ππ΅) = ((1 / π΄)π(π΄ππ΅))) |
15 | 7, 9, 10, 11, 14 | syl13anc 1373 |
. . . . . . . . 9
β’ (((π β NrmCVec β§ π΄ β β β§ π΅ β π) β§ π΄ β 0) β (((1 / π΄) Β· π΄)ππ΅) = ((1 / π΄)π(π΄ππ΅))) |
16 | 12, 13 | nvsid 29618 |
. . . . . . . . . . 11
β’ ((π β NrmCVec β§ π΅ β π) β (1ππ΅) = π΅) |
17 | 16 | 3adant2 1132 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ π΄ β β β§ π΅ β π) β (1ππ΅) = π΅) |
18 | 17 | adantr 482 |
. . . . . . . . 9
β’ (((π β NrmCVec β§ π΄ β β β§ π΅ β π) β§ π΄ β 0) β (1ππ΅) = π΅) |
19 | 6, 15, 18 | 3eqtr3d 2781 |
. . . . . . . 8
β’ (((π β NrmCVec β§ π΄ β β β§ π΅ β π) β§ π΄ β 0) β ((1 / π΄)π(π΄ππ΅)) = π΅) |
20 | 19 | adantlr 714 |
. . . . . . 7
β’ ((((π β NrmCVec β§ π΄ β β β§ π΅ β π) β§ (π΄ππ΅) = π) β§ π΄ β 0) β ((1 / π΄)π(π΄ππ΅)) = π΅) |
21 | | nvmul0or.6 |
. . . . . . . . . . . 12
β’ π = (0vecβπ) |
22 | 13, 21 | nvsz 29629 |
. . . . . . . . . . 11
β’ ((π β NrmCVec β§ (1 / π΄) β β) β ((1 /
π΄)ππ) = π) |
23 | 8, 22 | sylan2 594 |
. . . . . . . . . 10
β’ ((π β NrmCVec β§ (π΄ β β β§ π΄ β 0)) β ((1 / π΄)ππ) = π) |
24 | 23 | anassrs 469 |
. . . . . . . . 9
β’ (((π β NrmCVec β§ π΄ β β) β§ π΄ β 0) β ((1 / π΄)ππ) = π) |
25 | 24 | 3adantl3 1169 |
. . . . . . . 8
β’ (((π β NrmCVec β§ π΄ β β β§ π΅ β π) β§ π΄ β 0) β ((1 / π΄)ππ) = π) |
26 | 25 | adantlr 714 |
. . . . . . 7
β’ ((((π β NrmCVec β§ π΄ β β β§ π΅ β π) β§ (π΄ππ΅) = π) β§ π΄ β 0) β ((1 / π΄)ππ) = π) |
27 | 3, 20, 26 | 3eqtr3d 2781 |
. . . . . 6
β’ ((((π β NrmCVec β§ π΄ β β β§ π΅ β π) β§ (π΄ππ΅) = π) β§ π΄ β 0) β π΅ = π) |
28 | 27 | ex 414 |
. . . . 5
β’ (((π β NrmCVec β§ π΄ β β β§ π΅ β π) β§ (π΄ππ΅) = π) β (π΄ β 0 β π΅ = π)) |
29 | 1, 28 | biimtrrid 242 |
. . . 4
β’ (((π β NrmCVec β§ π΄ β β β§ π΅ β π) β§ (π΄ππ΅) = π) β (Β¬ π΄ = 0 β π΅ = π)) |
30 | 29 | orrd 862 |
. . 3
β’ (((π β NrmCVec β§ π΄ β β β§ π΅ β π) β§ (π΄ππ΅) = π) β (π΄ = 0 β¨ π΅ = π)) |
31 | 30 | ex 414 |
. 2
β’ ((π β NrmCVec β§ π΄ β β β§ π΅ β π) β ((π΄ππ΅) = π β (π΄ = 0 β¨ π΅ = π))) |
32 | 12, 13, 21 | nv0 29628 |
. . . . 5
β’ ((π β NrmCVec β§ π΅ β π) β (0ππ΅) = π) |
33 | | oveq1 7368 |
. . . . . 6
β’ (π΄ = 0 β (π΄ππ΅) = (0ππ΅)) |
34 | 33 | eqeq1d 2735 |
. . . . 5
β’ (π΄ = 0 β ((π΄ππ΅) = π β (0ππ΅) = π)) |
35 | 32, 34 | syl5ibrcom 247 |
. . . 4
β’ ((π β NrmCVec β§ π΅ β π) β (π΄ = 0 β (π΄ππ΅) = π)) |
36 | 35 | 3adant2 1132 |
. . 3
β’ ((π β NrmCVec β§ π΄ β β β§ π΅ β π) β (π΄ = 0 β (π΄ππ΅) = π)) |
37 | 13, 21 | nvsz 29629 |
. . . . 5
β’ ((π β NrmCVec β§ π΄ β β) β (π΄ππ) = π) |
38 | | oveq2 7369 |
. . . . . 6
β’ (π΅ = π β (π΄ππ΅) = (π΄ππ)) |
39 | 38 | eqeq1d 2735 |
. . . . 5
β’ (π΅ = π β ((π΄ππ΅) = π β (π΄ππ) = π)) |
40 | 37, 39 | syl5ibrcom 247 |
. . . 4
β’ ((π β NrmCVec β§ π΄ β β) β (π΅ = π β (π΄ππ΅) = π)) |
41 | 40 | 3adant3 1133 |
. . 3
β’ ((π β NrmCVec β§ π΄ β β β§ π΅ β π) β (π΅ = π β (π΄ππ΅) = π)) |
42 | 36, 41 | jaod 858 |
. 2
β’ ((π β NrmCVec β§ π΄ β β β§ π΅ β π) β ((π΄ = 0 β¨ π΅ = π) β (π΄ππ΅) = π)) |
43 | 31, 42 | impbid 211 |
1
β’ ((π β NrmCVec β§ π΄ β β β§ π΅ β π) β ((π΄ππ΅) = π β (π΄ = 0 β¨ π΅ = π))) |