Step | Hyp | Ref
| Expression |
1 | | elin 3965 |
. . 3
β’ (π
β (Ring β© oGrp) β
(π
β Ring β§ π
β oGrp)) |
2 | 1 | anbi1i 625 |
. 2
β’ ((π
β (Ring β© oGrp) β§
βπ β π΅ βπ β π΅ (( 0 β€ π β§ 0 β€ π) β 0 β€ (π Β· π))) β ((π
β Ring β§ π
β oGrp) β§ βπ β π΅ βπ β π΅ (( 0 β€ π β§ 0 β€ π) β 0 β€ (π Β· π)))) |
3 | | fvexd 6907 |
. . . . 5
β’ (π = π
β (.rβπ) β V) |
4 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π = π
β§ π‘ = (.rβπ)) β π‘ = (.rβπ)) |
5 | | simpl 484 |
. . . . . . . . . . . . 13
β’ ((π = π
β§ π‘ = (.rβπ)) β π = π
) |
6 | 5 | fveq2d 6896 |
. . . . . . . . . . . 12
β’ ((π = π
β§ π‘ = (.rβπ)) β (.rβπ) = (.rβπ
)) |
7 | | isorng.2 |
. . . . . . . . . . . 12
β’ Β· =
(.rβπ
) |
8 | 6, 7 | eqtr4di 2791 |
. . . . . . . . . . 11
β’ ((π = π
β§ π‘ = (.rβπ)) β (.rβπ) = Β· ) |
9 | 4, 8 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((π = π
β§ π‘ = (.rβπ)) β π‘ = Β· ) |
10 | 9 | oveqd 7426 |
. . . . . . . . 9
β’ ((π = π
β§ π‘ = (.rβπ)) β (ππ‘π) = (π Β· π)) |
11 | 10 | breq2d 5161 |
. . . . . . . 8
β’ ((π = π
β§ π‘ = (.rβπ)) β ( 0 π(ππ‘π) β 0 π(π Β· π))) |
12 | 11 | imbi2d 341 |
. . . . . . 7
β’ ((π = π
β§ π‘ = (.rβπ)) β ((( 0 ππ β§ 0 ππ) β 0 π(ππ‘π)) β (( 0 ππ β§ 0 ππ) β 0 π(π Β· π)))) |
13 | 12 | 2ralbidv 3219 |
. . . . . 6
β’ ((π = π
β§ π‘ = (.rβπ)) β (βπ β π΅ βπ β π΅ (( 0 ππ β§ 0 ππ) β 0 π(ππ‘π)) β βπ β π΅ βπ β π΅ (( 0 ππ β§ 0 ππ) β 0 π(π Β· π)))) |
14 | 13 | sbcbidv 3837 |
. . . . 5
β’ ((π = π
β§ π‘ = (.rβπ)) β ([(leβπ) / π]βπ β π΅ βπ β π΅ (( 0 ππ β§ 0 ππ) β 0 π(ππ‘π)) β [(leβπ) / π]βπ β π΅ βπ β π΅ (( 0 ππ β§ 0 ππ) β 0 π(π Β· π)))) |
15 | 3, 14 | sbcied 3823 |
. . . 4
β’ (π = π
β ([(.rβπ) / π‘][(leβπ) / π]βπ β π΅ βπ β π΅ (( 0 ππ β§ 0 ππ) β 0 π(ππ‘π)) β [(leβπ) / π]βπ β π΅ βπ β π΅ (( 0 ππ β§ 0 ππ) β 0 π(π Β· π)))) |
16 | | fvexd 6907 |
. . . . . 6
β’ (π = π
β (Baseβπ) β V) |
17 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π = π
β§ π£ = (Baseβπ)) β π£ = (Baseβπ)) |
18 | | fveq2 6892 |
. . . . . . . . . . . . 13
β’ (π = π
β (Baseβπ) = (Baseβπ
)) |
19 | | isorng.0 |
. . . . . . . . . . . . 13
β’ π΅ = (Baseβπ
) |
20 | 18, 19 | eqtr4di 2791 |
. . . . . . . . . . . 12
β’ (π = π
β (Baseβπ) = π΅) |
21 | 20 | adantr 482 |
. . . . . . . . . . 11
β’ ((π = π
β§ π£ = (Baseβπ)) β (Baseβπ) = π΅) |
22 | 17, 21 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((π = π
β§ π£ = (Baseβπ)) β π£ = π΅) |
23 | | raleq 3323 |
. . . . . . . . . . 11
β’ (π£ = π΅ β (βπ β π£ ((π§ππ β§ π§ππ) β π§π(ππ‘π)) β βπ β π΅ ((π§ππ β§ π§ππ) β π§π(ππ‘π)))) |
24 | 23 | raleqbi1dv 3334 |
. . . . . . . . . 10
β’ (π£ = π΅ β (βπ β π£ βπ β π£ ((π§ππ β§ π§ππ) β π§π(ππ‘π)) β βπ β π΅ βπ β π΅ ((π§ππ β§ π§ππ) β π§π(ππ‘π)))) |
25 | 22, 24 | syl 17 |
. . . . . . . . 9
β’ ((π = π
β§ π£ = (Baseβπ)) β (βπ β π£ βπ β π£ ((π§ππ β§ π§ππ) β π§π(ππ‘π)) β βπ β π΅ βπ β π΅ ((π§ππ β§ π§ππ) β π§π(ππ‘π)))) |
26 | 25 | sbcbidv 3837 |
. . . . . . . 8
β’ ((π = π
β§ π£ = (Baseβπ)) β ([(leβπ) / π]βπ β π£ βπ β π£ ((π§ππ β§ π§ππ) β π§π(ππ‘π)) β [(leβπ) / π]βπ β π΅ βπ β π΅ ((π§ππ β§ π§ππ) β π§π(ππ‘π)))) |
27 | 26 | sbcbidv 3837 |
. . . . . . 7
β’ ((π = π
β§ π£ = (Baseβπ)) β ([(.rβπ) / π‘][(leβπ) / π]βπ β π£ βπ β π£ ((π§ππ β§ π§ππ) β π§π(ππ‘π)) β [(.rβπ) / π‘][(leβπ) / π]βπ β π΅ βπ β π΅ ((π§ππ β§ π§ππ) β π§π(ππ‘π)))) |
28 | 27 | sbcbidv 3837 |
. . . . . 6
β’ ((π = π
β§ π£ = (Baseβπ)) β ([(0gβπ) / π§][(.rβπ) / π‘][(leβπ) / π]βπ β π£ βπ β π£ ((π§ππ β§ π§ππ) β π§π(ππ‘π)) β [(0gβπ) / π§][(.rβπ) / π‘][(leβπ) / π]βπ β π΅ βπ β π΅ ((π§ππ β§ π§ππ) β π§π(ππ‘π)))) |
29 | 16, 28 | sbcied 3823 |
. . . . 5
β’ (π = π
β ([(Baseβπ) / π£][(0gβπ) / π§][(.rβπ) / π‘][(leβπ) / π]βπ β π£ βπ β π£ ((π§ππ β§ π§ππ) β π§π(ππ‘π)) β [(0gβπ) / π§][(.rβπ) / π‘][(leβπ) / π]βπ β π΅ βπ β π΅ ((π§ππ β§ π§ππ) β π§π(ππ‘π)))) |
30 | | fvexd 6907 |
. . . . . 6
β’ (π = π
β (0gβπ) β V) |
31 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π = π
β§ π§ = (0gβπ)) β π§ = (0gβπ)) |
32 | | fveq2 6892 |
. . . . . . . . . . . . . . 15
β’ (π = π
β (0gβπ) = (0gβπ
)) |
33 | | isorng.1 |
. . . . . . . . . . . . . . 15
β’ 0 =
(0gβπ
) |
34 | 32, 33 | eqtr4di 2791 |
. . . . . . . . . . . . . 14
β’ (π = π
β (0gβπ) = 0 ) |
35 | 34 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π = π
β§ π§ = (0gβπ)) β (0gβπ) = 0 ) |
36 | 31, 35 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ ((π = π
β§ π§ = (0gβπ)) β π§ = 0 ) |
37 | 36 | breq1d 5159 |
. . . . . . . . . . 11
β’ ((π = π
β§ π§ = (0gβπ)) β (π§ππ β 0 ππ)) |
38 | 36 | breq1d 5159 |
. . . . . . . . . . 11
β’ ((π = π
β§ π§ = (0gβπ)) β (π§ππ β 0 ππ)) |
39 | 37, 38 | anbi12d 632 |
. . . . . . . . . 10
β’ ((π = π
β§ π§ = (0gβπ)) β ((π§ππ β§ π§ππ) β ( 0 ππ β§ 0 ππ))) |
40 | 36 | breq1d 5159 |
. . . . . . . . . 10
β’ ((π = π
β§ π§ = (0gβπ)) β (π§π(ππ‘π) β 0 π(ππ‘π))) |
41 | 39, 40 | imbi12d 345 |
. . . . . . . . 9
β’ ((π = π
β§ π§ = (0gβπ)) β (((π§ππ β§ π§ππ) β π§π(ππ‘π)) β (( 0 ππ β§ 0 ππ) β 0 π(ππ‘π)))) |
42 | 41 | 2ralbidv 3219 |
. . . . . . . 8
β’ ((π = π
β§ π§ = (0gβπ)) β (βπ β π΅ βπ β π΅ ((π§ππ β§ π§ππ) β π§π(ππ‘π)) β βπ β π΅ βπ β π΅ (( 0 ππ β§ 0 ππ) β 0 π(ππ‘π)))) |
43 | 42 | sbcbidv 3837 |
. . . . . . 7
β’ ((π = π
β§ π§ = (0gβπ)) β ([(leβπ) / π]βπ β π΅ βπ β π΅ ((π§ππ β§ π§ππ) β π§π(ππ‘π)) β [(leβπ) / π]βπ β π΅ βπ β π΅ (( 0 ππ β§ 0 ππ) β 0 π(ππ‘π)))) |
44 | 43 | sbcbidv 3837 |
. . . . . 6
β’ ((π = π
β§ π§ = (0gβπ)) β ([(.rβπ) / π‘][(leβπ) / π]βπ β π΅ βπ β π΅ ((π§ππ β§ π§ππ) β π§π(ππ‘π)) β [(.rβπ) / π‘][(leβπ) / π]βπ β π΅ βπ β π΅ (( 0 ππ β§ 0 ππ) β 0 π(ππ‘π)))) |
45 | 30, 44 | sbcied 3823 |
. . . . 5
β’ (π = π
β ([(0gβπ) / π§][(.rβπ) / π‘][(leβπ) / π]βπ β π΅ βπ β π΅ ((π§ππ β§ π§ππ) β π§π(ππ‘π)) β [(.rβπ) / π‘][(leβπ) / π]βπ β π΅ βπ β π΅ (( 0 ππ β§ 0 ππ) β 0 π(ππ‘π)))) |
46 | 29, 45 | bitr2d 280 |
. . . 4
β’ (π = π
β ([(.rβπ) / π‘][(leβπ) / π]βπ β π΅ βπ β π΅ (( 0 ππ β§ 0 ππ) β 0 π(ππ‘π)) β [(Baseβπ) / π£][(0gβπ) / π§][(.rβπ) / π‘][(leβπ) / π]βπ β π£ βπ β π£ ((π§ππ β§ π§ππ) β π§π(ππ‘π)))) |
47 | | fvexd 6907 |
. . . . 5
β’ (π = π
β (leβπ) β V) |
48 | | simpr 486 |
. . . . . . . . . 10
β’ ((π = π
β§ π = (leβπ)) β π = (leβπ)) |
49 | | simpl 484 |
. . . . . . . . . . . 12
β’ ((π = π
β§ π = (leβπ)) β π = π
) |
50 | 49 | fveq2d 6896 |
. . . . . . . . . . 11
β’ ((π = π
β§ π = (leβπ)) β (leβπ) = (leβπ
)) |
51 | | isorng.3 |
. . . . . . . . . . 11
β’ β€ =
(leβπ
) |
52 | 50, 51 | eqtr4di 2791 |
. . . . . . . . . 10
β’ ((π = π
β§ π = (leβπ)) β (leβπ) = β€ ) |
53 | 48, 52 | eqtrd 2773 |
. . . . . . . . 9
β’ ((π = π
β§ π = (leβπ)) β π = β€ ) |
54 | 53 | breqd 5160 |
. . . . . . . 8
β’ ((π = π
β§ π = (leβπ)) β ( 0 ππ β 0 β€ π)) |
55 | 53 | breqd 5160 |
. . . . . . . 8
β’ ((π = π
β§ π = (leβπ)) β ( 0 ππ β 0 β€ π)) |
56 | 54, 55 | anbi12d 632 |
. . . . . . 7
β’ ((π = π
β§ π = (leβπ)) β (( 0 ππ β§ 0 ππ) β ( 0 β€ π β§ 0 β€ π))) |
57 | 53 | breqd 5160 |
. . . . . . 7
β’ ((π = π
β§ π = (leβπ)) β ( 0 π(π Β· π) β 0 β€ (π Β· π))) |
58 | 56, 57 | imbi12d 345 |
. . . . . 6
β’ ((π = π
β§ π = (leβπ)) β ((( 0 ππ β§ 0 ππ) β 0 π(π Β· π)) β (( 0 β€ π β§ 0 β€ π) β 0 β€ (π Β· π)))) |
59 | 58 | 2ralbidv 3219 |
. . . . 5
β’ ((π = π
β§ π = (leβπ)) β (βπ β π΅ βπ β π΅ (( 0 ππ β§ 0 ππ) β 0 π(π Β· π)) β βπ β π΅ βπ β π΅ (( 0 β€ π β§ 0 β€ π) β 0 β€ (π Β· π)))) |
60 | 47, 59 | sbcied 3823 |
. . . 4
β’ (π = π
β ([(leβπ) / π]βπ β π΅ βπ β π΅ (( 0 ππ β§ 0 ππ) β 0 π(π Β· π)) β βπ β π΅ βπ β π΅ (( 0 β€ π β§ 0 β€ π) β 0 β€ (π Β· π)))) |
61 | 15, 46, 60 | 3bitr3d 309 |
. . 3
β’ (π = π
β ([(Baseβπ) / π£][(0gβπ) / π§][(.rβπ) / π‘][(leβπ) / π]βπ β π£ βπ β π£ ((π§ππ β§ π§ππ) β π§π(ππ‘π)) β βπ β π΅ βπ β π΅ (( 0 β€ π β§ 0 β€ π) β 0 β€ (π Β· π)))) |
62 | | df-orng 32415 |
. . 3
β’ oRing =
{π β (Ring β© oGrp)
β£ [(Baseβπ) / π£][(0gβπ) / π§][(.rβπ) / π‘][(leβπ) / π]βπ β π£ βπ β π£ ((π§ππ β§ π§ππ) β π§π(ππ‘π))} |
63 | 61, 62 | elrab2 3687 |
. 2
β’ (π
β oRing β (π
β (Ring β© oGrp) β§
βπ β π΅ βπ β π΅ (( 0 β€ π β§ 0 β€ π) β 0 β€ (π Β· π)))) |
64 | | df-3an 1090 |
. 2
β’ ((π
β Ring β§ π
β oGrp β§ βπ β π΅ βπ β π΅ (( 0 β€ π β§ 0 β€ π) β 0 β€ (π Β· π))) β ((π
β Ring β§ π
β oGrp) β§ βπ β π΅ βπ β π΅ (( 0 β€ π β§ 0 β€ π) β 0 β€ (π Β· π)))) |
65 | 2, 63, 64 | 3bitr4i 303 |
1
β’ (π
β oRing β (π
β Ring β§ π
β oGrp β§ βπ β π΅ βπ β π΅ (( 0 β€ π β§ 0 β€ π) β 0 β€ (π Β· π)))) |