Step | Hyp | Ref
| Expression |
1 | | smfmullem4.x |
. . . . 5
β’
β²π₯π |
2 | | smfmullem4.r |
. . . . . . . . . 10
β’ (π β π
β β) |
3 | 2 | 3ad2ant1 1133 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄ β© πΆ) β§ (π΅ Β· π·) < π
) β π
β β) |
4 | | smfmullem4.k |
. . . . . . . . 9
β’ πΎ = {π β (β βm (0...3))
β£ βπ’ β
((πβ0)(,)(πβ1))βπ£ β ((πβ2)(,)(πβ3))(π’ Β· π£) < π
} |
5 | | inss1 4228 |
. . . . . . . . . . . . 13
β’ (π΄ β© πΆ) β π΄ |
6 | 5 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (π΄ β© πΆ) β π΄) |
7 | 6 | sselda 3982 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (π΄ β© πΆ)) β π₯ β π΄) |
8 | | smfmullem4.b |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β π΅ β β) |
9 | 7, 8 | syldan 591 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄ β© πΆ)) β π΅ β β) |
10 | 9 | 3adant3 1132 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄ β© πΆ) β§ (π΅ Β· π·) < π
) β π΅ β β) |
11 | | elinel2 4196 |
. . . . . . . . . . . 12
β’ (π₯ β (π΄ β© πΆ) β π₯ β πΆ) |
12 | 11 | adantl 482 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (π΄ β© πΆ)) β π₯ β πΆ) |
13 | | smfmullem4.d |
. . . . . . . . . . 11
β’ ((π β§ π₯ β πΆ) β π· β β) |
14 | 12, 13 | syldan 591 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (π΄ β© πΆ)) β π· β β) |
15 | 14 | 3adant3 1132 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄ β© πΆ) β§ (π΅ Β· π·) < π
) β π· β β) |
16 | | simp3 1138 |
. . . . . . . . 9
β’ ((π β§ π₯ β (π΄ β© πΆ) β§ (π΅ Β· π·) < π
) β (π΅ Β· π·) < π
) |
17 | | eqid 2732 |
. . . . . . . . 9
β’ ((π
β (π΅ Β· π·)) / (1 + ((absβπ΅) + (absβπ·)))) = ((π
β (π΅ Β· π·)) / (1 + ((absβπ΅) + (absβπ·)))) |
18 | | eqid 2732 |
. . . . . . . . 9
β’ if(1 β€
((π
β (π΅ Β· π·)) / (1 + ((absβπ΅) + (absβπ·)))), 1, ((π
β (π΅ Β· π·)) / (1 + ((absβπ΅) + (absβπ·))))) = if(1 β€ ((π
β (π΅ Β· π·)) / (1 + ((absβπ΅) + (absβπ·)))), 1, ((π
β (π΅ Β· π·)) / (1 + ((absβπ΅) + (absβπ·))))) |
19 | 3, 4, 10, 15, 16, 17, 18 | smfmullem3 45588 |
. . . . . . . 8
β’ ((π β§ π₯ β (π΄ β© πΆ) β§ (π΅ Β· π·) < π
) β βπ β πΎ (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3)))) |
20 | | rabid 3452 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β {π₯ β (π΄ β© πΆ) β£ (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3)))} β (π₯ β (π΄ β© πΆ) β§ (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3))))) |
21 | 20 | bicomi 223 |
. . . . . . . . . . . . . . 15
β’ ((π₯ β (π΄ β© πΆ) β§ (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3)))) β π₯ β {π₯ β (π΄ β© πΆ) β£ (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3)))}) |
22 | 21 | biimpi 215 |
. . . . . . . . . . . . . 14
β’ ((π₯ β (π΄ β© πΆ) β§ (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3)))) β π₯ β {π₯ β (π΄ β© πΆ) β£ (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3)))}) |
23 | 22 | adantll 712 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β (π΄ β© πΆ)) β§ (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3)))) β π₯ β {π₯ β (π΄ β© πΆ) β£ (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3)))}) |
24 | 23 | adantlr 713 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β (π΄ β© πΆ)) β§ π β πΎ) β§ (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3)))) β π₯ β {π₯ β (π΄ β© πΆ) β£ (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3)))}) |
25 | | smfmullem4.e |
. . . . . . . . . . . . . . . . 17
β’ πΈ = (π β πΎ β¦ {π₯ β (π΄ β© πΆ) β£ (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3)))}) |
26 | 25 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π β πΈ = (π β πΎ β¦ {π₯ β (π΄ β© πΆ) β£ (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3)))})) |
27 | | inrab 4306 |
. . . . . . . . . . . . . . . . . 18
β’ ({π₯ β (π΄ β© πΆ) β£ π΅ β ((πβ0)(,)(πβ1))} β© {π₯ β (π΄ β© πΆ) β£ π· β ((πβ2)(,)(πβ3))}) = {π₯ β (π΄ β© πΆ) β£ (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3)))} |
28 | | smfmullem4.s |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π β SAlg) |
29 | | smfmullem4.a |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π΄ β π) |
30 | 29, 6 | ssexd 5324 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π΄ β© πΆ) β V) |
31 | | eqid 2732 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π βΎt (π΄ β© πΆ)) = (π βΎt (π΄ β© πΆ)) |
32 | 28, 30, 31 | subsalsal 45154 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π βΎt (π΄ β© πΆ)) β SAlg) |
33 | 32 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β πΎ) β (π βΎt (π΄ β© πΆ)) β SAlg) |
34 | | nfv 1917 |
. . . . . . . . . . . . . . . . . . . . 21
β’
β²π₯ π β πΎ |
35 | 1, 34 | nfan 1902 |
. . . . . . . . . . . . . . . . . . . 20
β’
β²π₯(π β§ π β πΎ) |
36 | 28 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β πΎ) β π β SAlg) |
37 | 30 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β πΎ) β (π΄ β© πΆ) β V) |
38 | 9 | adantlr 713 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β πΎ) β§ π₯ β (π΄ β© πΆ)) β π΅ β β) |
39 | | smfmullem4.m |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π₯ β π΄ β¦ π΅) β (SMblFnβπ)) |
40 | 28, 39, 6 | sssmfmpt 45545 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π₯ β (π΄ β© πΆ) β¦ π΅) β (SMblFnβπ)) |
41 | 40 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β πΎ) β (π₯ β (π΄ β© πΆ) β¦ π΅) β (SMblFnβπ)) |
42 | | ssrab2 4077 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ {π β (β
βm (0...3)) β£ βπ’ β ((πβ0)(,)(πβ1))βπ£ β ((πβ2)(,)(πβ3))(π’ Β· π£) < π
} β (β βm
(0...3)) |
43 | 4, 42 | eqsstri 4016 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ πΎ β (β
βm (0...3)) |
44 | | reex 11203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ β
β V |
45 | | qssre 12945 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ β
β β |
46 | | mapss 8885 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((β
β V β§ β β β) β (β βm
(0...3)) β (β βm (0...3))) |
47 | 44, 45, 46 | mp2an 690 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (β
βm (0...3)) β (β βm
(0...3)) |
48 | 43, 47 | sstri 3991 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ πΎ β (β
βm (0...3)) |
49 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β πΎ β π β πΎ) |
50 | 48, 49 | sselid 3980 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β πΎ β π β (β βm
(0...3))) |
51 | 44 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β πΎ β β β V) |
52 | | ovexd 7446 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β πΎ β (0...3) β V) |
53 | 51, 52 | elmapd 8836 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β πΎ β (π β (β βm (0...3))
β π:(0...3)βΆβ)) |
54 | 50, 53 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β πΎ β π:(0...3)βΆβ) |
55 | | 0z 12571 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ 0 β
β€ |
56 | | 3z 12597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ 3 β
β€ |
57 | | 0re 11218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ 0 β
β |
58 | | 3re 12294 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ 3 β
β |
59 | | 3pos 12319 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ 0 <
3 |
60 | 57, 58, 59 | ltleii 11339 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ 0 β€
3 |
61 | 55, 56, 60 | 3pm3.2i 1339 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (0 β
β€ β§ 3 β β€ β§ 0 β€ 3) |
62 | | eluz2 12830 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (3 β
(β€β₯β0) β (0 β β€ β§ 3 β
β€ β§ 0 β€ 3)) |
63 | 61, 62 | mpbir 230 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ 3 β
(β€β₯β0) |
64 | | eluzfz1 13510 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (3 β
(β€β₯β0) β 0 β (0...3)) |
65 | 63, 64 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ 0 β
(0...3) |
66 | 65 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β πΎ β 0 β (0...3)) |
67 | 54, 66 | ffvelcdmd 7087 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β πΎ β (πβ0) β β) |
68 | 67 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β πΎ) β (πβ0) β β) |
69 | 68 | rexrd 11266 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β πΎ) β (πβ0) β
β*) |
70 | | 0le1 11739 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ 0 β€
1 |
71 | | 1re 11216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ 1 β
β |
72 | | 1lt3 12387 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ 1 <
3 |
73 | 71, 58, 72 | ltleii 11339 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ 1 β€
3 |
74 | 70, 73 | pm3.2i 471 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (0 β€ 1
β§ 1 β€ 3) |
75 | | 1z 12594 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ 1 β
β€ |
76 | | elfz 13492 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((1
β β€ β§ 0 β β€ β§ 3 β β€) β (1 β
(0...3) β (0 β€ 1 β§ 1 β€ 3))) |
77 | 75, 55, 56, 76 | mp3an 1461 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (1 β
(0...3) β (0 β€ 1 β§ 1 β€ 3)) |
78 | 74, 77 | mpbir 230 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ 1 β
(0...3) |
79 | 78 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β πΎ β 1 β (0...3)) |
80 | 54, 79 | ffvelcdmd 7087 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β πΎ β (πβ1) β β) |
81 | 80 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β πΎ) β (πβ1) β β) |
82 | 81 | rexrd 11266 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β πΎ) β (πβ1) β
β*) |
83 | 35, 36, 37, 38, 41, 69, 82 | smfpimioompt 45581 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β πΎ) β {π₯ β (π΄ β© πΆ) β£ π΅ β ((πβ0)(,)(πβ1))} β (π βΎt (π΄ β© πΆ))) |
84 | 14 | adantlr 713 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β πΎ) β§ π₯ β (π΄ β© πΆ)) β π· β β) |
85 | | smfmullem4.n |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π₯ β πΆ β¦ π·) β (SMblFnβπ)) |
86 | 1, 12 | ssdf 43846 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π΄ β© πΆ) β πΆ) |
87 | 28, 85, 86 | sssmfmpt 45545 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π₯ β (π΄ β© πΆ) β¦ π·) β (SMblFnβπ)) |
88 | 87 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β πΎ) β (π₯ β (π΄ β© πΆ) β¦ π·) β (SMblFnβπ)) |
89 | | 0le2 12316 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ 0 β€
2 |
90 | | 2re 12288 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ 2 β
β |
91 | | 2lt3 12386 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ 2 <
3 |
92 | 90, 58, 91 | ltleii 11339 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ 2 β€
3 |
93 | 89, 92 | pm3.2i 471 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (0 β€ 2
β§ 2 β€ 3) |
94 | | 2z 12596 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ 2 β
β€ |
95 | | elfz 13492 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((2
β β€ β§ 0 β β€ β§ 3 β β€) β (2 β
(0...3) β (0 β€ 2 β§ 2 β€ 3))) |
96 | 94, 55, 56, 95 | mp3an 1461 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (2 β
(0...3) β (0 β€ 2 β§ 2 β€ 3)) |
97 | 93, 96 | mpbir 230 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ 2 β
(0...3) |
98 | 97 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β πΎ β 2 β (0...3)) |
99 | 54, 98 | ffvelcdmd 7087 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β πΎ β (πβ2) β β) |
100 | 99 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β πΎ) β (πβ2) β β) |
101 | 100 | rexrd 11266 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β πΎ) β (πβ2) β
β*) |
102 | | eluzfz2 13511 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (3 β
(β€β₯β0) β 3 β (0...3)) |
103 | 63, 102 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ 3 β
(0...3) |
104 | 103 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β πΎ β 3 β (0...3)) |
105 | 54, 104 | ffvelcdmd 7087 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β πΎ β (πβ3) β β) |
106 | 105 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β πΎ) β (πβ3) β β) |
107 | 106 | rexrd 11266 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β πΎ) β (πβ3) β
β*) |
108 | 35, 36, 37, 84, 88, 101, 107 | smfpimioompt 45581 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β πΎ) β {π₯ β (π΄ β© πΆ) β£ π· β ((πβ2)(,)(πβ3))} β (π βΎt (π΄ β© πΆ))) |
109 | 33, 83, 108 | salincld 45147 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β πΎ) β ({π₯ β (π΄ β© πΆ) β£ π΅ β ((πβ0)(,)(πβ1))} β© {π₯ β (π΄ β© πΆ) β£ π· β ((πβ2)(,)(πβ3))}) β (π βΎt (π΄ β© πΆ))) |
110 | 27, 109 | eqeltrrid 2838 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β πΎ) β {π₯ β (π΄ β© πΆ) β£ (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3)))} β (π βΎt (π΄ β© πΆ))) |
111 | 110 | elexd 3494 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β πΎ) β {π₯ β (π΄ β© πΆ) β£ (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3)))} β V) |
112 | 26, 111 | fvmpt2d 7011 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β πΎ) β (πΈβπ) = {π₯ β (π΄ β© πΆ) β£ (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3)))}) |
113 | 112 | eqcomd 2738 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β πΎ) β {π₯ β (π΄ β© πΆ) β£ (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3)))} = (πΈβπ)) |
114 | 113 | adantlr 713 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β (π΄ β© πΆ)) β§ π β πΎ) β {π₯ β (π΄ β© πΆ) β£ (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3)))} = (πΈβπ)) |
115 | 114 | adantr 481 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β (π΄ β© πΆ)) β§ π β πΎ) β§ (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3)))) β {π₯ β (π΄ β© πΆ) β£ (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3)))} = (πΈβπ)) |
116 | 24, 115 | eleqtrd 2835 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β (π΄ β© πΆ)) β§ π β πΎ) β§ (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3)))) β π₯ β (πΈβπ)) |
117 | 116 | ex 413 |
. . . . . . . . . 10
β’ (((π β§ π₯ β (π΄ β© πΆ)) β§ π β πΎ) β ((π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3))) β π₯ β (πΈβπ))) |
118 | 117 | 3adantl3 1168 |
. . . . . . . . 9
β’ (((π β§ π₯ β (π΄ β© πΆ) β§ (π΅ Β· π·) < π
) β§ π β πΎ) β ((π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3))) β π₯ β (πΈβπ))) |
119 | 118 | reximdva 3168 |
. . . . . . . 8
β’ ((π β§ π₯ β (π΄ β© πΆ) β§ (π΅ Β· π·) < π
) β (βπ β πΎ (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3))) β βπ β πΎ π₯ β (πΈβπ))) |
120 | 19, 119 | mpd 15 |
. . . . . . 7
β’ ((π β§ π₯ β (π΄ β© πΆ) β§ (π΅ Β· π·) < π
) β βπ β πΎ π₯ β (πΈβπ)) |
121 | | eliun 5001 |
. . . . . . 7
β’ (π₯ β βͺ π β πΎ (πΈβπ) β βπ β πΎ π₯ β (πΈβπ)) |
122 | 120, 121 | sylibr 233 |
. . . . . 6
β’ ((π β§ π₯ β (π΄ β© πΆ) β§ (π΅ Β· π·) < π
) β π₯ β βͺ
π β πΎ (πΈβπ)) |
123 | 122 | 3exp 1119 |
. . . . 5
β’ (π β (π₯ β (π΄ β© πΆ) β ((π΅ Β· π·) < π
β π₯ β βͺ
π β πΎ (πΈβπ)))) |
124 | 1, 123 | ralrimi 3254 |
. . . 4
β’ (π β βπ₯ β (π΄ β© πΆ)((π΅ Β· π·) < π
β π₯ β βͺ
π β πΎ (πΈβπ))) |
125 | 34 | nfci 2886 |
. . . . . 6
β’
β²π₯πΎ |
126 | | nfrab1 3451 |
. . . . . . . . 9
β’
β²π₯{π₯ β (π΄ β© πΆ) β£ (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3)))} |
127 | 125, 126 | nfmpt 5255 |
. . . . . . . 8
β’
β²π₯(π β πΎ β¦ {π₯ β (π΄ β© πΆ) β£ (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3)))}) |
128 | 25, 127 | nfcxfr 2901 |
. . . . . . 7
β’
β²π₯πΈ |
129 | | nfcv 2903 |
. . . . . . 7
β’
β²π₯π |
130 | 128, 129 | nffv 6901 |
. . . . . 6
β’
β²π₯(πΈβπ) |
131 | 125, 130 | nfiun 5027 |
. . . . 5
β’
β²π₯βͺ π β πΎ (πΈβπ) |
132 | 131 | rabssf 43890 |
. . . 4
β’ ({π₯ β (π΄ β© πΆ) β£ (π΅ Β· π·) < π
} β βͺ π β πΎ (πΈβπ) β βπ₯ β (π΄ β© πΆ)((π΅ Β· π·) < π
β π₯ β βͺ
π β πΎ (πΈβπ))) |
133 | 124, 132 | sylibr 233 |
. . 3
β’ (π β {π₯ β (π΄ β© πΆ) β£ (π΅ Β· π·) < π
} β βͺ π β πΎ (πΈβπ)) |
134 | | ssrab2 4077 |
. . . . . . 7
β’ {π₯ β (π΄ β© πΆ) β£ (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3)))} β (π΄ β© πΆ) |
135 | 112, 134 | eqsstrdi 4036 |
. . . . . 6
β’ ((π β§ π β πΎ) β (πΈβπ) β (π΄ β© πΆ)) |
136 | | simpr 485 |
. . . . . . . . . . . 12
β’ (((π β§ π β πΎ) β§ π₯ β (πΈβπ)) β π₯ β (πΈβπ)) |
137 | 112 | adantr 481 |
. . . . . . . . . . . 12
β’ (((π β§ π β πΎ) β§ π₯ β (πΈβπ)) β (πΈβπ) = {π₯ β (π΄ β© πΆ) β£ (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3)))}) |
138 | 136, 137 | eleqtrd 2835 |
. . . . . . . . . . 11
β’ (((π β§ π β πΎ) β§ π₯ β (πΈβπ)) β π₯ β {π₯ β (π΄ β© πΆ) β£ (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3)))}) |
139 | | rabidim2 43873 |
. . . . . . . . . . 11
β’ (π₯ β {π₯ β (π΄ β© πΆ) β£ (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3)))} β (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3)))) |
140 | 138, 139 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π β πΎ) β§ π₯ β (πΈβπ)) β (π΅ β ((πβ0)(,)(πβ1)) β§ π· β ((πβ2)(,)(πβ3)))) |
141 | 140 | simprd 496 |
. . . . . . . . 9
β’ (((π β§ π β πΎ) β§ π₯ β (πΈβπ)) β π· β ((πβ2)(,)(πβ3))) |
142 | 140 | simpld 495 |
. . . . . . . . . 10
β’ (((π β§ π β πΎ) β§ π₯ β (πΈβπ)) β π΅ β ((πβ0)(,)(πβ1))) |
143 | 49, 4 | eleqtrdi 2843 |
. . . . . . . . . . . 12
β’ (π β πΎ β π β {π β (β βm (0...3))
β£ βπ’ β
((πβ0)(,)(πβ1))βπ£ β ((πβ2)(,)(πβ3))(π’ Β· π£) < π
}) |
144 | | rabidim2 43873 |
. . . . . . . . . . . 12
β’ (π β {π β (β βm (0...3))
β£ βπ’ β
((πβ0)(,)(πβ1))βπ£ β ((πβ2)(,)(πβ3))(π’ Β· π£) < π
} β βπ’ β ((πβ0)(,)(πβ1))βπ£ β ((πβ2)(,)(πβ3))(π’ Β· π£) < π
) |
145 | 143, 144 | syl 17 |
. . . . . . . . . . 11
β’ (π β πΎ β βπ’ β ((πβ0)(,)(πβ1))βπ£ β ((πβ2)(,)(πβ3))(π’ Β· π£) < π
) |
146 | 145 | ad2antlr 725 |
. . . . . . . . . 10
β’ (((π β§ π β πΎ) β§ π₯ β (πΈβπ)) β βπ’ β ((πβ0)(,)(πβ1))βπ£ β ((πβ2)(,)(πβ3))(π’ Β· π£) < π
) |
147 | | oveq1 7418 |
. . . . . . . . . . . . 13
β’ (π’ = π΅ β (π’ Β· π£) = (π΅ Β· π£)) |
148 | 147 | breq1d 5158 |
. . . . . . . . . . . 12
β’ (π’ = π΅ β ((π’ Β· π£) < π
β (π΅ Β· π£) < π
)) |
149 | 148 | ralbidv 3177 |
. . . . . . . . . . 11
β’ (π’ = π΅ β (βπ£ β ((πβ2)(,)(πβ3))(π’ Β· π£) < π
β βπ£ β ((πβ2)(,)(πβ3))(π΅ Β· π£) < π
)) |
150 | 149 | rspcva 3610 |
. . . . . . . . . 10
β’ ((π΅ β ((πβ0)(,)(πβ1)) β§ βπ’ β ((πβ0)(,)(πβ1))βπ£ β ((πβ2)(,)(πβ3))(π’ Β· π£) < π
) β βπ£ β ((πβ2)(,)(πβ3))(π΅ Β· π£) < π
) |
151 | 142, 146,
150 | syl2anc 584 |
. . . . . . . . 9
β’ (((π β§ π β πΎ) β§ π₯ β (πΈβπ)) β βπ£ β ((πβ2)(,)(πβ3))(π΅ Β· π£) < π
) |
152 | | oveq2 7419 |
. . . . . . . . . . 11
β’ (π£ = π· β (π΅ Β· π£) = (π΅ Β· π·)) |
153 | 152 | breq1d 5158 |
. . . . . . . . . 10
β’ (π£ = π· β ((π΅ Β· π£) < π
β (π΅ Β· π·) < π
)) |
154 | 153 | rspcva 3610 |
. . . . . . . . 9
β’ ((π· β ((πβ2)(,)(πβ3)) β§ βπ£ β ((πβ2)(,)(πβ3))(π΅ Β· π£) < π
) β (π΅ Β· π·) < π
) |
155 | 141, 151,
154 | syl2anc 584 |
. . . . . . . 8
β’ (((π β§ π β πΎ) β§ π₯ β (πΈβπ)) β (π΅ Β· π·) < π
) |
156 | 155 | ex 413 |
. . . . . . 7
β’ ((π β§ π β πΎ) β (π₯ β (πΈβπ) β (π΅ Β· π·) < π
)) |
157 | 35, 156 | ralrimi 3254 |
. . . . . 6
β’ ((π β§ π β πΎ) β βπ₯ β (πΈβπ)(π΅ Β· π·) < π
) |
158 | 135, 157 | jca 512 |
. . . . 5
β’ ((π β§ π β πΎ) β ((πΈβπ) β (π΄ β© πΆ) β§ βπ₯ β (πΈβπ)(π΅ Β· π·) < π
)) |
159 | | nfcv 2903 |
. . . . . 6
β’
β²π₯(π΄ β© πΆ) |
160 | 130, 159 | ssrabf 43885 |
. . . . 5
β’ ((πΈβπ) β {π₯ β (π΄ β© πΆ) β£ (π΅ Β· π·) < π
} β ((πΈβπ) β (π΄ β© πΆ) β§ βπ₯ β (πΈβπ)(π΅ Β· π·) < π
)) |
161 | 158, 160 | sylibr 233 |
. . . 4
β’ ((π β§ π β πΎ) β (πΈβπ) β {π₯ β (π΄ β© πΆ) β£ (π΅ Β· π·) < π
}) |
162 | 161 | iunssd 5053 |
. . 3
β’ (π β βͺ π β πΎ (πΈβπ) β {π₯ β (π΄ β© πΆ) β£ (π΅ Β· π·) < π
}) |
163 | 133, 162 | eqssd 3999 |
. 2
β’ (π β {π₯ β (π΄ β© πΆ) β£ (π΅ Β· π·) < π
} = βͺ
π β πΎ (πΈβπ)) |
164 | | ovex 7444 |
. . . . . . 7
β’ (β
βm (0...3)) β V |
165 | | ssdomg 8998 |
. . . . . . 7
β’ ((β
βm (0...3)) β V β (πΎ β (β βm
(0...3)) β πΎ βΌ
(β βm (0...3)))) |
166 | 164, 165 | ax-mp 5 |
. . . . . 6
β’ (πΎ β (β
βm (0...3)) β πΎ βΌ (β βm
(0...3))) |
167 | 43, 166 | ax-mp 5 |
. . . . 5
β’ πΎ βΌ (β
βm (0...3)) |
168 | | qct 44151 |
. . . . . . . 8
β’ β
βΌ Ο |
169 | 168 | a1i 11 |
. . . . . . 7
β’ (β€
β β βΌ Ο) |
170 | | fzfid 13940 |
. . . . . . 7
β’ (β€
β (0...3) β Fin) |
171 | 169, 170 | mpct 43979 |
. . . . . 6
β’ (β€
β (β βm (0...3)) βΌ Ο) |
172 | 171 | mptru 1548 |
. . . . 5
β’ (β
βm (0...3)) βΌ Ο |
173 | | domtr 9005 |
. . . . 5
β’ ((πΎ βΌ (β
βm (0...3)) β§ (β βm (0...3)) βΌ
Ο) β πΎ βΌ
Ο) |
174 | 167, 172,
173 | mp2an 690 |
. . . 4
β’ πΎ βΌ
Ο |
175 | 174 | a1i 11 |
. . 3
β’ (π β πΎ βΌ Ο) |
176 | 110, 25 | fmptd 7115 |
. . . 4
β’ (π β πΈ:πΎβΆ(π βΎt (π΄ β© πΆ))) |
177 | 176 | ffvelcdmda 7086 |
. . 3
β’ ((π β§ π β πΎ) β (πΈβπ) β (π βΎt (π΄ β© πΆ))) |
178 | 32, 175, 177 | saliuncl 45118 |
. 2
β’ (π β βͺ π β πΎ (πΈβπ) β (π βΎt (π΄ β© πΆ))) |
179 | 163, 178 | eqeltrd 2833 |
1
β’ (π β {π₯ β (π΄ β© πΆ) β£ (π΅ Β· π·) < π
} β (π βΎt (π΄ β© πΆ))) |