Step | Hyp | Ref
| Expression |
1 | | cnlnadjlem.1 |
. . . . . . . 8
β’ π β LinOp |
2 | 1 | lnopfi 30953 |
. . . . . . 7
β’ π: ββΆ
β |
3 | 2 | ffvelcdmi 7039 |
. . . . . 6
β’ (π β β β (πβπ) β β) |
4 | | hicl 30064 |
. . . . . 6
β’ (((πβπ) β β β§ π¦ β β) β ((πβπ) Β·ih π¦) β
β) |
5 | 3, 4 | sylan 581 |
. . . . 5
β’ ((π β β β§ π¦ β β) β ((πβπ) Β·ih π¦) β
β) |
6 | 5 | ancoms 460 |
. . . 4
β’ ((π¦ β β β§ π β β) β ((πβπ) Β·ih π¦) β
β) |
7 | | cnlnadjlem.3 |
. . . 4
β’ πΊ = (π β β β¦ ((πβπ) Β·ih π¦)) |
8 | 6, 7 | fmptd 7067 |
. . 3
β’ (π¦ β β β πΊ:
ββΆβ) |
9 | | hvmulcl 29997 |
. . . . . . 7
β’ ((π₯ β β β§ π€ β β) β (π₯
Β·β π€) β β) |
10 | 1 | lnopaddi 30955 |
. . . . . . . . . . . 12
β’ (((π₯
Β·β π€) β β β§ π§ β β) β (πβ((π₯ Β·β π€) +β π§)) = ((πβ(π₯ Β·β π€)) +β (πβπ§))) |
11 | 10 | 3adant3 1133 |
. . . . . . . . . . 11
β’ (((π₯
Β·β π€) β β β§ π§ β β β§ π¦ β β) β (πβ((π₯ Β·β π€) +β π§)) = ((πβ(π₯ Β·β π€)) +β (πβπ§))) |
12 | 11 | oveq1d 7377 |
. . . . . . . . . 10
β’ (((π₯
Β·β π€) β β β§ π§ β β β§ π¦ β β) β ((πβ((π₯ Β·β π€) +β π§))
Β·ih π¦) = (((πβ(π₯ Β·β π€)) +β (πβπ§)) Β·ih π¦)) |
13 | 2 | ffvelcdmi 7039 |
. . . . . . . . . . 11
β’ ((π₯
Β·β π€) β β β (πβ(π₯ Β·β π€)) β
β) |
14 | 2 | ffvelcdmi 7039 |
. . . . . . . . . . 11
β’ (π§ β β β (πβπ§) β β) |
15 | | id 22 |
. . . . . . . . . . 11
β’ (π¦ β β β π¦ β
β) |
16 | | ax-his2 30067 |
. . . . . . . . . . 11
β’ (((πβ(π₯ Β·β π€)) β β β§ (πβπ§) β β β§ π¦ β β) β (((πβ(π₯ Β·β π€)) +β (πβπ§)) Β·ih π¦) = (((πβ(π₯ Β·β π€))
Β·ih π¦) + ((πβπ§) Β·ih π¦))) |
17 | 13, 14, 15, 16 | syl3an 1161 |
. . . . . . . . . 10
β’ (((π₯
Β·β π€) β β β§ π§ β β β§ π¦ β β) β (((πβ(π₯ Β·β π€)) +β (πβπ§)) Β·ih π¦) = (((πβ(π₯ Β·β π€))
Β·ih π¦) + ((πβπ§) Β·ih π¦))) |
18 | 12, 17 | eqtrd 2777 |
. . . . . . . . 9
β’ (((π₯
Β·β π€) β β β§ π§ β β β§ π¦ β β) β ((πβ((π₯ Β·β π€) +β π§))
Β·ih π¦) = (((πβ(π₯ Β·β π€))
Β·ih π¦) + ((πβπ§) Β·ih π¦))) |
19 | 18 | 3comr 1126 |
. . . . . . . 8
β’ ((π¦ β β β§ (π₯
Β·β π€) β β β§ π§ β β) β ((πβ((π₯ Β·β π€) +β π§))
Β·ih π¦) = (((πβ(π₯ Β·β π€))
Β·ih π¦) + ((πβπ§) Β·ih π¦))) |
20 | 19 | 3expa 1119 |
. . . . . . 7
β’ (((π¦ β β β§ (π₯
Β·β π€) β β) β§ π§ β β) β ((πβ((π₯ Β·β π€) +β π§))
Β·ih π¦) = (((πβ(π₯ Β·β π€))
Β·ih π¦) + ((πβπ§) Β·ih π¦))) |
21 | 9, 20 | sylanl2 680 |
. . . . . 6
β’ (((π¦ β β β§ (π₯ β β β§ π€ β β)) β§ π§ β β) β ((πβ((π₯ Β·β π€) +β π§))
Β·ih π¦) = (((πβ(π₯ Β·β π€))
Β·ih π¦) + ((πβπ§) Β·ih π¦))) |
22 | | hvaddcl 29996 |
. . . . . . . . 9
β’ (((π₯
Β·β π€) β β β§ π§ β β) β ((π₯ Β·β π€) +β π§) β
β) |
23 | 9, 22 | sylan 581 |
. . . . . . . 8
β’ (((π₯ β β β§ π€ β β) β§ π§ β β) β ((π₯
Β·β π€) +β π§) β β) |
24 | | cnlnadjlem.2 |
. . . . . . . . 9
β’ π β ContOp |
25 | 1, 24, 7 | cnlnadjlem1 31051 |
. . . . . . . 8
β’ (((π₯
Β·β π€) +β π§) β β β (πΊβ((π₯ Β·β π€) +β π§)) = ((πβ((π₯ Β·β π€) +β π§))
Β·ih π¦)) |
26 | 23, 25 | syl 17 |
. . . . . . 7
β’ (((π₯ β β β§ π€ β β) β§ π§ β β) β (πΊβ((π₯ Β·β π€) +β π§)) = ((πβ((π₯ Β·β π€) +β π§))
Β·ih π¦)) |
27 | 26 | adantll 713 |
. . . . . 6
β’ (((π¦ β β β§ (π₯ β β β§ π€ β β)) β§ π§ β β) β (πΊβ((π₯ Β·β π€) +β π§)) = ((πβ((π₯ Β·β π€) +β π§))
Β·ih π¦)) |
28 | 2 | ffvelcdmi 7039 |
. . . . . . . . . . 11
β’ (π€ β β β (πβπ€) β β) |
29 | | ax-his3 30068 |
. . . . . . . . . . 11
β’ ((π₯ β β β§ (πβπ€) β β β§ π¦ β β) β ((π₯ Β·β (πβπ€)) Β·ih π¦) = (π₯ Β· ((πβπ€) Β·ih π¦))) |
30 | 28, 29 | syl3an2 1165 |
. . . . . . . . . 10
β’ ((π₯ β β β§ π€ β β β§ π¦ β β) β ((π₯
Β·β (πβπ€)) Β·ih π¦) = (π₯ Β· ((πβπ€) Β·ih π¦))) |
31 | 30 | 3comr 1126 |
. . . . . . . . 9
β’ ((π¦ β β β§ π₯ β β β§ π€ β β) β ((π₯
Β·β (πβπ€)) Β·ih π¦) = (π₯ Β· ((πβπ€) Β·ih π¦))) |
32 | 31 | 3expb 1121 |
. . . . . . . 8
β’ ((π¦ β β β§ (π₯ β β β§ π€ β β)) β ((π₯
Β·β (πβπ€)) Β·ih π¦) = (π₯ Β· ((πβπ€) Β·ih π¦))) |
33 | 1 | lnopmuli 30956 |
. . . . . . . . . 10
β’ ((π₯ β β β§ π€ β β) β (πβ(π₯ Β·β π€)) = (π₯ Β·β (πβπ€))) |
34 | 33 | oveq1d 7377 |
. . . . . . . . 9
β’ ((π₯ β β β§ π€ β β) β ((πβ(π₯ Β·β π€))
Β·ih π¦) = ((π₯ Β·β (πβπ€)) Β·ih π¦)) |
35 | 34 | adantl 483 |
. . . . . . . 8
β’ ((π¦ β β β§ (π₯ β β β§ π€ β β)) β ((πβ(π₯ Β·β π€))
Β·ih π¦) = ((π₯ Β·β (πβπ€)) Β·ih π¦)) |
36 | 1, 24, 7 | cnlnadjlem1 31051 |
. . . . . . . . . 10
β’ (π€ β β β (πΊβπ€) = ((πβπ€) Β·ih π¦)) |
37 | 36 | oveq2d 7378 |
. . . . . . . . 9
β’ (π€ β β β (π₯ Β· (πΊβπ€)) = (π₯ Β· ((πβπ€) Β·ih π¦))) |
38 | 37 | ad2antll 728 |
. . . . . . . 8
β’ ((π¦ β β β§ (π₯ β β β§ π€ β β)) β (π₯ Β· (πΊβπ€)) = (π₯ Β· ((πβπ€) Β·ih π¦))) |
39 | 32, 35, 38 | 3eqtr4rd 2788 |
. . . . . . 7
β’ ((π¦ β β β§ (π₯ β β β§ π€ β β)) β (π₯ Β· (πΊβπ€)) = ((πβ(π₯ Β·β π€))
Β·ih π¦)) |
40 | 1, 24, 7 | cnlnadjlem1 31051 |
. . . . . . 7
β’ (π§ β β β (πΊβπ§) = ((πβπ§) Β·ih π¦)) |
41 | 39, 40 | oveqan12d 7381 |
. . . . . 6
β’ (((π¦ β β β§ (π₯ β β β§ π€ β β)) β§ π§ β β) β ((π₯ Β· (πΊβπ€)) + (πΊβπ§)) = (((πβ(π₯ Β·β π€))
Β·ih π¦) + ((πβπ§) Β·ih π¦))) |
42 | 21, 27, 41 | 3eqtr4d 2787 |
. . . . 5
β’ (((π¦ β β β§ (π₯ β β β§ π€ β β)) β§ π§ β β) β (πΊβ((π₯ Β·β π€) +β π§)) = ((π₯ Β· (πΊβπ€)) + (πΊβπ§))) |
43 | 42 | ralrimiva 3144 |
. . . 4
β’ ((π¦ β β β§ (π₯ β β β§ π€ β β)) β
βπ§ β β
(πΊβ((π₯
Β·β π€) +β π§)) = ((π₯ Β· (πΊβπ€)) + (πΊβπ§))) |
44 | 43 | ralrimivva 3198 |
. . 3
β’ (π¦ β β β
βπ₯ β β
βπ€ β β
βπ§ β β
(πΊβ((π₯
Β·β π€) +β π§)) = ((π₯ Β· (πΊβπ€)) + (πΊβπ§))) |
45 | | ellnfn 30867 |
. . 3
β’ (πΊ β LinFn β (πΊ: ββΆβ β§
βπ₯ β β
βπ€ β β
βπ§ β β
(πΊβ((π₯
Β·β π€) +β π§)) = ((π₯ Β· (πΊβπ€)) + (πΊβπ§)))) |
46 | 8, 44, 45 | sylanbrc 584 |
. 2
β’ (π¦ β β β πΊ β LinFn) |
47 | 1, 24 | nmcopexi 31011 |
. . . . 5
β’
(normopβπ) β β |
48 | | normcl 30109 |
. . . . 5
β’ (π¦ β β β
(normββπ¦) β β) |
49 | | remulcl 11143 |
. . . . 5
β’
(((normopβπ) β β β§
(normββπ¦) β β) β
((normopβπ) Β·
(normββπ¦)) β β) |
50 | 47, 48, 49 | sylancr 588 |
. . . 4
β’ (π¦ β β β
((normopβπ) Β·
(normββπ¦)) β β) |
51 | 40 | adantr 482 |
. . . . . . . . . 10
β’ ((π§ β β β§ π¦ β β) β (πΊβπ§) = ((πβπ§) Β·ih π¦)) |
52 | | hicl 30064 |
. . . . . . . . . . 11
β’ (((πβπ§) β β β§ π¦ β β) β ((πβπ§) Β·ih π¦) β
β) |
53 | 14, 52 | sylan 581 |
. . . . . . . . . 10
β’ ((π§ β β β§ π¦ β β) β ((πβπ§) Β·ih π¦) β
β) |
54 | 51, 53 | eqeltrd 2838 |
. . . . . . . . 9
β’ ((π§ β β β§ π¦ β β) β (πΊβπ§) β β) |
55 | 54 | abscld 15328 |
. . . . . . . 8
β’ ((π§ β β β§ π¦ β β) β
(absβ(πΊβπ§)) β
β) |
56 | | normcl 30109 |
. . . . . . . . . 10
β’ ((πβπ§) β β β
(normββ(πβπ§)) β β) |
57 | 14, 56 | syl 17 |
. . . . . . . . 9
β’ (π§ β β β
(normββ(πβπ§)) β β) |
58 | | remulcl 11143 |
. . . . . . . . 9
β’
(((normββ(πβπ§)) β β β§
(normββπ¦) β β) β
((normββ(πβπ§)) Β·
(normββπ¦)) β β) |
59 | 57, 48, 58 | syl2an 597 |
. . . . . . . 8
β’ ((π§ β β β§ π¦ β β) β
((normββ(πβπ§)) Β·
(normββπ¦)) β β) |
60 | | normcl 30109 |
. . . . . . . . . 10
β’ (π§ β β β
(normββπ§) β β) |
61 | | remulcl 11143 |
. . . . . . . . . 10
β’
(((normopβπ) β β β§
(normββπ§) β β) β
((normopβπ) Β·
(normββπ§)) β β) |
62 | 47, 60, 61 | sylancr 588 |
. . . . . . . . 9
β’ (π§ β β β
((normopβπ) Β·
(normββπ§)) β β) |
63 | | remulcl 11143 |
. . . . . . . . 9
β’
((((normopβπ) Β·
(normββπ§)) β β β§
(normββπ¦) β β) β
(((normopβπ) Β·
(normββπ§)) Β·
(normββπ¦)) β β) |
64 | 62, 48, 63 | syl2an 597 |
. . . . . . . 8
β’ ((π§ β β β§ π¦ β β) β
(((normopβπ) Β·
(normββπ§)) Β·
(normββπ¦)) β β) |
65 | 51 | fveq2d 6851 |
. . . . . . . . 9
β’ ((π§ β β β§ π¦ β β) β
(absβ(πΊβπ§)) = (absβ((πβπ§) Β·ih π¦))) |
66 | | bcs 30165 |
. . . . . . . . . 10
β’ (((πβπ§) β β β§ π¦ β β) β (absβ((πβπ§) Β·ih π¦)) β€
((normββ(πβπ§)) Β·
(normββπ¦))) |
67 | 14, 66 | sylan 581 |
. . . . . . . . 9
β’ ((π§ β β β§ π¦ β β) β
(absβ((πβπ§)
Β·ih π¦)) β€
((normββ(πβπ§)) Β·
(normββπ¦))) |
68 | 65, 67 | eqbrtrd 5132 |
. . . . . . . 8
β’ ((π§ β β β§ π¦ β β) β
(absβ(πΊβπ§)) β€
((normββ(πβπ§)) Β·
(normββπ¦))) |
69 | 57 | adantr 482 |
. . . . . . . . 9
β’ ((π§ β β β§ π¦ β β) β
(normββ(πβπ§)) β β) |
70 | 62 | adantr 482 |
. . . . . . . . 9
β’ ((π§ β β β§ π¦ β β) β
((normopβπ) Β·
(normββπ§)) β β) |
71 | | normge0 30110 |
. . . . . . . . . . 11
β’ (π¦ β β β 0 β€
(normββπ¦)) |
72 | 48, 71 | jca 513 |
. . . . . . . . . 10
β’ (π¦ β β β
((normββπ¦) β β β§ 0 β€
(normββπ¦))) |
73 | 72 | adantl 483 |
. . . . . . . . 9
β’ ((π§ β β β§ π¦ β β) β
((normββπ¦) β β β§ 0 β€
(normββπ¦))) |
74 | 1, 24 | nmcoplbi 31012 |
. . . . . . . . . 10
β’ (π§ β β β
(normββ(πβπ§)) β€ ((normopβπ) Β·
(normββπ§))) |
75 | 74 | adantr 482 |
. . . . . . . . 9
β’ ((π§ β β β§ π¦ β β) β
(normββ(πβπ§)) β€ ((normopβπ) Β·
(normββπ§))) |
76 | | lemul1a 12016 |
. . . . . . . . 9
β’
((((normββ(πβπ§)) β β β§
((normopβπ) Β·
(normββπ§)) β β β§
((normββπ¦) β β β§ 0 β€
(normββπ¦))) β§
(normββ(πβπ§)) β€ ((normopβπ) Β·
(normββπ§))) β
((normββ(πβπ§)) Β·
(normββπ¦)) β€ (((normopβπ) Β·
(normββπ§)) Β·
(normββπ¦))) |
77 | 69, 70, 73, 75, 76 | syl31anc 1374 |
. . . . . . . 8
β’ ((π§ β β β§ π¦ β β) β
((normββ(πβπ§)) Β·
(normββπ¦)) β€ (((normopβπ) Β·
(normββπ§)) Β·
(normββπ¦))) |
78 | 55, 59, 64, 68, 77 | letrd 11319 |
. . . . . . 7
β’ ((π§ β β β§ π¦ β β) β
(absβ(πΊβπ§)) β€
(((normopβπ) Β·
(normββπ§)) Β·
(normββπ¦))) |
79 | 60 | recnd 11190 |
. . . . . . . 8
β’ (π§ β β β
(normββπ§) β β) |
80 | 48 | recnd 11190 |
. . . . . . . 8
β’ (π¦ β β β
(normββπ¦) β β) |
81 | 47 | recni 11176 |
. . . . . . . . 9
β’
(normopβπ) β β |
82 | | mul32 11328 |
. . . . . . . . 9
β’
(((normopβπ) β β β§
(normββπ§) β β β§
(normββπ¦) β β) β
(((normopβπ) Β·
(normββπ§)) Β·
(normββπ¦)) = (((normopβπ) Β·
(normββπ¦)) Β·
(normββπ§))) |
83 | 81, 82 | mp3an1 1449 |
. . . . . . . 8
β’
(((normββπ§) β β β§
(normββπ¦) β β) β
(((normopβπ) Β·
(normββπ§)) Β·
(normββπ¦)) = (((normopβπ) Β·
(normββπ¦)) Β·
(normββπ§))) |
84 | 79, 80, 83 | syl2an 597 |
. . . . . . 7
β’ ((π§ β β β§ π¦ β β) β
(((normopβπ) Β·
(normββπ§)) Β·
(normββπ¦)) = (((normopβπ) Β·
(normββπ¦)) Β·
(normββπ§))) |
85 | 78, 84 | breqtrd 5136 |
. . . . . 6
β’ ((π§ β β β§ π¦ β β) β
(absβ(πΊβπ§)) β€
(((normopβπ) Β·
(normββπ¦)) Β·
(normββπ§))) |
86 | 85 | ancoms 460 |
. . . . 5
β’ ((π¦ β β β§ π§ β β) β
(absβ(πΊβπ§)) β€
(((normopβπ) Β·
(normββπ¦)) Β·
(normββπ§))) |
87 | 86 | ralrimiva 3144 |
. . . 4
β’ (π¦ β β β
βπ§ β β
(absβ(πΊβπ§)) β€
(((normopβπ) Β·
(normββπ¦)) Β·
(normββπ§))) |
88 | | oveq1 7369 |
. . . . . . 7
β’ (π₯ =
((normopβπ) Β·
(normββπ¦)) β (π₯ Β·
(normββπ§)) = (((normopβπ) Β·
(normββπ¦)) Β·
(normββπ§))) |
89 | 88 | breq2d 5122 |
. . . . . 6
β’ (π₯ =
((normopβπ) Β·
(normββπ¦)) β ((absβ(πΊβπ§)) β€ (π₯ Β·
(normββπ§)) β (absβ(πΊβπ§)) β€ (((normopβπ) Β·
(normββπ¦)) Β·
(normββπ§)))) |
90 | 89 | ralbidv 3175 |
. . . . 5
β’ (π₯ =
((normopβπ) Β·
(normββπ¦)) β (βπ§ β β (absβ(πΊβπ§)) β€ (π₯ Β·
(normββπ§)) β βπ§ β β (absβ(πΊβπ§)) β€ (((normopβπ) Β·
(normββπ¦)) Β·
(normββπ§)))) |
91 | 90 | rspcev 3584 |
. . . 4
β’
((((normopβπ) Β·
(normββπ¦)) β β β§ βπ§ β β
(absβ(πΊβπ§)) β€
(((normopβπ) Β·
(normββπ¦)) Β·
(normββπ§))) β βπ₯ β β βπ§ β β (absβ(πΊβπ§)) β€ (π₯ Β·
(normββπ§))) |
92 | 50, 87, 91 | syl2anc 585 |
. . 3
β’ (π¦ β β β
βπ₯ β β
βπ§ β β
(absβ(πΊβπ§)) β€ (π₯ Β·
(normββπ§))) |
93 | | lnfncon 31040 |
. . . 4
β’ (πΊ β LinFn β (πΊ β ContFn β
βπ₯ β β
βπ§ β β
(absβ(πΊβπ§)) β€ (π₯ Β·
(normββπ§)))) |
94 | 46, 93 | syl 17 |
. . 3
β’ (π¦ β β β (πΊ β ContFn β
βπ₯ β β
βπ§ β β
(absβ(πΊβπ§)) β€ (π₯ Β·
(normββπ§)))) |
95 | 92, 94 | mpbird 257 |
. 2
β’ (π¦ β β β πΊ β ContFn) |
96 | 46, 95 | jca 513 |
1
β’ (π¦ β β β (πΊ β LinFn β§ πΊ β
ContFn)) |