Step | Hyp | Ref
| Expression |
1 | | hmopf 30913 |
. . . . . . 7
β’ (π β HrmOp β π: ββΆ
β) |
2 | | eleigveccl 30998 |
. . . . . . 7
β’ ((π: ββΆ β β§
π΄ β
(eigvecβπ)) β
π΄ β
β) |
3 | 1, 2 | sylan 580 |
. . . . . 6
β’ ((π β HrmOp β§ π΄ β (eigvecβπ)) β π΄ β β) |
4 | 3 | adantr 481 |
. . . . 5
β’ (((π β HrmOp β§ π΄ β (eigvecβπ)) β§ π΅ β (eigvecβπ)) β π΄ β β) |
5 | | eleigveccl 30998 |
. . . . . . 7
β’ ((π: ββΆ β β§
π΅ β
(eigvecβπ)) β
π΅ β
β) |
6 | 1, 5 | sylan 580 |
. . . . . 6
β’ ((π β HrmOp β§ π΅ β (eigvecβπ)) β π΅ β β) |
7 | 6 | adantlr 713 |
. . . . 5
β’ (((π β HrmOp β§ π΄ β (eigvecβπ)) β§ π΅ β (eigvecβπ)) β π΅ β β) |
8 | 4, 7 | jca 512 |
. . . 4
β’ (((π β HrmOp β§ π΄ β (eigvecβπ)) β§ π΅ β (eigvecβπ)) β (π΄ β β β§ π΅ β β)) |
9 | | eighmre 31002 |
. . . . . . 7
β’ ((π β HrmOp β§ π΄ β (eigvecβπ)) β ((eigvalβπ)βπ΄) β β) |
10 | 9 | recnd 11207 |
. . . . . 6
β’ ((π β HrmOp β§ π΄ β (eigvecβπ)) β ((eigvalβπ)βπ΄) β β) |
11 | 10 | adantr 481 |
. . . . 5
β’ (((π β HrmOp β§ π΄ β (eigvecβπ)) β§ π΅ β (eigvecβπ)) β ((eigvalβπ)βπ΄) β β) |
12 | | eighmre 31002 |
. . . . . . 7
β’ ((π β HrmOp β§ π΅ β (eigvecβπ)) β ((eigvalβπ)βπ΅) β β) |
13 | 12 | recnd 11207 |
. . . . . 6
β’ ((π β HrmOp β§ π΅ β (eigvecβπ)) β ((eigvalβπ)βπ΅) β β) |
14 | 13 | adantlr 713 |
. . . . 5
β’ (((π β HrmOp β§ π΄ β (eigvecβπ)) β§ π΅ β (eigvecβπ)) β ((eigvalβπ)βπ΅) β β) |
15 | 11, 14 | jca 512 |
. . . 4
β’ (((π β HrmOp β§ π΄ β (eigvecβπ)) β§ π΅ β (eigvecβπ)) β (((eigvalβπ)βπ΄) β β β§ ((eigvalβπ)βπ΅) β β)) |
16 | 8, 15 | jca 512 |
. . 3
β’ (((π β HrmOp β§ π΄ β (eigvecβπ)) β§ π΅ β (eigvecβπ)) β ((π΄ β β β§ π΅ β β) β§ (((eigvalβπ)βπ΄) β β β§ ((eigvalβπ)βπ΅) β β))) |
17 | 16 | adantrr 715 |
. 2
β’ (((π β HrmOp β§ π΄ β (eigvecβπ)) β§ (π΅ β (eigvecβπ) β§ ((eigvalβπ)βπ΄) β ((eigvalβπ)βπ΅))) β ((π΄ β β β§ π΅ β β) β§ (((eigvalβπ)βπ΄) β β β§ ((eigvalβπ)βπ΅) β β))) |
18 | | eigvec1 31001 |
. . . . . . . 8
β’ ((π: ββΆ β β§
π΄ β
(eigvecβπ)) β
((πβπ΄) = (((eigvalβπ)βπ΄) Β·β π΄) β§ π΄ β
0β)) |
19 | 18 | simpld 495 |
. . . . . . 7
β’ ((π: ββΆ β β§
π΄ β
(eigvecβπ)) β
(πβπ΄) = (((eigvalβπ)βπ΄) Β·β π΄)) |
20 | 1, 19 | sylan 580 |
. . . . . 6
β’ ((π β HrmOp β§ π΄ β (eigvecβπ)) β (πβπ΄) = (((eigvalβπ)βπ΄) Β·β π΄)) |
21 | 20 | adantr 481 |
. . . . 5
β’ (((π β HrmOp β§ π΄ β (eigvecβπ)) β§ π΅ β (eigvecβπ)) β (πβπ΄) = (((eigvalβπ)βπ΄) Β·β π΄)) |
22 | | eigvec1 31001 |
. . . . . . . 8
β’ ((π: ββΆ β β§
π΅ β
(eigvecβπ)) β
((πβπ΅) = (((eigvalβπ)βπ΅) Β·β π΅) β§ π΅ β
0β)) |
23 | 22 | simpld 495 |
. . . . . . 7
β’ ((π: ββΆ β β§
π΅ β
(eigvecβπ)) β
(πβπ΅) = (((eigvalβπ)βπ΅) Β·β π΅)) |
24 | 1, 23 | sylan 580 |
. . . . . 6
β’ ((π β HrmOp β§ π΅ β (eigvecβπ)) β (πβπ΅) = (((eigvalβπ)βπ΅) Β·β π΅)) |
25 | 24 | adantlr 713 |
. . . . 5
β’ (((π β HrmOp β§ π΄ β (eigvecβπ)) β§ π΅ β (eigvecβπ)) β (πβπ΅) = (((eigvalβπ)βπ΅) Β·β π΅)) |
26 | 21, 25 | jca 512 |
. . . 4
β’ (((π β HrmOp β§ π΄ β (eigvecβπ)) β§ π΅ β (eigvecβπ)) β ((πβπ΄) = (((eigvalβπ)βπ΄) Β·β π΄) β§ (πβπ΅) = (((eigvalβπ)βπ΅) Β·β π΅))) |
27 | 26 | adantrr 715 |
. . 3
β’ (((π β HrmOp β§ π΄ β (eigvecβπ)) β§ (π΅ β (eigvecβπ) β§ ((eigvalβπ)βπ΄) β ((eigvalβπ)βπ΅))) β ((πβπ΄) = (((eigvalβπ)βπ΄) Β·β π΄) β§ (πβπ΅) = (((eigvalβπ)βπ΅) Β·β π΅))) |
28 | 12 | cjred 15138 |
. . . . . . 7
β’ ((π β HrmOp β§ π΅ β (eigvecβπ)) β
(ββ((eigvalβπ)βπ΅)) = ((eigvalβπ)βπ΅)) |
29 | 28 | neeq2d 3000 |
. . . . . 6
β’ ((π β HrmOp β§ π΅ β (eigvecβπ)) β (((eigvalβπ)βπ΄) β (ββ((eigvalβπ)βπ΅)) β ((eigvalβπ)βπ΄) β ((eigvalβπ)βπ΅))) |
30 | 29 | biimpar 478 |
. . . . 5
β’ (((π β HrmOp β§ π΅ β (eigvecβπ)) β§ ((eigvalβπ)βπ΄) β ((eigvalβπ)βπ΅)) β ((eigvalβπ)βπ΄) β (ββ((eigvalβπ)βπ΅))) |
31 | 30 | anasss 467 |
. . . 4
β’ ((π β HrmOp β§ (π΅ β (eigvecβπ) β§ ((eigvalβπ)βπ΄) β ((eigvalβπ)βπ΅))) β ((eigvalβπ)βπ΄) β (ββ((eigvalβπ)βπ΅))) |
32 | 31 | adantlr 713 |
. . 3
β’ (((π β HrmOp β§ π΄ β (eigvecβπ)) β§ (π΅ β (eigvecβπ) β§ ((eigvalβπ)βπ΄) β ((eigvalβπ)βπ΅))) β ((eigvalβπ)βπ΄) β (ββ((eigvalβπ)βπ΅))) |
33 | 27, 32 | jca 512 |
. 2
β’ (((π β HrmOp β§ π΄ β (eigvecβπ)) β§ (π΅ β (eigvecβπ) β§ ((eigvalβπ)βπ΄) β ((eigvalβπ)βπ΅))) β (((πβπ΄) = (((eigvalβπ)βπ΄) Β·β π΄) β§ (πβπ΅) = (((eigvalβπ)βπ΅) Β·β π΅)) β§ ((eigvalβπ)βπ΄) β (ββ((eigvalβπ)βπ΅)))) |
34 | | simpll 765 |
. . . 4
β’ (((π β HrmOp β§ π΄ β (eigvecβπ)) β§ π΅ β (eigvecβπ)) β π β HrmOp) |
35 | | hmop 30961 |
. . . 4
β’ ((π β HrmOp β§ π΄ β β β§ π΅ β β) β (π΄
Β·ih (πβπ΅)) = ((πβπ΄) Β·ih π΅)) |
36 | 34, 4, 7, 35 | syl3anc 1371 |
. . 3
β’ (((π β HrmOp β§ π΄ β (eigvecβπ)) β§ π΅ β (eigvecβπ)) β (π΄ Β·ih (πβπ΅)) = ((πβπ΄) Β·ih π΅)) |
37 | 36 | adantrr 715 |
. 2
β’ (((π β HrmOp β§ π΄ β (eigvecβπ)) β§ (π΅ β (eigvecβπ) β§ ((eigvalβπ)βπ΄) β ((eigvalβπ)βπ΅))) β (π΄ Β·ih (πβπ΅)) = ((πβπ΄) Β·ih π΅)) |
38 | | eigorth 30877 |
. . 3
β’ ((((π΄ β β β§ π΅ β β) β§
(((eigvalβπ)βπ΄) β β β§ ((eigvalβπ)βπ΅) β β)) β§ (((πβπ΄) = (((eigvalβπ)βπ΄) Β·β π΄) β§ (πβπ΅) = (((eigvalβπ)βπ΅) Β·β π΅)) β§ ((eigvalβπ)βπ΄) β (ββ((eigvalβπ)βπ΅)))) β ((π΄ Β·ih (πβπ΅)) = ((πβπ΄) Β·ih π΅) β (π΄ Β·ih π΅) = 0)) |
39 | 38 | biimpa 477 |
. 2
β’
(((((π΄ β
β β§ π΅ β
β) β§ (((eigvalβπ)βπ΄) β β β§ ((eigvalβπ)βπ΅) β β)) β§ (((πβπ΄) = (((eigvalβπ)βπ΄) Β·β π΄) β§ (πβπ΅) = (((eigvalβπ)βπ΅) Β·β π΅)) β§ ((eigvalβπ)βπ΄) β (ββ((eigvalβπ)βπ΅)))) β§ (π΄ Β·ih (πβπ΅)) = ((πβπ΄) Β·ih π΅)) β (π΄ Β·ih π΅) = 0) |
40 | 17, 33, 37, 39 | syl21anc 836 |
1
β’ (((π β HrmOp β§ π΄ β (eigvecβπ)) β§ (π΅ β (eigvecβπ) β§ ((eigvalβπ)βπ΄) β ((eigvalβπ)βπ΅))) β (π΄ Β·ih π΅) = 0) |