Step | Hyp | Ref
| Expression |
1 | | df-br 5110 |
. . . 4
β’ (πΊRingOpsπ» β β¨πΊ, π»β© β RingOps) |
2 | | relrngo 36405 |
. . . . 5
β’ Rel
RingOps |
3 | 2 | brrelex1i 5692 |
. . . 4
β’ (πΊRingOpsπ» β πΊ β V) |
4 | 1, 3 | sylbir 234 |
. . 3
β’
(β¨πΊ, π»β© β RingOps β
πΊ β
V) |
5 | 4 | a1i 11 |
. 2
β’ (π» β π΄ β (β¨πΊ, π»β© β RingOps β πΊ β V)) |
6 | | elex 3465 |
. . . 4
β’ (πΊ β AbelOp β πΊ β V) |
7 | 6 | ad2antrr 725 |
. . 3
β’ (((πΊ β AbelOp β§ π»:(π Γ π)βΆπ) β§ (βπ₯ β π βπ¦ β π βπ§ β π (((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§)) β§ ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§))) β§ βπ₯ β π βπ¦ β π ((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦))) β πΊ β V) |
8 | 7 | a1i 11 |
. 2
β’ (π» β π΄ β (((πΊ β AbelOp β§ π»:(π Γ π)βΆπ) β§ (βπ₯ β π βπ¦ β π βπ§ β π (((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§)) β§ ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§))) β§ βπ₯ β π βπ¦ β π ((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦))) β πΊ β V)) |
9 | | df-rngo 36404 |
. . . . 5
β’ RingOps =
{β¨π, ββ© β£ ((π β AbelOp β§ β:(ran π Γ ran π)βΆran π) β§ (βπ₯ β ran πβπ¦ β ran πβπ§ β ran π(((π₯βπ¦)βπ§) = (π₯β(π¦βπ§)) β§ (π₯β(π¦ππ§)) = ((π₯βπ¦)π(π₯βπ§)) β§ ((π₯ππ¦)βπ§) = ((π₯βπ§)π(π¦βπ§))) β§ βπ₯ β ran πβπ¦ β ran π((π₯βπ¦) = π¦ β§ (π¦βπ₯) = π¦)))} |
10 | 9 | eleq2i 2826 |
. . . 4
β’
(β¨πΊ, π»β© β RingOps β
β¨πΊ, π»β© β {β¨π, ββ© β£ ((π β AbelOp β§ β:(ran π Γ ran π)βΆran π) β§ (βπ₯ β ran πβπ¦ β ran πβπ§ β ran π(((π₯βπ¦)βπ§) = (π₯β(π¦βπ§)) β§ (π₯β(π¦ππ§)) = ((π₯βπ¦)π(π₯βπ§)) β§ ((π₯ππ¦)βπ§) = ((π₯βπ§)π(π¦βπ§))) β§ βπ₯ β ran πβπ¦ β ran π((π₯βπ¦) = π¦ β§ (π¦βπ₯) = π¦)))}) |
11 | | simpl 484 |
. . . . . . . 8
β’ ((π = πΊ β§ β = π») β π = πΊ) |
12 | 11 | eleq1d 2819 |
. . . . . . 7
β’ ((π = πΊ β§ β = π») β (π β AbelOp β πΊ β AbelOp)) |
13 | | simpr 486 |
. . . . . . . 8
β’ ((π = πΊ β§ β = π») β β = π») |
14 | 11 | rneqd 5897 |
. . . . . . . . . 10
β’ ((π = πΊ β§ β = π») β ran π = ran πΊ) |
15 | | isring.1 |
. . . . . . . . . 10
β’ π = ran πΊ |
16 | 14, 15 | eqtr4di 2791 |
. . . . . . . . 9
β’ ((π = πΊ β§ β = π») β ran π = π) |
17 | 16 | sqxpeqd 5669 |
. . . . . . . 8
β’ ((π = πΊ β§ β = π») β (ran π Γ ran π) = (π Γ π)) |
18 | 13, 17, 16 | feq123d 6661 |
. . . . . . 7
β’ ((π = πΊ β§ β = π») β (β:(ran π Γ ran π)βΆran π β π»:(π Γ π)βΆπ)) |
19 | 12, 18 | anbi12d 632 |
. . . . . 6
β’ ((π = πΊ β§ β = π») β ((π β AbelOp β§ β:(ran π Γ ran π)βΆran π) β (πΊ β AbelOp β§ π»:(π Γ π)βΆπ))) |
20 | 13 | oveqd 7378 |
. . . . . . . . . . . . 13
β’ ((π = πΊ β§ β = π») β (π₯βπ¦) = (π₯π»π¦)) |
21 | | eqidd 2734 |
. . . . . . . . . . . . 13
β’ ((π = πΊ β§ β = π») β π§ = π§) |
22 | 13, 20, 21 | oveq123d 7382 |
. . . . . . . . . . . 12
β’ ((π = πΊ β§ β = π») β ((π₯βπ¦)βπ§) = ((π₯π»π¦)π»π§)) |
23 | | eqidd 2734 |
. . . . . . . . . . . . 13
β’ ((π = πΊ β§ β = π») β π₯ = π₯) |
24 | 13 | oveqd 7378 |
. . . . . . . . . . . . 13
β’ ((π = πΊ β§ β = π») β (π¦βπ§) = (π¦π»π§)) |
25 | 13, 23, 24 | oveq123d 7382 |
. . . . . . . . . . . 12
β’ ((π = πΊ β§ β = π») β (π₯β(π¦βπ§)) = (π₯π»(π¦π»π§))) |
26 | 22, 25 | eqeq12d 2749 |
. . . . . . . . . . 11
β’ ((π = πΊ β§ β = π») β (((π₯βπ¦)βπ§) = (π₯β(π¦βπ§)) β ((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)))) |
27 | 11 | oveqd 7378 |
. . . . . . . . . . . . 13
β’ ((π = πΊ β§ β = π») β (π¦ππ§) = (π¦πΊπ§)) |
28 | 13, 23, 27 | oveq123d 7382 |
. . . . . . . . . . . 12
β’ ((π = πΊ β§ β = π») β (π₯β(π¦ππ§)) = (π₯π»(π¦πΊπ§))) |
29 | 13 | oveqd 7378 |
. . . . . . . . . . . . 13
β’ ((π = πΊ β§ β = π») β (π₯βπ§) = (π₯π»π§)) |
30 | 11, 20, 29 | oveq123d 7382 |
. . . . . . . . . . . 12
β’ ((π = πΊ β§ β = π») β ((π₯βπ¦)π(π₯βπ§)) = ((π₯π»π¦)πΊ(π₯π»π§))) |
31 | 28, 30 | eqeq12d 2749 |
. . . . . . . . . . 11
β’ ((π = πΊ β§ β = π») β ((π₯β(π¦ππ§)) = ((π₯βπ¦)π(π₯βπ§)) β (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§)))) |
32 | 11 | oveqd 7378 |
. . . . . . . . . . . . 13
β’ ((π = πΊ β§ β = π») β (π₯ππ¦) = (π₯πΊπ¦)) |
33 | 13, 32, 21 | oveq123d 7382 |
. . . . . . . . . . . 12
β’ ((π = πΊ β§ β = π») β ((π₯ππ¦)βπ§) = ((π₯πΊπ¦)π»π§)) |
34 | 11, 29, 24 | oveq123d 7382 |
. . . . . . . . . . . 12
β’ ((π = πΊ β§ β = π») β ((π₯βπ§)π(π¦βπ§)) = ((π₯π»π§)πΊ(π¦π»π§))) |
35 | 33, 34 | eqeq12d 2749 |
. . . . . . . . . . 11
β’ ((π = πΊ β§ β = π») β (((π₯ππ¦)βπ§) = ((π₯βπ§)π(π¦βπ§)) β ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§)))) |
36 | 26, 31, 35 | 3anbi123d 1437 |
. . . . . . . . . 10
β’ ((π = πΊ β§ β = π») β ((((π₯βπ¦)βπ§) = (π₯β(π¦βπ§)) β§ (π₯β(π¦ππ§)) = ((π₯βπ¦)π(π₯βπ§)) β§ ((π₯ππ¦)βπ§) = ((π₯βπ§)π(π¦βπ§))) β (((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§)) β§ ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§))))) |
37 | 16, 36 | raleqbidv 3318 |
. . . . . . . . 9
β’ ((π = πΊ β§ β = π») β (βπ§ β ran π(((π₯βπ¦)βπ§) = (π₯β(π¦βπ§)) β§ (π₯β(π¦ππ§)) = ((π₯βπ¦)π(π₯βπ§)) β§ ((π₯ππ¦)βπ§) = ((π₯βπ§)π(π¦βπ§))) β βπ§ β π (((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§)) β§ ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§))))) |
38 | 16, 37 | raleqbidv 3318 |
. . . . . . . 8
β’ ((π = πΊ β§ β = π») β (βπ¦ β ran πβπ§ β ran π(((π₯βπ¦)βπ§) = (π₯β(π¦βπ§)) β§ (π₯β(π¦ππ§)) = ((π₯βπ¦)π(π₯βπ§)) β§ ((π₯ππ¦)βπ§) = ((π₯βπ§)π(π¦βπ§))) β βπ¦ β π βπ§ β π (((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§)) β§ ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§))))) |
39 | 16, 38 | raleqbidv 3318 |
. . . . . . 7
β’ ((π = πΊ β§ β = π») β (βπ₯ β ran πβπ¦ β ran πβπ§ β ran π(((π₯βπ¦)βπ§) = (π₯β(π¦βπ§)) β§ (π₯β(π¦ππ§)) = ((π₯βπ¦)π(π₯βπ§)) β§ ((π₯ππ¦)βπ§) = ((π₯βπ§)π(π¦βπ§))) β βπ₯ β π βπ¦ β π βπ§ β π (((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§)) β§ ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§))))) |
40 | 20 | eqeq1d 2735 |
. . . . . . . . . 10
β’ ((π = πΊ β§ β = π») β ((π₯βπ¦) = π¦ β (π₯π»π¦) = π¦)) |
41 | 13 | oveqd 7378 |
. . . . . . . . . . 11
β’ ((π = πΊ β§ β = π») β (π¦βπ₯) = (π¦π»π₯)) |
42 | 41 | eqeq1d 2735 |
. . . . . . . . . 10
β’ ((π = πΊ β§ β = π») β ((π¦βπ₯) = π¦ β (π¦π»π₯) = π¦)) |
43 | 40, 42 | anbi12d 632 |
. . . . . . . . 9
β’ ((π = πΊ β§ β = π») β (((π₯βπ¦) = π¦ β§ (π¦βπ₯) = π¦) β ((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦))) |
44 | 16, 43 | raleqbidv 3318 |
. . . . . . . 8
β’ ((π = πΊ β§ β = π») β (βπ¦ β ran π((π₯βπ¦) = π¦ β§ (π¦βπ₯) = π¦) β βπ¦ β π ((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦))) |
45 | 16, 44 | rexeqbidv 3319 |
. . . . . . 7
β’ ((π = πΊ β§ β = π») β (βπ₯ β ran πβπ¦ β ran π((π₯βπ¦) = π¦ β§ (π¦βπ₯) = π¦) β βπ₯ β π βπ¦ β π ((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦))) |
46 | 39, 45 | anbi12d 632 |
. . . . . 6
β’ ((π = πΊ β§ β = π») β ((βπ₯ β ran πβπ¦ β ran πβπ§ β ran π(((π₯βπ¦)βπ§) = (π₯β(π¦βπ§)) β§ (π₯β(π¦ππ§)) = ((π₯βπ¦)π(π₯βπ§)) β§ ((π₯ππ¦)βπ§) = ((π₯βπ§)π(π¦βπ§))) β§ βπ₯ β ran πβπ¦ β ran π((π₯βπ¦) = π¦ β§ (π¦βπ₯) = π¦)) β (βπ₯ β π βπ¦ β π βπ§ β π (((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§)) β§ ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§))) β§ βπ₯ β π βπ¦ β π ((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦)))) |
47 | 19, 46 | anbi12d 632 |
. . . . 5
β’ ((π = πΊ β§ β = π») β (((π β AbelOp β§ β:(ran π Γ ran π)βΆran π) β§ (βπ₯ β ran πβπ¦ β ran πβπ§ β ran π(((π₯βπ¦)βπ§) = (π₯β(π¦βπ§)) β§ (π₯β(π¦ππ§)) = ((π₯βπ¦)π(π₯βπ§)) β§ ((π₯ππ¦)βπ§) = ((π₯βπ§)π(π¦βπ§))) β§ βπ₯ β ran πβπ¦ β ran π((π₯βπ¦) = π¦ β§ (π¦βπ₯) = π¦))) β ((πΊ β AbelOp β§ π»:(π Γ π)βΆπ) β§ (βπ₯ β π βπ¦ β π βπ§ β π (((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§)) β§ ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§))) β§ βπ₯ β π βπ¦ β π ((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦))))) |
48 | 47 | opelopabga 5494 |
. . . 4
β’ ((πΊ β V β§ π» β π΄) β (β¨πΊ, π»β© β {β¨π, ββ© β£ ((π β AbelOp β§ β:(ran π Γ ran π)βΆran π) β§ (βπ₯ β ran πβπ¦ β ran πβπ§ β ran π(((π₯βπ¦)βπ§) = (π₯β(π¦βπ§)) β§ (π₯β(π¦ππ§)) = ((π₯βπ¦)π(π₯βπ§)) β§ ((π₯ππ¦)βπ§) = ((π₯βπ§)π(π¦βπ§))) β§ βπ₯ β ran πβπ¦ β ran π((π₯βπ¦) = π¦ β§ (π¦βπ₯) = π¦)))} β ((πΊ β AbelOp β§ π»:(π Γ π)βΆπ) β§ (βπ₯ β π βπ¦ β π βπ§ β π (((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§)) β§ ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§))) β§ βπ₯ β π βπ¦ β π ((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦))))) |
49 | 10, 48 | bitrid 283 |
. . 3
β’ ((πΊ β V β§ π» β π΄) β (β¨πΊ, π»β© β RingOps β ((πΊ β AbelOp β§ π»:(π Γ π)βΆπ) β§ (βπ₯ β π βπ¦ β π βπ§ β π (((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§)) β§ ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§))) β§ βπ₯ β π βπ¦ β π ((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦))))) |
50 | 49 | expcom 415 |
. 2
β’ (π» β π΄ β (πΊ β V β (β¨πΊ, π»β© β RingOps β ((πΊ β AbelOp β§ π»:(π Γ π)βΆπ) β§ (βπ₯ β π βπ¦ β π βπ§ β π (((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§)) β§ ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§))) β§ βπ₯ β π βπ¦ β π ((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦)))))) |
51 | 5, 8, 50 | pm5.21ndd 381 |
1
β’ (π» β π΄ β (β¨πΊ, π»β© β RingOps β ((πΊ β AbelOp β§ π»:(π Γ π)βΆπ) β§ (βπ₯ β π βπ¦ β π βπ§ β π (((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§)) β§ ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§))) β§ βπ₯ β π βπ¦ β π ((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦))))) |