Step | Hyp | Ref
| Expression |
1 | | ovnsubadd2lem.x |
. . 3
β’ (π β π β Fin) |
2 | | iftrue 4497 |
. . . . . . . 8
β’ (π = 1 β if(π = 1, π΄, if(π = 2, π΅, β
)) = π΄) |
3 | 2 | adantl 483 |
. . . . . . 7
β’ ((π β§ π = 1) β if(π = 1, π΄, if(π = 2, π΅, β
)) = π΄) |
4 | | ovexd 7397 |
. . . . . . . . . 10
β’ (π β (β
βm π)
β V) |
5 | | ovnsubadd2lem.a |
. . . . . . . . . 10
β’ (π β π΄ β (β βm π)) |
6 | 4, 5 | ssexd 5286 |
. . . . . . . . 9
β’ (π β π΄ β V) |
7 | 6, 5 | elpwd 4571 |
. . . . . . . 8
β’ (π β π΄ β π« (β
βm π)) |
8 | 7 | adantr 482 |
. . . . . . 7
β’ ((π β§ π = 1) β π΄ β π« (β
βm π)) |
9 | 3, 8 | eqeltrd 2838 |
. . . . . 6
β’ ((π β§ π = 1) β if(π = 1, π΄, if(π = 2, π΅, β
)) β π« (β
βm π)) |
10 | 9 | adantlr 714 |
. . . . 5
β’ (((π β§ π β β) β§ π = 1) β if(π = 1, π΄, if(π = 2, π΅, β
)) β π« (β
βm π)) |
11 | | simpl 484 |
. . . . . . . . . . 11
β’ ((Β¬
π = 1 β§ π = 2) β Β¬ π = 1) |
12 | 11 | iffalsed 4502 |
. . . . . . . . . 10
β’ ((Β¬
π = 1 β§ π = 2) β if(π = 1, π΄, if(π = 2, π΅, β
)) = if(π = 2, π΅, β
)) |
13 | | simpr 486 |
. . . . . . . . . . 11
β’ ((Β¬
π = 1 β§ π = 2) β π = 2) |
14 | 13 | iftrued 4499 |
. . . . . . . . . 10
β’ ((Β¬
π = 1 β§ π = 2) β if(π = 2, π΅, β
) = π΅) |
15 | 12, 14 | eqtrd 2777 |
. . . . . . . . 9
β’ ((Β¬
π = 1 β§ π = 2) β if(π = 1, π΄, if(π = 2, π΅, β
)) = π΅) |
16 | 15 | adantll 713 |
. . . . . . . 8
β’ (((π β§ Β¬ π = 1) β§ π = 2) β if(π = 1, π΄, if(π = 2, π΅, β
)) = π΅) |
17 | | ovnsubadd2lem.b |
. . . . . . . . . . 11
β’ (π β π΅ β (β βm π)) |
18 | 4, 17 | ssexd 5286 |
. . . . . . . . . 10
β’ (π β π΅ β V) |
19 | 18, 17 | elpwd 4571 |
. . . . . . . . 9
β’ (π β π΅ β π« (β
βm π)) |
20 | 19 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ Β¬ π = 1) β§ π = 2) β π΅ β π« (β
βm π)) |
21 | 16, 20 | eqeltrd 2838 |
. . . . . . 7
β’ (((π β§ Β¬ π = 1) β§ π = 2) β if(π = 1, π΄, if(π = 2, π΅, β
)) β π« (β
βm π)) |
22 | 21 | adantllr 718 |
. . . . . 6
β’ ((((π β§ π β β) β§ Β¬ π = 1) β§ π = 2) β if(π = 1, π΄, if(π = 2, π΅, β
)) β π« (β
βm π)) |
23 | | simpl 484 |
. . . . . . . . . 10
β’ ((Β¬
π = 1 β§ Β¬ π = 2) β Β¬ π = 1) |
24 | 23 | iffalsed 4502 |
. . . . . . . . 9
β’ ((Β¬
π = 1 β§ Β¬ π = 2) β if(π = 1, π΄, if(π = 2, π΅, β
)) = if(π = 2, π΅, β
)) |
25 | | simpr 486 |
. . . . . . . . . 10
β’ ((Β¬
π = 1 β§ Β¬ π = 2) β Β¬ π = 2) |
26 | 25 | iffalsed 4502 |
. . . . . . . . 9
β’ ((Β¬
π = 1 β§ Β¬ π = 2) β if(π = 2, π΅, β
) = β
) |
27 | 24, 26 | eqtrd 2777 |
. . . . . . . 8
β’ ((Β¬
π = 1 β§ Β¬ π = 2) β if(π = 1, π΄, if(π = 2, π΅, β
)) = β
) |
28 | | 0elpw 5316 |
. . . . . . . . 9
β’ β
β π« (β βm π) |
29 | 28 | a1i 11 |
. . . . . . . 8
β’ ((Β¬
π = 1 β§ Β¬ π = 2) β β
β
π« (β βm π)) |
30 | 27, 29 | eqeltrd 2838 |
. . . . . . 7
β’ ((Β¬
π = 1 β§ Β¬ π = 2) β if(π = 1, π΄, if(π = 2, π΅, β
)) β π« (β
βm π)) |
31 | 30 | adantll 713 |
. . . . . 6
β’ ((((π β§ π β β) β§ Β¬ π = 1) β§ Β¬ π = 2) β if(π = 1, π΄, if(π = 2, π΅, β
)) β π« (β
βm π)) |
32 | 22, 31 | pm2.61dan 812 |
. . . . 5
β’ (((π β§ π β β) β§ Β¬ π = 1) β if(π = 1, π΄, if(π = 2, π΅, β
)) β π« (β
βm π)) |
33 | 10, 32 | pm2.61dan 812 |
. . . 4
β’ ((π β§ π β β) β if(π = 1, π΄, if(π = 2, π΅, β
)) β π« (β
βm π)) |
34 | | ovnsubadd2lem.c |
. . . 4
β’ πΆ = (π β β β¦ if(π = 1, π΄, if(π = 2, π΅, β
))) |
35 | 33, 34 | fmptd 7067 |
. . 3
β’ (π β πΆ:ββΆπ« (β
βm π)) |
36 | 1, 35 | ovnsubadd 44887 |
. 2
β’ (π β ((voln*βπ)ββͺ π β β (πΆβπ)) β€
(Ξ£^β(π β β β¦ ((voln*βπ)β(πΆβπ))))) |
37 | | eldifi 4091 |
. . . . . . . . . . 11
β’ (π β (β β {1, 2})
β π β
β) |
38 | 37 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β (β β {1, 2})) β
π β
β) |
39 | | eldifn 4092 |
. . . . . . . . . . . . . 14
β’ (π β (β β {1, 2})
β Β¬ π β {1,
2}) |
40 | | vex 3452 |
. . . . . . . . . . . . . . . . 17
β’ π β V |
41 | 40 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
π β {1, 2} β
π β
V) |
42 | | id 22 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
π β {1, 2} β
Β¬ π β {1,
2}) |
43 | 41, 42 | nelpr1 4619 |
. . . . . . . . . . . . . . 15
β’ (Β¬
π β {1, 2} β
π β 1) |
44 | 43 | neneqd 2949 |
. . . . . . . . . . . . . 14
β’ (Β¬
π β {1, 2} β
Β¬ π =
1) |
45 | 39, 44 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (β β {1, 2})
β Β¬ π =
1) |
46 | 41, 42 | nelpr2 4618 |
. . . . . . . . . . . . . . 15
β’ (Β¬
π β {1, 2} β
π β 2) |
47 | 46 | neneqd 2949 |
. . . . . . . . . . . . . 14
β’ (Β¬
π β {1, 2} β
Β¬ π =
2) |
48 | 39, 47 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (β β {1, 2})
β Β¬ π =
2) |
49 | 45, 48, 27 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (β β {1, 2})
β if(π = 1, π΄, if(π = 2, π΅, β
)) = β
) |
50 | | 0ex 5269 |
. . . . . . . . . . . . 13
β’ β
β V |
51 | 50 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (β β {1, 2})
β β
β V) |
52 | 49, 51 | eqeltrd 2838 |
. . . . . . . . . . 11
β’ (π β (β β {1, 2})
β if(π = 1, π΄, if(π = 2, π΅, β
)) β V) |
53 | 52 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β (β β {1, 2})) β
if(π = 1, π΄, if(π = 2, π΅, β
)) β V) |
54 | 34 | fvmpt2 6964 |
. . . . . . . . . 10
β’ ((π β β β§ if(π = 1, π΄, if(π = 2, π΅, β
)) β V) β (πΆβπ) = if(π = 1, π΄, if(π = 2, π΅, β
))) |
55 | 38, 53, 54 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ π β (β β {1, 2})) β
(πΆβπ) = if(π = 1, π΄, if(π = 2, π΅, β
))) |
56 | 49 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β (β β {1, 2})) β
if(π = 1, π΄, if(π = 2, π΅, β
)) = β
) |
57 | 55, 56 | eqtrd 2777 |
. . . . . . . 8
β’ ((π β§ π β (β β {1, 2})) β
(πΆβπ) = β
) |
58 | 57 | ralrimiva 3144 |
. . . . . . 7
β’ (π β βπ β (β β {1, 2})(πΆβπ) = β
) |
59 | | nfcv 2908 |
. . . . . . . 8
β’
β²π(β β {1, 2}) |
60 | 59 | iunxdif3 5060 |
. . . . . . 7
β’
(βπ β
(β β {1, 2})(πΆβπ) = β
β βͺ π β (β β (β β {1,
2}))(πΆβπ) = βͺ π β β (πΆβπ)) |
61 | 58, 60 | syl 17 |
. . . . . 6
β’ (π β βͺ π β (β β (β β {1,
2}))(πΆβπ) = βͺ π β β (πΆβπ)) |
62 | 61 | eqcomd 2743 |
. . . . 5
β’ (π β βͺ π β β (πΆβπ) = βͺ π β (β β
(β β {1, 2}))(πΆβπ)) |
63 | | 1nn 12171 |
. . . . . . . . . 10
β’ 1 β
β |
64 | | 2nn 12233 |
. . . . . . . . . 10
β’ 2 β
β |
65 | 63, 64 | pm3.2i 472 |
. . . . . . . . 9
β’ (1 β
β β§ 2 β β) |
66 | | prssi 4786 |
. . . . . . . . 9
β’ ((1
β β β§ 2 β β) β {1, 2} β
β) |
67 | 65, 66 | ax-mp 5 |
. . . . . . . 8
β’ {1, 2}
β β |
68 | | dfss4 4223 |
. . . . . . . 8
β’ ({1, 2}
β β β (β β (β β {1, 2})) = {1,
2}) |
69 | 67, 68 | mpbi 229 |
. . . . . . 7
β’ (β
β (β β {1, 2})) = {1, 2} |
70 | | iuneq1 4975 |
. . . . . . 7
β’ ((β
β (β β {1, 2})) = {1, 2} β βͺ π β (β β (β β {1,
2}))(πΆβπ) = βͺ π β {1, 2} (πΆβπ)) |
71 | 69, 70 | ax-mp 5 |
. . . . . 6
β’ βͺ π β (β β (β β {1,
2}))(πΆβπ) = βͺ π β {1, 2} (πΆβπ) |
72 | 71 | a1i 11 |
. . . . 5
β’ (π β βͺ π β (β β (β β {1,
2}))(πΆβπ) = βͺ π β {1, 2} (πΆβπ)) |
73 | | fveq2 6847 |
. . . . . . . . 9
β’ (π = 1 β (πΆβπ) = (πΆβ1)) |
74 | | fveq2 6847 |
. . . . . . . . 9
β’ (π = 2 β (πΆβπ) = (πΆβ2)) |
75 | 73, 74 | iunxprg 5061 |
. . . . . . . 8
β’ ((1
β β β§ 2 β β) β βͺ π β {1, 2} (πΆβπ) = ((πΆβ1) βͺ (πΆβ2))) |
76 | 63, 64, 75 | mp2an 691 |
. . . . . . 7
β’ βͺ π β {1, 2} (πΆβπ) = ((πΆβ1) βͺ (πΆβ2)) |
77 | 76 | a1i 11 |
. . . . . 6
β’ (π β βͺ π β {1, 2} (πΆβπ) = ((πΆβ1) βͺ (πΆβ2))) |
78 | 63 | a1i 11 |
. . . . . . . 8
β’ (π β 1 β
β) |
79 | 34, 2, 78, 6 | fvmptd3 6976 |
. . . . . . 7
β’ (π β (πΆβ1) = π΄) |
80 | | id 22 |
. . . . . . . . . . . 12
β’ (π = 2 β π = 2) |
81 | | 1ne2 12368 |
. . . . . . . . . . . . . 14
β’ 1 β
2 |
82 | 81 | necomi 2999 |
. . . . . . . . . . . . 13
β’ 2 β
1 |
83 | 82 | a1i 11 |
. . . . . . . . . . . 12
β’ (π = 2 β 2 β
1) |
84 | 80, 83 | eqnetrd 3012 |
. . . . . . . . . . 11
β’ (π = 2 β π β 1) |
85 | 84 | neneqd 2949 |
. . . . . . . . . 10
β’ (π = 2 β Β¬ π = 1) |
86 | 85 | iffalsed 4502 |
. . . . . . . . 9
β’ (π = 2 β if(π = 1, π΄, if(π = 2, π΅, β
)) = if(π = 2, π΅, β
)) |
87 | | iftrue 4497 |
. . . . . . . . 9
β’ (π = 2 β if(π = 2, π΅, β
) = π΅) |
88 | 86, 87 | eqtrd 2777 |
. . . . . . . 8
β’ (π = 2 β if(π = 1, π΄, if(π = 2, π΅, β
)) = π΅) |
89 | 64 | a1i 11 |
. . . . . . . 8
β’ (π β 2 β
β) |
90 | 34, 88, 89, 18 | fvmptd3 6976 |
. . . . . . 7
β’ (π β (πΆβ2) = π΅) |
91 | 79, 90 | uneq12d 4129 |
. . . . . 6
β’ (π β ((πΆβ1) βͺ (πΆβ2)) = (π΄ βͺ π΅)) |
92 | | eqidd 2738 |
. . . . . 6
β’ (π β (π΄ βͺ π΅) = (π΄ βͺ π΅)) |
93 | 77, 91, 92 | 3eqtrd 2781 |
. . . . 5
β’ (π β βͺ π β {1, 2} (πΆβπ) = (π΄ βͺ π΅)) |
94 | 62, 72, 93 | 3eqtrd 2781 |
. . . 4
β’ (π β βͺ π β β (πΆβπ) = (π΄ βͺ π΅)) |
95 | 94 | fveq2d 6851 |
. . 3
β’ (π β ((voln*βπ)ββͺ π β β (πΆβπ)) = ((voln*βπ)β(π΄ βͺ π΅))) |
96 | | nfv 1918 |
. . . . . 6
β’
β²ππ |
97 | | nnex 12166 |
. . . . . . 7
β’ β
β V |
98 | 97 | a1i 11 |
. . . . . 6
β’ (π β β β
V) |
99 | 67 | a1i 11 |
. . . . . 6
β’ (π β {1, 2} β
β) |
100 | 1 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β {1, 2}) β π β Fin) |
101 | | simpl 484 |
. . . . . . . 8
β’ ((π β§ π β {1, 2}) β π) |
102 | 99 | sselda 3949 |
. . . . . . . 8
β’ ((π β§ π β {1, 2}) β π β β) |
103 | 35 | ffvelcdmda 7040 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πΆβπ) β π« (β
βm π)) |
104 | | elpwi 4572 |
. . . . . . . . 9
β’ ((πΆβπ) β π« (β
βm π)
β (πΆβπ) β (β
βm π)) |
105 | 103, 104 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β β) β (πΆβπ) β (β βm π)) |
106 | 101, 102,
105 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π β {1, 2}) β (πΆβπ) β (β βm π)) |
107 | 100, 106 | ovncl 44882 |
. . . . . 6
β’ ((π β§ π β {1, 2}) β ((voln*βπ)β(πΆβπ)) β (0[,]+β)) |
108 | 57 | fveq2d 6851 |
. . . . . . 7
β’ ((π β§ π β (β β {1, 2})) β
((voln*βπ)β(πΆβπ)) = ((voln*βπ)ββ
)) |
109 | 1 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β (β β {1, 2})) β
π β
Fin) |
110 | 109 | ovn0 44881 |
. . . . . . 7
β’ ((π β§ π β (β β {1, 2})) β
((voln*βπ)ββ
) = 0) |
111 | 108, 110 | eqtrd 2777 |
. . . . . 6
β’ ((π β§ π β (β β {1, 2})) β
((voln*βπ)β(πΆβπ)) = 0) |
112 | 96, 98, 99, 107, 111 | sge0ss 44727 |
. . . . 5
β’ (π β
(Ξ£^β(π β {1, 2} β¦ ((voln*βπ)β(πΆβπ)))) =
(Ξ£^β(π β β β¦ ((voln*βπ)β(πΆβπ))))) |
113 | 112 | eqcomd 2743 |
. . . 4
β’ (π β
(Ξ£^β(π β β β¦ ((voln*βπ)β(πΆβπ)))) =
(Ξ£^β(π β {1, 2} β¦ ((voln*βπ)β(πΆβπ))))) |
114 | 79, 5 | eqsstrd 3987 |
. . . . . 6
β’ (π β (πΆβ1) β (β
βm π)) |
115 | 1, 114 | ovncl 44882 |
. . . . 5
β’ (π β ((voln*βπ)β(πΆβ1)) β
(0[,]+β)) |
116 | 90, 17 | eqsstrd 3987 |
. . . . . 6
β’ (π β (πΆβ2) β (β
βm π)) |
117 | 1, 116 | ovncl 44882 |
. . . . 5
β’ (π β ((voln*βπ)β(πΆβ2)) β
(0[,]+β)) |
118 | | 2fveq3 6852 |
. . . . 5
β’ (π = 1 β ((voln*βπ)β(πΆβπ)) = ((voln*βπ)β(πΆβ1))) |
119 | | 2fveq3 6852 |
. . . . 5
β’ (π = 2 β ((voln*βπ)β(πΆβπ)) = ((voln*βπ)β(πΆβ2))) |
120 | 81 | a1i 11 |
. . . . 5
β’ (π β 1 β 2) |
121 | 78, 89, 115, 117, 118, 119, 120 | sge0pr 44709 |
. . . 4
β’ (π β
(Ξ£^β(π β {1, 2} β¦ ((voln*βπ)β(πΆβπ)))) = (((voln*βπ)β(πΆβ1)) +π
((voln*βπ)β(πΆβ2)))) |
122 | 79 | fveq2d 6851 |
. . . . 5
β’ (π β ((voln*βπ)β(πΆβ1)) = ((voln*βπ)βπ΄)) |
123 | 90 | fveq2d 6851 |
. . . . 5
β’ (π β ((voln*βπ)β(πΆβ2)) = ((voln*βπ)βπ΅)) |
124 | 122, 123 | oveq12d 7380 |
. . . 4
β’ (π β (((voln*βπ)β(πΆβ1)) +π
((voln*βπ)β(πΆβ2))) = (((voln*βπ)βπ΄) +π ((voln*βπ)βπ΅))) |
125 | 113, 121,
124 | 3eqtrd 2781 |
. . 3
β’ (π β
(Ξ£^β(π β β β¦ ((voln*βπ)β(πΆβπ)))) = (((voln*βπ)βπ΄) +π ((voln*βπ)βπ΅))) |
126 | 95, 125 | breq12d 5123 |
. 2
β’ (π β (((voln*βπ)ββͺ π β β (πΆβπ)) β€
(Ξ£^β(π β β β¦ ((voln*βπ)β(πΆβπ)))) β ((voln*βπ)β(π΄ βͺ π΅)) β€ (((voln*βπ)βπ΄) +π ((voln*βπ)βπ΅)))) |
127 | 36, 126 | mpbid 231 |
1
β’ (π β ((voln*βπ)β(π΄ βͺ π΅)) β€ (((voln*βπ)βπ΄) +π ((voln*βπ)βπ΅))) |