Step | Hyp | Ref
| Expression |
1 | | smueq.a |
. . . . . . . 8
β’ (π β π΄ β
β0) |
2 | 1 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β π΄ β
β0) |
3 | | smueq.b |
. . . . . . . 8
β’ (π β π΅ β
β0) |
4 | 3 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β π΅ β
β0) |
5 | | smueq.p |
. . . . . . 7
β’ π = seq0((π β π« β0, π β β0
β¦ (π sadd {π β β0
β£ (π β π΄ β§ (π β π) β π΅)})), (π β β0 β¦ if(π = 0, β
, (π β 1)))) |
6 | | elfzouz 13582 |
. . . . . . . . 9
β’ (π β (0..^π) β π β
(β€β₯β0)) |
7 | 6 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β π β
(β€β₯β0)) |
8 | | nn0uz 12810 |
. . . . . . . 8
β’
β0 = (β€β₯β0) |
9 | 7, 8 | eleqtrrdi 2845 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β π β β0) |
10 | 9 | nn0zd 12530 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β π β β€) |
11 | 10 | peano2zd 12615 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β (π + 1) β β€) |
12 | | smueq.n |
. . . . . . . . . 10
β’ (π β π β
β0) |
13 | 12 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β π β
β0) |
14 | 13 | nn0zd 12530 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β π β β€) |
15 | | elfzolt2 13587 |
. . . . . . . . . 10
β’ (π β (0..^π) β π < π) |
16 | 15 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β π < π) |
17 | | nn0ltp1le 12566 |
. . . . . . . . . 10
β’ ((π β β0
β§ π β
β0) β (π < π β (π + 1) β€ π)) |
18 | 9, 13, 17 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ π β (0..^π)) β (π < π β (π + 1) β€ π)) |
19 | 16, 18 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β (π + 1) β€ π) |
20 | | eluz2 12774 |
. . . . . . . 8
β’ (π β
(β€β₯β(π + 1)) β ((π + 1) β β€ β§ π β β€ β§ (π + 1) β€ π)) |
21 | 11, 14, 19, 20 | syl3anbrc 1344 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β π β (β€β₯β(π + 1))) |
22 | 2, 4, 5, 9, 21 | smuval2 16367 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β (π β (π΄ smul π΅) β π β (πβπ))) |
23 | 12, 8 | eleqtrdi 2844 |
. . . . . . . . . . 11
β’ (π β π β
(β€β₯β0)) |
24 | | eluzfz2b 13456 |
. . . . . . . . . . 11
β’ (π β
(β€β₯β0) β π β (0...π)) |
25 | 23, 24 | sylib 217 |
. . . . . . . . . 10
β’ (π β π β (0...π)) |
26 | | fveq2 6843 |
. . . . . . . . . . . . . 14
β’ (π₯ = 0 β (πβπ₯) = (πβ0)) |
27 | 26 | ineq1d 4172 |
. . . . . . . . . . . . 13
β’ (π₯ = 0 β ((πβπ₯) β© (0..^π)) = ((πβ0) β© (0..^π))) |
28 | | fveq2 6843 |
. . . . . . . . . . . . . 14
β’ (π₯ = 0 β (πβπ₯) = (πβ0)) |
29 | 28 | ineq1d 4172 |
. . . . . . . . . . . . 13
β’ (π₯ = 0 β ((πβπ₯) β© (0..^π)) = ((πβ0) β© (0..^π))) |
30 | 27, 29 | eqeq12d 2749 |
. . . . . . . . . . . 12
β’ (π₯ = 0 β (((πβπ₯) β© (0..^π)) = ((πβπ₯) β© (0..^π)) β ((πβ0) β© (0..^π)) = ((πβ0) β© (0..^π)))) |
31 | 30 | imbi2d 341 |
. . . . . . . . . . 11
β’ (π₯ = 0 β ((π β ((πβπ₯) β© (0..^π)) = ((πβπ₯) β© (0..^π))) β (π β ((πβ0) β© (0..^π)) = ((πβ0) β© (0..^π))))) |
32 | | fveq2 6843 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β (πβπ₯) = (πβπ)) |
33 | 32 | ineq1d 4172 |
. . . . . . . . . . . . 13
β’ (π₯ = π β ((πβπ₯) β© (0..^π)) = ((πβπ) β© (0..^π))) |
34 | | fveq2 6843 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β (πβπ₯) = (πβπ)) |
35 | 34 | ineq1d 4172 |
. . . . . . . . . . . . 13
β’ (π₯ = π β ((πβπ₯) β© (0..^π)) = ((πβπ) β© (0..^π))) |
36 | 33, 35 | eqeq12d 2749 |
. . . . . . . . . . . 12
β’ (π₯ = π β (((πβπ₯) β© (0..^π)) = ((πβπ₯) β© (0..^π)) β ((πβπ) β© (0..^π)) = ((πβπ) β© (0..^π)))) |
37 | 36 | imbi2d 341 |
. . . . . . . . . . 11
β’ (π₯ = π β ((π β ((πβπ₯) β© (0..^π)) = ((πβπ₯) β© (0..^π))) β (π β ((πβπ) β© (0..^π)) = ((πβπ) β© (0..^π))))) |
38 | | fveq2 6843 |
. . . . . . . . . . . . . 14
β’ (π₯ = (π + 1) β (πβπ₯) = (πβ(π + 1))) |
39 | 38 | ineq1d 4172 |
. . . . . . . . . . . . 13
β’ (π₯ = (π + 1) β ((πβπ₯) β© (0..^π)) = ((πβ(π + 1)) β© (0..^π))) |
40 | | fveq2 6843 |
. . . . . . . . . . . . . 14
β’ (π₯ = (π + 1) β (πβπ₯) = (πβ(π + 1))) |
41 | 40 | ineq1d 4172 |
. . . . . . . . . . . . 13
β’ (π₯ = (π + 1) β ((πβπ₯) β© (0..^π)) = ((πβ(π + 1)) β© (0..^π))) |
42 | 39, 41 | eqeq12d 2749 |
. . . . . . . . . . . 12
β’ (π₯ = (π + 1) β (((πβπ₯) β© (0..^π)) = ((πβπ₯) β© (0..^π)) β ((πβ(π + 1)) β© (0..^π)) = ((πβ(π + 1)) β© (0..^π)))) |
43 | 42 | imbi2d 341 |
. . . . . . . . . . 11
β’ (π₯ = (π + 1) β ((π β ((πβπ₯) β© (0..^π)) = ((πβπ₯) β© (0..^π))) β (π β ((πβ(π + 1)) β© (0..^π)) = ((πβ(π + 1)) β© (0..^π))))) |
44 | | fveq2 6843 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β (πβπ₯) = (πβπ)) |
45 | 44 | ineq1d 4172 |
. . . . . . . . . . . . 13
β’ (π₯ = π β ((πβπ₯) β© (0..^π)) = ((πβπ) β© (0..^π))) |
46 | | fveq2 6843 |
. . . . . . . . . . . . . 14
β’ (π₯ = π β (πβπ₯) = (πβπ)) |
47 | 46 | ineq1d 4172 |
. . . . . . . . . . . . 13
β’ (π₯ = π β ((πβπ₯) β© (0..^π)) = ((πβπ) β© (0..^π))) |
48 | 45, 47 | eqeq12d 2749 |
. . . . . . . . . . . 12
β’ (π₯ = π β (((πβπ₯) β© (0..^π)) = ((πβπ₯) β© (0..^π)) β ((πβπ) β© (0..^π)) = ((πβπ) β© (0..^π)))) |
49 | 48 | imbi2d 341 |
. . . . . . . . . . 11
β’ (π₯ = π β ((π β ((πβπ₯) β© (0..^π)) = ((πβπ₯) β© (0..^π))) β (π β ((πβπ) β© (0..^π)) = ((πβπ) β© (0..^π))))) |
50 | 1, 3, 5 | smup0 16364 |
. . . . . . . . . . . . . 14
β’ (π β (πβ0) = β
) |
51 | | inss1 4189 |
. . . . . . . . . . . . . . . 16
β’ (π΅ β© (0..^π)) β π΅ |
52 | 51, 3 | sstrid 3956 |
. . . . . . . . . . . . . . 15
β’ (π β (π΅ β© (0..^π)) β
β0) |
53 | | smueq.q |
. . . . . . . . . . . . . . 15
β’ π = seq0((π β π« β0, π β β0
β¦ (π sadd {π β β0
β£ (π β π΄ β§ (π β π) β (π΅ β© (0..^π)))})), (π β β0 β¦ if(π = 0, β
, (π β 1)))) |
54 | 1, 52, 53 | smup0 16364 |
. . . . . . . . . . . . . 14
β’ (π β (πβ0) = β
) |
55 | 50, 54 | eqtr4d 2776 |
. . . . . . . . . . . . 13
β’ (π β (πβ0) = (πβ0)) |
56 | 55 | ineq1d 4172 |
. . . . . . . . . . . 12
β’ (π β ((πβ0) β© (0..^π)) = ((πβ0) β© (0..^π))) |
57 | 56 | a1i 11 |
. . . . . . . . . . 11
β’ (π β
(β€β₯β0) β (π β ((πβ0) β© (0..^π)) = ((πβ0) β© (0..^π)))) |
58 | | oveq1 7365 |
. . . . . . . . . . . . . . 15
β’ (((πβπ) β© (0..^π)) = ((πβπ) β© (0..^π)) β (((πβπ) β© (0..^π)) sadd ({π β β0 β£ (π β π΄ β§ (π β π) β π΅)} β© (0..^π))) = (((πβπ) β© (0..^π)) sadd ({π β β0 β£ (π β π΄ β§ (π β π) β π΅)} β© (0..^π)))) |
59 | 58 | ineq1d 4172 |
. . . . . . . . . . . . . 14
β’ (((πβπ) β© (0..^π)) = ((πβπ) β© (0..^π)) β ((((πβπ) β© (0..^π)) sadd ({π β β0 β£ (π β π΄ β§ (π β π) β π΅)} β© (0..^π))) β© (0..^π)) = ((((πβπ) β© (0..^π)) sadd ({π β β0 β£ (π β π΄ β§ (π β π) β π΅)} β© (0..^π))) β© (0..^π))) |
60 | 1 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (0..^π)) β π΄ β
β0) |
61 | 3 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (0..^π)) β π΅ β
β0) |
62 | | elfzonn0 13623 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (0..^π) β π β β0) |
63 | 62 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (0..^π)) β π β β0) |
64 | 60, 61, 5, 63 | smupp1 16365 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) = ((πβπ) sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)})) |
65 | 64 | ineq1d 4172 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β ((πβ(π + 1)) β© (0..^π)) = (((πβπ) sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)}) β© (0..^π))) |
66 | 1, 3, 5 | smupf 16363 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π:β0βΆπ«
β0) |
67 | | ffvelcdm 7033 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π:β0βΆπ«
β0 β§ π
β β0) β (πβπ) β π«
β0) |
68 | 66, 62, 67 | syl2an 597 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (0..^π)) β (πβπ) β π«
β0) |
69 | 68 | elpwid 4570 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0..^π)) β (πβπ) β
β0) |
70 | | ssrab2 4038 |
. . . . . . . . . . . . . . . . . 18
β’ {π β β0
β£ (π β π΄ β§ (π β π) β π΅)} β
β0 |
71 | 70 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0..^π)) β {π β β0 β£ (π β π΄ β§ (π β π) β π΅)} β
β0) |
72 | 12 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0..^π)) β π β
β0) |
73 | 69, 71, 72 | sadeq 16357 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β (((πβπ) sadd {π β β0 β£ (π β π΄ β§ (π β π) β π΅)}) β© (0..^π)) = ((((πβπ) β© (0..^π)) sadd ({π β β0 β£ (π β π΄ β§ (π β π) β π΅)} β© (0..^π))) β© (0..^π))) |
74 | 65, 73 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β ((πβ(π + 1)) β© (0..^π)) = ((((πβπ) β© (0..^π)) sadd ({π β β0 β£ (π β π΄ β§ (π β π) β π΅)} β© (0..^π))) β© (0..^π))) |
75 | 52 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (0..^π)) β (π΅ β© (0..^π)) β
β0) |
76 | 60, 75, 53, 63 | smupp1 16365 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0..^π)) β (πβ(π + 1)) = ((πβπ) sadd {π β β0 β£ (π β π΄ β§ (π β π) β (π΅ β© (0..^π)))})) |
77 | 76 | ineq1d 4172 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β ((πβ(π + 1)) β© (0..^π)) = (((πβπ) sadd {π β β0 β£ (π β π΄ β§ (π β π) β (π΅ β© (0..^π)))}) β© (0..^π))) |
78 | 1, 52, 53 | smupf 16363 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π:β0βΆπ«
β0) |
79 | | ffvelcdm 7033 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π:β0βΆπ«
β0 β§ π
β β0) β (πβπ) β π«
β0) |
80 | 78, 62, 79 | syl2an 597 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (0..^π)) β (πβπ) β π«
β0) |
81 | 80 | elpwid 4570 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0..^π)) β (πβπ) β
β0) |
82 | | ssrab2 4038 |
. . . . . . . . . . . . . . . . . 18
β’ {π β β0
β£ (π β π΄ β§ (π β π) β (π΅ β© (0..^π)))} β
β0 |
83 | 82 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0..^π)) β {π β β0 β£ (π β π΄ β§ (π β π) β (π΅ β© (0..^π)))} β
β0) |
84 | 81, 83, 72 | sadeq 16357 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β (((πβπ) sadd {π β β0 β£ (π β π΄ β§ (π β π) β (π΅ β© (0..^π)))}) β© (0..^π)) = ((((πβπ) β© (0..^π)) sadd ({π β β0 β£ (π β π΄ β§ (π β π) β (π΅ β© (0..^π)))} β© (0..^π))) β© (0..^π))) |
85 | | elinel2 4157 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (β0
β© (0..^π)) β π β (0..^π)) |
86 | 61 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π β (0..^π)) β§ π β (0..^π)) β π΅ β
β0) |
87 | 86 | sseld 3944 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π β (0..^π)) β§ π β (0..^π)) β ((π β π) β π΅ β (π β π) β
β0)) |
88 | | elfzo0 13619 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β (0..^π) β (π β β0 β§ π β β β§ π < π)) |
89 | 88 | simp2bi 1147 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (0..^π) β π β β) |
90 | 89 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ π β (0..^π)) β§ π β (0..^π)) β π β β) |
91 | | elfzonn0 13623 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β (0..^π) β π β β0) |
92 | 91 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ π β (0..^π)) β§ π β (0..^π)) β π β β0) |
93 | 92 | nn0red 12479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ π β (0..^π)) β§ π β (0..^π)) β π β β) |
94 | 63 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ π β (0..^π)) β§ π β (0..^π)) β π β β0) |
95 | 94 | nn0red 12479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ π β (0..^π)) β§ π β (0..^π)) β π β β) |
96 | 93, 95 | resubcld 11588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ π β (0..^π)) β§ π β (0..^π)) β (π β π) β β) |
97 | 90 | nnred 12173 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ π β (0..^π)) β§ π β (0..^π)) β π β β) |
98 | 94 | nn0ge0d 12481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ π β (0..^π)) β§ π β (0..^π)) β 0 β€ π) |
99 | 93, 95 | subge02d 11752 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β§ π β (0..^π)) β§ π β (0..^π)) β (0 β€ π β (π β π) β€ π)) |
100 | 98, 99 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ π β (0..^π)) β§ π β (0..^π)) β (π β π) β€ π) |
101 | | elfzolt2 13587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β (0..^π) β π < π) |
102 | 101 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ π β (0..^π)) β§ π β (0..^π)) β π < π) |
103 | 96, 93, 97, 100, 102 | lelttrd 11318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ π β (0..^π)) β§ π β (0..^π)) β (π β π) < π) |
104 | 90, 103 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ π β (0..^π)) β§ π β (0..^π)) β (π β β β§ (π β π) < π)) |
105 | | elfzo0 13619 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β π) β (0..^π) β ((π β π) β β0 β§ π β β β§ (π β π) < π)) |
106 | | 3anass 1096 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β π) β β0 β§ π β β β§ (π β π) < π) β ((π β π) β β0 β§ (π β β β§ (π β π) < π))) |
107 | 105, 106 | bitri 275 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β π) β (0..^π) β ((π β π) β β0 β§ (π β β β§ (π β π) < π))) |
108 | 107 | baib 537 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β π) β β0 β ((π β π) β (0..^π) β (π β β β§ (π β π) < π))) |
109 | 104, 108 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π β (0..^π)) β§ π β (0..^π)) β ((π β π) β β0 β (π β π) β (0..^π))) |
110 | 87, 109 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β (0..^π)) β§ π β (0..^π)) β ((π β π) β π΅ β (π β π) β (0..^π))) |
111 | 110 | pm4.71rd 564 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β (0..^π)) β§ π β (0..^π)) β ((π β π) β π΅ β ((π β π) β (0..^π) β§ (π β π) β π΅))) |
112 | | ancom 462 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β π) β (0..^π) β§ (π β π) β π΅) β ((π β π) β π΅ β§ (π β π) β (0..^π))) |
113 | | elin 3927 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β π) β (π΅ β© (0..^π)) β ((π β π) β π΅ β§ (π β π) β (0..^π))) |
114 | 112, 113 | bitr4i 278 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β π) β (0..^π) β§ (π β π) β π΅) β (π β π) β (π΅ β© (0..^π))) |
115 | 111, 114 | bitr2di 288 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β (0..^π)) β§ π β (0..^π)) β ((π β π) β (π΅ β© (0..^π)) β (π β π) β π΅)) |
116 | 115 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β (0..^π)) β§ π β (0..^π)) β ((π β π΄ β§ (π β π) β (π΅ β© (0..^π))) β (π β π΄ β§ (π β π) β π΅))) |
117 | 85, 116 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β (0..^π)) β§ π β (β0 β© (0..^π))) β ((π β π΄ β§ (π β π) β (π΅ β© (0..^π))) β (π β π΄ β§ (π β π) β π΅))) |
118 | 117 | rabbidva 3413 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (0..^π)) β {π β (β0 β© (0..^π)) β£ (π β π΄ β§ (π β π) β (π΅ β© (0..^π)))} = {π β (β0 β© (0..^π)) β£ (π β π΄ β§ (π β π) β π΅)}) |
119 | | inrab2 4268 |
. . . . . . . . . . . . . . . . . . 19
β’ ({π β β0
β£ (π β π΄ β§ (π β π) β (π΅ β© (0..^π)))} β© (0..^π)) = {π β (β0 β© (0..^π)) β£ (π β π΄ β§ (π β π) β (π΅ β© (0..^π)))} |
120 | | inrab2 4268 |
. . . . . . . . . . . . . . . . . . 19
β’ ({π β β0
β£ (π β π΄ β§ (π β π) β π΅)} β© (0..^π)) = {π β (β0 β© (0..^π)) β£ (π β π΄ β§ (π β π) β π΅)} |
121 | 118, 119,
120 | 3eqtr4g 2798 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (0..^π)) β ({π β β0 β£ (π β π΄ β§ (π β π) β (π΅ β© (0..^π)))} β© (0..^π)) = ({π β β0 β£ (π β π΄ β§ (π β π) β π΅)} β© (0..^π))) |
122 | 121 | oveq2d 7374 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (0..^π)) β (((πβπ) β© (0..^π)) sadd ({π β β0 β£ (π β π΄ β§ (π β π) β (π΅ β© (0..^π)))} β© (0..^π))) = (((πβπ) β© (0..^π)) sadd ({π β β0 β£ (π β π΄ β§ (π β π) β π΅)} β© (0..^π)))) |
123 | 122 | ineq1d 4172 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (0..^π)) β ((((πβπ) β© (0..^π)) sadd ({π β β0 β£ (π β π΄ β§ (π β π) β (π΅ β© (0..^π)))} β© (0..^π))) β© (0..^π)) = ((((πβπ) β© (0..^π)) sadd ({π β β0 β£ (π β π΄ β§ (π β π) β π΅)} β© (0..^π))) β© (0..^π))) |
124 | 77, 84, 123 | 3eqtrd 2777 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (0..^π)) β ((πβ(π + 1)) β© (0..^π)) = ((((πβπ) β© (0..^π)) sadd ({π β β0 β£ (π β π΄ β§ (π β π) β π΅)} β© (0..^π))) β© (0..^π))) |
125 | 74, 124 | eqeq12d 2749 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (0..^π)) β (((πβ(π + 1)) β© (0..^π)) = ((πβ(π + 1)) β© (0..^π)) β ((((πβπ) β© (0..^π)) sadd ({π β β0 β£ (π β π΄ β§ (π β π) β π΅)} β© (0..^π))) β© (0..^π)) = ((((πβπ) β© (0..^π)) sadd ({π β β0 β£ (π β π΄ β§ (π β π) β π΅)} β© (0..^π))) β© (0..^π)))) |
126 | 59, 125 | syl5ibr 246 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (0..^π)) β (((πβπ) β© (0..^π)) = ((πβπ) β© (0..^π)) β ((πβ(π + 1)) β© (0..^π)) = ((πβ(π + 1)) β© (0..^π)))) |
127 | 126 | expcom 415 |
. . . . . . . . . . . 12
β’ (π β (0..^π) β (π β (((πβπ) β© (0..^π)) = ((πβπ) β© (0..^π)) β ((πβ(π + 1)) β© (0..^π)) = ((πβ(π + 1)) β© (0..^π))))) |
128 | 127 | a2d 29 |
. . . . . . . . . . 11
β’ (π β (0..^π) β ((π β ((πβπ) β© (0..^π)) = ((πβπ) β© (0..^π))) β (π β ((πβ(π + 1)) β© (0..^π)) = ((πβ(π + 1)) β© (0..^π))))) |
129 | 31, 37, 43, 49, 57, 128 | fzind2 13696 |
. . . . . . . . . 10
β’ (π β (0...π) β (π β ((πβπ) β© (0..^π)) = ((πβπ) β© (0..^π)))) |
130 | 25, 129 | mpcom 38 |
. . . . . . . . 9
β’ (π β ((πβπ) β© (0..^π)) = ((πβπ) β© (0..^π))) |
131 | 130 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β ((πβπ) β© (0..^π)) = ((πβπ) β© (0..^π))) |
132 | 131 | eleq2d 2820 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β (π β ((πβπ) β© (0..^π)) β π β ((πβπ) β© (0..^π)))) |
133 | | elin 3927 |
. . . . . . . . 9
β’ (π β ((πβπ) β© (0..^π)) β (π β (πβπ) β§ π β (0..^π))) |
134 | 133 | rbaib 540 |
. . . . . . . 8
β’ (π β (0..^π) β (π β ((πβπ) β© (0..^π)) β π β (πβπ))) |
135 | 134 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β (π β ((πβπ) β© (0..^π)) β π β (πβπ))) |
136 | | elin 3927 |
. . . . . . . . 9
β’ (π β ((πβπ) β© (0..^π)) β (π β (πβπ) β§ π β (0..^π))) |
137 | 136 | rbaib 540 |
. . . . . . . 8
β’ (π β (0..^π) β (π β ((πβπ) β© (0..^π)) β π β (πβπ))) |
138 | 137 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β (π β ((πβπ) β© (0..^π)) β π β (πβπ))) |
139 | 132, 135,
138 | 3bitr3d 309 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β (π β (πβπ) β π β (πβπ))) |
140 | 52 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (0..^π)) β (π΅ β© (0..^π)) β
β0) |
141 | 2, 140, 53, 13 | smupval 16373 |
. . . . . . 7
β’ ((π β§ π β (0..^π)) β (πβπ) = ((π΄ β© (0..^π)) smul (π΅ β© (0..^π)))) |
142 | 141 | eleq2d 2820 |
. . . . . 6
β’ ((π β§ π β (0..^π)) β (π β (πβπ) β π β ((π΄ β© (0..^π)) smul (π΅ β© (0..^π))))) |
143 | 22, 139, 142 | 3bitrd 305 |
. . . . 5
β’ ((π β§ π β (0..^π)) β (π β (π΄ smul π΅) β π β ((π΄ β© (0..^π)) smul (π΅ β© (0..^π))))) |
144 | 143 | ex 414 |
. . . 4
β’ (π β (π β (0..^π) β (π β (π΄ smul π΅) β π β ((π΄ β© (0..^π)) smul (π΅ β© (0..^π)))))) |
145 | 144 | pm5.32rd 579 |
. . 3
β’ (π β ((π β (π΄ smul π΅) β§ π β (0..^π)) β (π β ((π΄ β© (0..^π)) smul (π΅ β© (0..^π))) β§ π β (0..^π)))) |
146 | | elin 3927 |
. . 3
β’ (π β ((π΄ smul π΅) β© (0..^π)) β (π β (π΄ smul π΅) β§ π β (0..^π))) |
147 | | elin 3927 |
. . 3
β’ (π β (((π΄ β© (0..^π)) smul (π΅ β© (0..^π))) β© (0..^π)) β (π β ((π΄ β© (0..^π)) smul (π΅ β© (0..^π))) β§ π β (0..^π))) |
148 | 145, 146,
147 | 3bitr4g 314 |
. 2
β’ (π β (π β ((π΄ smul π΅) β© (0..^π)) β π β (((π΄ β© (0..^π)) smul (π΅ β© (0..^π))) β© (0..^π)))) |
149 | 148 | eqrdv 2731 |
1
β’ (π β ((π΄ smul π΅) β© (0..^π)) = (((π΄ β© (0..^π)) smul (π΅ β© (0..^π))) β© (0..^π))) |