Step | Hyp | Ref
| Expression |
1 | | fvexd 6858 |
. . . . 5
β’ (π = π β (Baseβπ) β V) |
2 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π = π β§ π£ = (Baseβπ)) β π£ = (Baseβπ)) |
3 | | fveq2 6843 |
. . . . . . . . . . . 12
β’ (π = π β (Baseβπ) = (Baseβπ)) |
4 | 3 | adantr 482 |
. . . . . . . . . . 11
β’ ((π = π β§ π£ = (Baseβπ)) β (Baseβπ) = (Baseβπ)) |
5 | 2, 4 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((π = π β§ π£ = (Baseβπ)) β π£ = (Baseβπ)) |
6 | | isomnd.0 |
. . . . . . . . . 10
β’ π΅ = (Baseβπ) |
7 | 5, 6 | eqtr4di 2791 |
. . . . . . . . 9
β’ ((π = π β§ π£ = (Baseβπ)) β π£ = π΅) |
8 | | raleq 3308 |
. . . . . . . . . . 11
β’ (π£ = π΅ β (βπ β π£ (πππ β (πππ)π(πππ)) β βπ β π΅ (πππ β (πππ)π(πππ)))) |
9 | 8 | raleqbi1dv 3306 |
. . . . . . . . . 10
β’ (π£ = π΅ β (βπ β π£ βπ β π£ (πππ β (πππ)π(πππ)) β βπ β π΅ βπ β π΅ (πππ β (πππ)π(πππ)))) |
10 | 9 | raleqbi1dv 3306 |
. . . . . . . . 9
β’ (π£ = π΅ β (βπ β π£ βπ β π£ βπ β π£ (πππ β (πππ)π(πππ)) β βπ β π΅ βπ β π΅ βπ β π΅ (πππ β (πππ)π(πππ)))) |
11 | 7, 10 | syl 17 |
. . . . . . . 8
β’ ((π = π β§ π£ = (Baseβπ)) β (βπ β π£ βπ β π£ βπ β π£ (πππ β (πππ)π(πππ)) β βπ β π΅ βπ β π΅ βπ β π΅ (πππ β (πππ)π(πππ)))) |
12 | 11 | anbi2d 630 |
. . . . . . 7
β’ ((π = π β§ π£ = (Baseβπ)) β ((π β Toset β§ βπ β π£ βπ β π£ βπ β π£ (πππ β (πππ)π(πππ))) β (π β Toset β§ βπ β π΅ βπ β π΅ βπ β π΅ (πππ β (πππ)π(πππ))))) |
13 | 12 | sbcbidv 3799 |
. . . . . 6
β’ ((π = π β§ π£ = (Baseβπ)) β ([(leβπ) / π](π β Toset β§ βπ β π£ βπ β π£ βπ β π£ (πππ β (πππ)π(πππ))) β [(leβπ) / π](π β Toset β§ βπ β π΅ βπ β π΅ βπ β π΅ (πππ β (πππ)π(πππ))))) |
14 | 13 | sbcbidv 3799 |
. . . . 5
β’ ((π = π β§ π£ = (Baseβπ)) β ([(+gβπ) / π][(leβπ) / π](π β Toset β§ βπ β π£ βπ β π£ βπ β π£ (πππ β (πππ)π(πππ))) β [(+gβπ) / π][(leβπ) / π](π β Toset β§ βπ β π΅ βπ β π΅ βπ β π΅ (πππ β (πππ)π(πππ))))) |
15 | 1, 14 | sbcied 3785 |
. . . 4
β’ (π = π β ([(Baseβπ) / π£][(+gβπ) / π][(leβπ) / π](π β Toset β§ βπ β π£ βπ β π£ βπ β π£ (πππ β (πππ)π(πππ))) β [(+gβπ) / π][(leβπ) / π](π β Toset β§ βπ β π΅ βπ β π΅ βπ β π΅ (πππ β (πππ)π(πππ))))) |
16 | | fvexd 6858 |
. . . . 5
β’ (π = π β (+gβπ) β V) |
17 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π = π β§ π = (+gβπ)) β π = (+gβπ)) |
18 | | fveq2 6843 |
. . . . . . . . . . . . . . 15
β’ (π = π β (+gβπ) = (+gβπ)) |
19 | 18 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π = π β§ π = (+gβπ)) β (+gβπ) = (+gβπ)) |
20 | 17, 19 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ ((π = π β§ π = (+gβπ)) β π = (+gβπ)) |
21 | | isomnd.1 |
. . . . . . . . . . . . 13
β’ + =
(+gβπ) |
22 | 20, 21 | eqtr4di 2791 |
. . . . . . . . . . . 12
β’ ((π = π β§ π = (+gβπ)) β π = + ) |
23 | 22 | oveqd 7375 |
. . . . . . . . . . 11
β’ ((π = π β§ π = (+gβπ)) β (πππ) = (π + π)) |
24 | 22 | oveqd 7375 |
. . . . . . . . . . 11
β’ ((π = π β§ π = (+gβπ)) β (πππ) = (π + π)) |
25 | 23, 24 | breq12d 5119 |
. . . . . . . . . 10
β’ ((π = π β§ π = (+gβπ)) β ((πππ)π(πππ) β (π + π)π(π + π))) |
26 | 25 | imbi2d 341 |
. . . . . . . . 9
β’ ((π = π β§ π = (+gβπ)) β ((πππ β (πππ)π(πππ)) β (πππ β (π + π)π(π + π)))) |
27 | 26 | ralbidv 3171 |
. . . . . . . 8
β’ ((π = π β§ π = (+gβπ)) β (βπ β π΅ (πππ β (πππ)π(πππ)) β βπ β π΅ (πππ β (π + π)π(π + π)))) |
28 | 27 | 2ralbidv 3209 |
. . . . . . 7
β’ ((π = π β§ π = (+gβπ)) β (βπ β π΅ βπ β π΅ βπ β π΅ (πππ β (πππ)π(πππ)) β βπ β π΅ βπ β π΅ βπ β π΅ (πππ β (π + π)π(π + π)))) |
29 | 28 | anbi2d 630 |
. . . . . 6
β’ ((π = π β§ π = (+gβπ)) β ((π β Toset β§ βπ β π΅ βπ β π΅ βπ β π΅ (πππ β (πππ)π(πππ))) β (π β Toset β§ βπ β π΅ βπ β π΅ βπ β π΅ (πππ β (π + π)π(π + π))))) |
30 | 29 | sbcbidv 3799 |
. . . . 5
β’ ((π = π β§ π = (+gβπ)) β ([(leβπ) / π](π β Toset β§ βπ β π΅ βπ β π΅ βπ β π΅ (πππ β (πππ)π(πππ))) β [(leβπ) / π](π β Toset β§ βπ β π΅ βπ β π΅ βπ β π΅ (πππ β (π + π)π(π + π))))) |
31 | 16, 30 | sbcied 3785 |
. . . 4
β’ (π = π β ([(+gβπ) / π][(leβπ) / π](π β Toset β§ βπ β π΅ βπ β π΅ βπ β π΅ (πππ β (πππ)π(πππ))) β [(leβπ) / π](π β Toset β§ βπ β π΅ βπ β π΅ βπ β π΅ (πππ β (π + π)π(π + π))))) |
32 | | fvexd 6858 |
. . . . . 6
β’ (π = π β (leβπ) β V) |
33 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π = π β§ π = (leβπ)) β π = (leβπ)) |
34 | | simpl 484 |
. . . . . . . . . . . . . 14
β’ ((π = π β§ π = (leβπ)) β π = π) |
35 | 34 | fveq2d 6847 |
. . . . . . . . . . . . 13
β’ ((π = π β§ π = (leβπ)) β (leβπ) = (leβπ)) |
36 | 33, 35 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ ((π = π β§ π = (leβπ)) β π = (leβπ)) |
37 | | isomnd.2 |
. . . . . . . . . . . 12
β’ β€ =
(leβπ) |
38 | 36, 37 | eqtr4di 2791 |
. . . . . . . . . . 11
β’ ((π = π β§ π = (leβπ)) β π = β€ ) |
39 | 38 | breqd 5117 |
. . . . . . . . . 10
β’ ((π = π β§ π = (leβπ)) β (πππ β π β€ π)) |
40 | 38 | breqd 5117 |
. . . . . . . . . 10
β’ ((π = π β§ π = (leβπ)) β ((π + π)π(π + π) β (π + π) β€ (π + π))) |
41 | 39, 40 | imbi12d 345 |
. . . . . . . . 9
β’ ((π = π β§ π = (leβπ)) β ((πππ β (π + π)π(π + π)) β (π β€ π β (π + π) β€ (π + π)))) |
42 | 41 | ralbidv 3171 |
. . . . . . . 8
β’ ((π = π β§ π = (leβπ)) β (βπ β π΅ (πππ β (π + π)π(π + π)) β βπ β π΅ (π β€ π β (π + π) β€ (π + π)))) |
43 | 42 | 2ralbidv 3209 |
. . . . . . 7
β’ ((π = π β§ π = (leβπ)) β (βπ β π΅ βπ β π΅ βπ β π΅ (πππ β (π + π)π(π + π)) β βπ β π΅ βπ β π΅ βπ β π΅ (π β€ π β (π + π) β€ (π + π)))) |
44 | 43 | anbi2d 630 |
. . . . . 6
β’ ((π = π β§ π = (leβπ)) β ((π β Toset β§ βπ β π΅ βπ β π΅ βπ β π΅ (πππ β (π + π)π(π + π))) β (π β Toset β§ βπ β π΅ βπ β π΅ βπ β π΅ (π β€ π β (π + π) β€ (π + π))))) |
45 | 32, 44 | sbcied 3785 |
. . . . 5
β’ (π = π β ([(leβπ) / π](π β Toset β§ βπ β π΅ βπ β π΅ βπ β π΅ (πππ β (π + π)π(π + π))) β (π β Toset β§ βπ β π΅ βπ β π΅ βπ β π΅ (π β€ π β (π + π) β€ (π + π))))) |
46 | | eleq1 2822 |
. . . . . 6
β’ (π = π β (π β Toset β π β Toset)) |
47 | 46 | anbi1d 631 |
. . . . 5
β’ (π = π β ((π β Toset β§ βπ β π΅ βπ β π΅ βπ β π΅ (π β€ π β (π + π) β€ (π + π))) β (π β Toset β§ βπ β π΅ βπ β π΅ βπ β π΅ (π β€ π β (π + π) β€ (π + π))))) |
48 | 45, 47 | bitrd 279 |
. . . 4
β’ (π = π β ([(leβπ) / π](π β Toset β§ βπ β π΅ βπ β π΅ βπ β π΅ (πππ β (π + π)π(π + π))) β (π β Toset β§ βπ β π΅ βπ β π΅ βπ β π΅ (π β€ π β (π + π) β€ (π + π))))) |
49 | 15, 31, 48 | 3bitrd 305 |
. . 3
β’ (π = π β ([(Baseβπ) / π£][(+gβπ) / π][(leβπ) / π](π β Toset β§ βπ β π£ βπ β π£ βπ β π£ (πππ β (πππ)π(πππ))) β (π β Toset β§ βπ β π΅ βπ β π΅ βπ β π΅ (π β€ π β (π + π) β€ (π + π))))) |
50 | | df-omnd 31956 |
. . 3
β’ oMnd =
{π β Mnd β£
[(Baseβπ) /
π£][(+gβπ) / π][(leβπ) / π](π β Toset β§ βπ β π£ βπ β π£ βπ β π£ (πππ β (πππ)π(πππ)))} |
51 | 49, 50 | elrab2 3649 |
. 2
β’ (π β oMnd β (π β Mnd β§ (π β Toset β§
βπ β π΅ βπ β π΅ βπ β π΅ (π β€ π β (π + π) β€ (π + π))))) |
52 | | 3anass 1096 |
. 2
β’ ((π β Mnd β§ π β Toset β§
βπ β π΅ βπ β π΅ βπ β π΅ (π β€ π β (π + π) β€ (π + π))) β (π β Mnd β§ (π β Toset β§ βπ β π΅ βπ β π΅ βπ β π΅ (π β€ π β (π + π) β€ (π + π))))) |
53 | 51, 52 | bitr4i 278 |
1
β’ (π β oMnd β (π β Mnd β§ π β Toset β§
βπ β π΅ βπ β π΅ βπ β π΅ (π β€ π β (π + π) β€ (π + π)))) |