Step | Hyp | Ref
| Expression |
1 | | isringod.1 |
. . 3
β’ (π β πΊ β AbelOp) |
2 | | isringod.3 |
. . . 4
β’ (π β π»:(π Γ π)βΆπ) |
3 | | isringod.2 |
. . . . . 6
β’ (π β π = ran πΊ) |
4 | 3 | sqxpeqd 5669 |
. . . . 5
β’ (π β (π Γ π) = (ran πΊ Γ ran πΊ)) |
5 | 4, 3 | feq23d 6667 |
. . . 4
β’ (π β (π»:(π Γ π)βΆπ β π»:(ran πΊ Γ ran πΊ)βΆran πΊ)) |
6 | 2, 5 | mpbid 231 |
. . 3
β’ (π β π»:(ran πΊ Γ ran πΊ)βΆran πΊ) |
7 | | isringod.4 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§))) |
8 | | isringod.5 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§))) |
9 | | isringod.6 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§))) |
10 | 7, 8, 9 | 3jca 1129 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§)) β§ ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§)))) |
11 | 10 | ralrimivvva 3197 |
. . . . 5
β’ (π β βπ₯ β π βπ¦ β π βπ§ β π (((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§)) β§ ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§)))) |
12 | 3 | raleqdv 3312 |
. . . . . . 7
β’ (π β (βπ§ β π (((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§)) β§ ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§))) β βπ§ β ran πΊ(((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§)) β§ ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§))))) |
13 | 3, 12 | raleqbidv 3318 |
. . . . . 6
β’ (π β (βπ¦ β π βπ§ β π (((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§)) β§ ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§))) β βπ¦ β ran πΊβπ§ β ran πΊ(((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§)) β§ ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§))))) |
14 | 3, 13 | raleqbidv 3318 |
. . . . 5
β’ (π β (βπ₯ β π βπ¦ β π βπ§ β π (((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§)) β§ ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§))) β βπ₯ β ran πΊβπ¦ β ran πΊβπ§ β ran πΊ(((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§)) β§ ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§))))) |
15 | 11, 14 | mpbid 231 |
. . . 4
β’ (π β βπ₯ β ran πΊβπ¦ β ran πΊβπ§ β ran πΊ(((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§)) β§ ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§)))) |
16 | | isringod.7 |
. . . . . 6
β’ (π β π β π) |
17 | | isringod.8 |
. . . . . . . 8
β’ ((π β§ π¦ β π) β (ππ»π¦) = π¦) |
18 | | isringod.9 |
. . . . . . . 8
β’ ((π β§ π¦ β π) β (π¦π»π) = π¦) |
19 | 17, 18 | jca 513 |
. . . . . . 7
β’ ((π β§ π¦ β π) β ((ππ»π¦) = π¦ β§ (π¦π»π) = π¦)) |
20 | 19 | ralrimiva 3140 |
. . . . . 6
β’ (π β βπ¦ β π ((ππ»π¦) = π¦ β§ (π¦π»π) = π¦)) |
21 | | oveq1 7368 |
. . . . . . . . 9
β’ (π₯ = π β (π₯π»π¦) = (ππ»π¦)) |
22 | 21 | eqeq1d 2735 |
. . . . . . . 8
β’ (π₯ = π β ((π₯π»π¦) = π¦ β (ππ»π¦) = π¦)) |
23 | 22 | ovanraleqv 7385 |
. . . . . . 7
β’ (π₯ = π β (βπ¦ β π ((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦) β βπ¦ β π ((ππ»π¦) = π¦ β§ (π¦π»π) = π¦))) |
24 | 23 | rspcev 3583 |
. . . . . 6
β’ ((π β π β§ βπ¦ β π ((ππ»π¦) = π¦ β§ (π¦π»π) = π¦)) β βπ₯ β π βπ¦ β π ((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦)) |
25 | 16, 20, 24 | syl2anc 585 |
. . . . 5
β’ (π β βπ₯ β π βπ¦ β π ((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦)) |
26 | 3 | raleqdv 3312 |
. . . . . 6
β’ (π β (βπ¦ β π ((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦) β βπ¦ β ran πΊ((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦))) |
27 | 3, 26 | rexeqbidv 3319 |
. . . . 5
β’ (π β (βπ₯ β π βπ¦ β π ((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦) β βπ₯ β ran πΊβπ¦ β ran πΊ((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦))) |
28 | 25, 27 | mpbid 231 |
. . . 4
β’ (π β βπ₯ β ran πΊβπ¦ β ran πΊ((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦)) |
29 | 15, 28 | jca 513 |
. . 3
β’ (π β (βπ₯ β ran πΊβπ¦ β ran πΊβπ§ β ran πΊ(((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§)) β§ ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§))) β§ βπ₯ β ran πΊβπ¦ β ran πΊ((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦))) |
30 | 1, 6, 29 | jca31 516 |
. 2
β’ (π β ((πΊ β AbelOp β§ π»:(ran πΊ Γ ran πΊ)βΆran πΊ) β§ (βπ₯ β ran πΊβπ¦ β ran πΊβπ§ β ran πΊ(((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§)) β§ ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§))) β§ βπ₯ β ran πΊβπ¦ β ran πΊ((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦)))) |
31 | | rnexg 7845 |
. . . . . 6
β’ (πΊ β AbelOp β ran πΊ β V) |
32 | 1, 31 | syl 17 |
. . . . 5
β’ (π β ran πΊ β V) |
33 | 32, 32 | xpexd 7689 |
. . . 4
β’ (π β (ran πΊ Γ ran πΊ) β V) |
34 | 6, 33 | fexd 7181 |
. . 3
β’ (π β π» β V) |
35 | | eqid 2733 |
. . . 4
β’ ran πΊ = ran πΊ |
36 | 35 | isrngo 36406 |
. . 3
β’ (π» β V β (β¨πΊ, π»β© β RingOps β ((πΊ β AbelOp β§ π»:(ran πΊ Γ ran πΊ)βΆran πΊ) β§ (βπ₯ β ran πΊβπ¦ β ran πΊβπ§ β ran πΊ(((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§)) β§ ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§))) β§ βπ₯ β ran πΊβπ¦ β ran πΊ((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦))))) |
37 | 34, 36 | syl 17 |
. 2
β’ (π β (β¨πΊ, π»β© β RingOps β ((πΊ β AbelOp β§ π»:(ran πΊ Γ ran πΊ)βΆran πΊ) β§ (βπ₯ β ran πΊβπ¦ β ran πΊβπ§ β ran πΊ(((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§)) β§ ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§))) β§ βπ₯ β ran πΊβπ¦ β ran πΊ((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦))))) |
38 | 30, 37 | mpbird 257 |
1
β’ (π β β¨πΊ, π»β© β RingOps) |