Step | Hyp | Ref
| Expression |
1 | | hmopidmch.1 |
. . . . . 6
β’ π β HrmOp |
2 | | hmoplin 30926 |
. . . . . 6
β’ (π β HrmOp β π β LinOp) |
3 | 1, 2 | ax-mp 5 |
. . . . 5
β’ π β LinOp |
4 | 3 | lnopfi 30953 |
. . . 4
β’ π: ββΆ
β |
5 | | ffn 6669 |
. . . 4
β’ (π: ββΆ β β
π Fn
β) |
6 | 4, 5 | ax-mp 5 |
. . 3
β’ π Fn β |
7 | | hmopidmch.2 |
. . . . 5
β’ (π β π) = π |
8 | 1, 7 | hmopidmchi 31135 |
. . . 4
β’ ran π β
Cβ |
9 | 8 | pjfni 30685 |
. . 3
β’
(projββran π) Fn β |
10 | | eqfnfv 6983 |
. . 3
β’ ((π Fn β β§
(projββran π) Fn β) β (π = (projββran π) β βπ₯ β β (πβπ₯) = ((projββran π)βπ₯))) |
11 | 6, 9, 10 | mp2an 691 |
. 2
β’ (π =
(projββran π) β βπ₯ β β (πβπ₯) = ((projββran π)βπ₯)) |
12 | | fnfvelrn 7032 |
. . . . 5
β’ ((π Fn β β§ π₯ β β) β (πβπ₯) β ran π) |
13 | 6, 12 | mpan 689 |
. . . 4
β’ (π₯ β β β (πβπ₯) β ran π) |
14 | | id 22 |
. . . . . 6
β’ (π₯ β β β π₯ β
β) |
15 | 4 | ffvelcdmi 7035 |
. . . . . 6
β’ (π₯ β β β (πβπ₯) β β) |
16 | | hvsubcl 30001 |
. . . . . 6
β’ ((π₯ β β β§ (πβπ₯) β β) β (π₯ ββ (πβπ₯)) β β) |
17 | 14, 15, 16 | syl2anc 585 |
. . . . 5
β’ (π₯ β β β (π₯ ββ
(πβπ₯)) β β) |
18 | | simpl 484 |
. . . . . . . . 9
β’ ((π₯ β β β§ π¦ β β) β π₯ β
β) |
19 | 15 | adantr 482 |
. . . . . . . . 9
β’ ((π₯ β β β§ π¦ β β) β (πβπ₯) β β) |
20 | 4 | ffvelcdmi 7035 |
. . . . . . . . . 10
β’ (π¦ β β β (πβπ¦) β β) |
21 | 20 | adantl 483 |
. . . . . . . . 9
β’ ((π₯ β β β§ π¦ β β) β (πβπ¦) β β) |
22 | | his2sub 30076 |
. . . . . . . . 9
β’ ((π₯ β β β§ (πβπ₯) β β β§ (πβπ¦) β β) β ((π₯ ββ (πβπ₯)) Β·ih (πβπ¦)) = ((π₯ Β·ih (πβπ¦)) β ((πβπ₯) Β·ih (πβπ¦)))) |
23 | 18, 19, 21, 22 | syl3anc 1372 |
. . . . . . . 8
β’ ((π₯ β β β§ π¦ β β) β ((π₯ ββ
(πβπ₯)) Β·ih (πβπ¦)) = ((π₯ Β·ih (πβπ¦)) β ((πβπ₯) Β·ih (πβπ¦)))) |
24 | | hmop 30906 |
. . . . . . . . . . . 12
β’ ((π β HrmOp β§ π₯ β β β§ (πβπ¦) β β) β (π₯ Β·ih (πβ(πβπ¦))) = ((πβπ₯) Β·ih (πβπ¦))) |
25 | 1, 24 | mp3an1 1449 |
. . . . . . . . . . 11
β’ ((π₯ β β β§ (πβπ¦) β β) β (π₯ Β·ih (πβ(πβπ¦))) = ((πβπ₯) Β·ih (πβπ¦))) |
26 | 20, 25 | sylan2 594 |
. . . . . . . . . 10
β’ ((π₯ β β β§ π¦ β β) β (π₯
Β·ih (πβ(πβπ¦))) = ((πβπ₯) Β·ih (πβπ¦))) |
27 | 4, 4 | hocoi 30748 |
. . . . . . . . . . . . 13
β’ (π¦ β β β ((π β π)βπ¦) = (πβ(πβπ¦))) |
28 | 7 | fveq1i 6844 |
. . . . . . . . . . . . 13
β’ ((π β π)βπ¦) = (πβπ¦) |
29 | 27, 28 | eqtr3di 2788 |
. . . . . . . . . . . 12
β’ (π¦ β β β (πβ(πβπ¦)) = (πβπ¦)) |
30 | 29 | adantl 483 |
. . . . . . . . . . 11
β’ ((π₯ β β β§ π¦ β β) β (πβ(πβπ¦)) = (πβπ¦)) |
31 | 30 | oveq2d 7374 |
. . . . . . . . . 10
β’ ((π₯ β β β§ π¦ β β) β (π₯
Β·ih (πβ(πβπ¦))) = (π₯ Β·ih (πβπ¦))) |
32 | 26, 31 | eqtr3d 2775 |
. . . . . . . . 9
β’ ((π₯ β β β§ π¦ β β) β ((πβπ₯) Β·ih (πβπ¦)) = (π₯ Β·ih (πβπ¦))) |
33 | 32 | oveq2d 7374 |
. . . . . . . 8
β’ ((π₯ β β β§ π¦ β β) β ((π₯
Β·ih (πβπ¦)) β ((πβπ₯) Β·ih (πβπ¦))) = ((π₯ Β·ih (πβπ¦)) β (π₯ Β·ih (πβπ¦)))) |
34 | | hicl 30064 |
. . . . . . . . . 10
β’ ((π₯ β β β§ (πβπ¦) β β) β (π₯ Β·ih (πβπ¦)) β β) |
35 | 20, 34 | sylan2 594 |
. . . . . . . . 9
β’ ((π₯ β β β§ π¦ β β) β (π₯
Β·ih (πβπ¦)) β β) |
36 | 35 | subidd 11505 |
. . . . . . . 8
β’ ((π₯ β β β§ π¦ β β) β ((π₯
Β·ih (πβπ¦)) β (π₯ Β·ih (πβπ¦))) = 0) |
37 | 23, 33, 36 | 3eqtrd 2777 |
. . . . . . 7
β’ ((π₯ β β β§ π¦ β β) β ((π₯ ββ
(πβπ₯)) Β·ih (πβπ¦)) = 0) |
38 | 37 | ralrimiva 3140 |
. . . . . 6
β’ (π₯ β β β
βπ¦ β β
((π₯
ββ (πβπ₯)) Β·ih (πβπ¦)) = 0) |
39 | | oveq2 7366 |
. . . . . . . . 9
β’ (π§ = (πβπ¦) β ((π₯ ββ (πβπ₯)) Β·ih π§) = ((π₯ ββ (πβπ₯)) Β·ih (πβπ¦))) |
40 | 39 | eqeq1d 2735 |
. . . . . . . 8
β’ (π§ = (πβπ¦) β (((π₯ ββ (πβπ₯)) Β·ih π§) = 0 β ((π₯ ββ
(πβπ₯)) Β·ih (πβπ¦)) = 0)) |
41 | 40 | ralrn 7039 |
. . . . . . 7
β’ (π Fn β β
(βπ§ β ran π((π₯ ββ (πβπ₯)) Β·ih π§) = 0 β βπ¦ β β ((π₯ ββ
(πβπ₯)) Β·ih (πβπ¦)) = 0)) |
42 | 6, 41 | ax-mp 5 |
. . . . . 6
β’
(βπ§ β
ran π((π₯ ββ (πβπ₯)) Β·ih π§) = 0 β βπ¦ β β ((π₯ ββ
(πβπ₯)) Β·ih (πβπ¦)) = 0) |
43 | 38, 42 | sylibr 233 |
. . . . 5
β’ (π₯ β β β
βπ§ β ran π((π₯ ββ (πβπ₯)) Β·ih π§) = 0) |
44 | 8 | chssii 30215 |
. . . . . 6
β’ ran π β
β |
45 | | ocel 30265 |
. . . . . 6
β’ (ran
π β β β
((π₯
ββ (πβπ₯)) β (β₯βran π) β ((π₯ ββ (πβπ₯)) β β β§ βπ§ β ran π((π₯ ββ (πβπ₯)) Β·ih π§) = 0))) |
46 | 44, 45 | ax-mp 5 |
. . . . 5
β’ ((π₯ ββ
(πβπ₯)) β (β₯βran π) β ((π₯ ββ (πβπ₯)) β β β§ βπ§ β ran π((π₯ ββ (πβπ₯)) Β·ih π§) = 0)) |
47 | 17, 43, 46 | sylanbrc 584 |
. . . 4
β’ (π₯ β β β (π₯ ββ
(πβπ₯)) β (β₯βran π)) |
48 | 8 | pjcompi 30656 |
. . . 4
β’ (((πβπ₯) β ran π β§ (π₯ ββ (πβπ₯)) β (β₯βran π)) β
((projββran π)β((πβπ₯) +β (π₯ ββ (πβπ₯)))) = (πβπ₯)) |
49 | 13, 47, 48 | syl2anc 585 |
. . 3
β’ (π₯ β β β
((projββran π)β((πβπ₯) +β (π₯ ββ (πβπ₯)))) = (πβπ₯)) |
50 | | hvpncan3 30026 |
. . . . 5
β’ (((πβπ₯) β β β§ π₯ β β) β ((πβπ₯) +β (π₯ ββ (πβπ₯))) = π₯) |
51 | 15, 14, 50 | syl2anc 585 |
. . . 4
β’ (π₯ β β β ((πβπ₯) +β (π₯ ββ (πβπ₯))) = π₯) |
52 | 51 | fveq2d 6847 |
. . 3
β’ (π₯ β β β
((projββran π)β((πβπ₯) +β (π₯ ββ (πβπ₯)))) = ((projββran
π)βπ₯)) |
53 | 49, 52 | eqtr3d 2775 |
. 2
β’ (π₯ β β β (πβπ₯) = ((projββran π)βπ₯)) |
54 | 11, 53 | mprgbir 3068 |
1
β’ π =
(projββran π) |