Step | Hyp | Ref
| Expression |
1 | | isdivrng1.1 |
. . 3
β’ πΊ = (1st βπ
) |
2 | | isdivrng1.2 |
. . 3
β’ π» = (2nd βπ
) |
3 | | isdivrng1.3 |
. . 3
β’ π = (GIdβπΊ) |
4 | | isdivrng1.4 |
. . 3
β’ π = ran πΊ |
5 | 1, 2, 3, 4 | isdrngo1 36418 |
. 2
β’ (π
β DivRingOps β (π
β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp)) |
6 | | isdivrng2.5 |
. . . . . . 7
β’ π = (GIdβπ») |
7 | 1, 2, 4, 3, 6 | dvrunz 36416 |
. . . . . 6
β’ (π
β DivRingOps β π β π) |
8 | 5, 7 | sylbir 234 |
. . . . 5
β’ ((π
β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp) β π β π) |
9 | | grporndm 29455 |
. . . . . . . . . . . 12
β’ ((π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp β ran (π» βΎ ((π β {π}) Γ (π β {π}))) = dom dom (π» βΎ ((π β {π}) Γ (π β {π})))) |
10 | 9 | adantl 483 |
. . . . . . . . . . 11
β’ ((π
β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp) β ran (π» βΎ ((π β {π}) Γ (π β {π}))) = dom dom (π» βΎ ((π β {π}) Γ (π β {π})))) |
11 | | difss 4092 |
. . . . . . . . . . . . . . . . 17
β’ (π β {π}) β π |
12 | | xpss12 5649 |
. . . . . . . . . . . . . . . . 17
β’ (((π β {π}) β π β§ (π β {π}) β π) β ((π β {π}) Γ (π β {π})) β (π Γ π)) |
13 | 11, 11, 12 | mp2an 691 |
. . . . . . . . . . . . . . . 16
β’ ((π β {π}) Γ (π β {π})) β (π Γ π) |
14 | 1, 2, 4 | rngosm 36362 |
. . . . . . . . . . . . . . . . 17
β’ (π
β RingOps β π»:(π Γ π)βΆπ) |
15 | 14 | fdmd 6680 |
. . . . . . . . . . . . . . . 16
β’ (π
β RingOps β dom π» = (π Γ π)) |
16 | 13, 15 | sseqtrrid 3998 |
. . . . . . . . . . . . . . 15
β’ (π
β RingOps β ((π β {π}) Γ (π β {π})) β dom π») |
17 | 16 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π
β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp) β ((π β {π}) Γ (π β {π})) β dom π») |
18 | | ssdmres 5961 |
. . . . . . . . . . . . . 14
β’ (((π β {π}) Γ (π β {π})) β dom π» β dom (π» βΎ ((π β {π}) Γ (π β {π}))) = ((π β {π}) Γ (π β {π}))) |
19 | 17, 18 | sylib 217 |
. . . . . . . . . . . . 13
β’ ((π
β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp) β dom (π» βΎ ((π β {π}) Γ (π β {π}))) = ((π β {π}) Γ (π β {π}))) |
20 | 19 | dmeqd 5862 |
. . . . . . . . . . . 12
β’ ((π
β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp) β dom dom (π» βΎ ((π β {π}) Γ (π β {π}))) = dom ((π β {π}) Γ (π β {π}))) |
21 | | dmxpid 5886 |
. . . . . . . . . . . 12
β’ dom
((π β {π}) Γ (π β {π})) = (π β {π}) |
22 | 20, 21 | eqtrdi 2793 |
. . . . . . . . . . 11
β’ ((π
β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp) β dom dom (π» βΎ ((π β {π}) Γ (π β {π}))) = (π β {π})) |
23 | 10, 22 | eqtrd 2777 |
. . . . . . . . . 10
β’ ((π
β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp) β ran (π» βΎ ((π β {π}) Γ (π β {π}))) = (π β {π})) |
24 | 23 | eleq2d 2824 |
. . . . . . . . 9
β’ ((π
β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp) β (π₯ β ran (π» βΎ ((π β {π}) Γ (π β {π}))) β π₯ β (π β {π}))) |
25 | 24 | biimpar 479 |
. . . . . . . 8
β’ (((π
β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp) β§ π₯ β (π β {π})) β π₯ β ran (π» βΎ ((π β {π}) Γ (π β {π})))) |
26 | | eqid 2737 |
. . . . . . . . . . 11
β’ ran
(π» βΎ ((π β {π}) Γ (π β {π}))) = ran (π» βΎ ((π β {π}) Γ (π β {π}))) |
27 | | eqid 2737 |
. . . . . . . . . . 11
β’
(invβ(π»
βΎ ((π β {π}) Γ (π β {π})))) = (invβ(π» βΎ ((π β {π}) Γ (π β {π})))) |
28 | 26, 27 | grpoinvcl 29469 |
. . . . . . . . . 10
β’ (((π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp β§ π₯ β ran (π» βΎ ((π β {π}) Γ (π β {π})))) β ((invβ(π» βΎ ((π β {π}) Γ (π β {π}))))βπ₯) β ran (π» βΎ ((π β {π}) Γ (π β {π})))) |
29 | 28 | adantll 713 |
. . . . . . . . 9
β’ (((π
β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp) β§ π₯ β ran (π» βΎ ((π β {π}) Γ (π β {π})))) β ((invβ(π» βΎ ((π β {π}) Γ (π β {π}))))βπ₯) β ran (π» βΎ ((π β {π}) Γ (π β {π})))) |
30 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(GIdβ(π»
βΎ ((π β {π}) Γ (π β {π})))) = (GIdβ(π» βΎ ((π β {π}) Γ (π β {π})))) |
31 | 26, 30, 27 | grpolinv 29471 |
. . . . . . . . . . 11
β’ (((π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp β§ π₯ β ran (π» βΎ ((π β {π}) Γ (π β {π})))) β (((invβ(π» βΎ ((π β {π}) Γ (π β {π}))))βπ₯)(π» βΎ ((π β {π}) Γ (π β {π})))π₯) = (GIdβ(π» βΎ ((π β {π}) Γ (π β {π}))))) |
32 | 31 | adantll 713 |
. . . . . . . . . 10
β’ (((π
β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp) β§ π₯ β ran (π» βΎ ((π β {π}) Γ (π β {π})))) β (((invβ(π» βΎ ((π β {π}) Γ (π β {π}))))βπ₯)(π» βΎ ((π β {π}) Γ (π β {π})))π₯) = (GIdβ(π» βΎ ((π β {π}) Γ (π β {π}))))) |
33 | 2 | rngomndo 36397 |
. . . . . . . . . . . . . 14
β’ (π
β RingOps β π» β MndOp) |
34 | | mndomgmid 36333 |
. . . . . . . . . . . . . 14
β’ (π» β MndOp β π» β (Magma β© ExId
)) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . 13
β’ (π
β RingOps β π» β (Magma β© ExId
)) |
36 | 35 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π
β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp) β π» β (Magma β© ExId
)) |
37 | 11, 4 | sseqtri 3981 |
. . . . . . . . . . . . . 14
β’ (π β {π}) β ran πΊ |
38 | 2, 1 | rngorn1eq 36396 |
. . . . . . . . . . . . . 14
β’ (π
β RingOps β ran πΊ = ran π») |
39 | 37, 38 | sseqtrid 3997 |
. . . . . . . . . . . . 13
β’ (π
β RingOps β (π β {π}) β ran π») |
40 | 39 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π
β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp) β (π β {π}) β ran π») |
41 | 1 | rneqi 5893 |
. . . . . . . . . . . . . . . 16
β’ ran πΊ = ran (1st
βπ
) |
42 | 4, 41 | eqtri 2765 |
. . . . . . . . . . . . . . 15
β’ π = ran (1st
βπ
) |
43 | 42, 2, 6 | rngo1cl 36401 |
. . . . . . . . . . . . . 14
β’ (π
β RingOps β π β π) |
44 | 43 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π
β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp) β π β π) |
45 | | eldifsn 4748 |
. . . . . . . . . . . . 13
β’ (π β (π β {π}) β (π β π β§ π β π)) |
46 | 44, 8, 45 | sylanbrc 584 |
. . . . . . . . . . . 12
β’ ((π
β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp) β π β (π β {π})) |
47 | | grpomndo 36337 |
. . . . . . . . . . . . . 14
β’ ((π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp β (π» βΎ ((π β {π}) Γ (π β {π}))) β MndOp) |
48 | | mndoismgmOLD 36332 |
. . . . . . . . . . . . . 14
β’ ((π» βΎ ((π β {π}) Γ (π β {π}))) β MndOp β (π» βΎ ((π β {π}) Γ (π β {π}))) β Magma) |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp β (π» βΎ ((π β {π}) Γ (π β {π}))) β Magma) |
50 | 49 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π
β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp) β (π» βΎ ((π β {π}) Γ (π β {π}))) β Magma) |
51 | | eqid 2737 |
. . . . . . . . . . . . 13
β’ ran π» = ran π» |
52 | | eqid 2737 |
. . . . . . . . . . . . 13
β’ (π» βΎ ((π β {π}) Γ (π β {π}))) = (π» βΎ ((π β {π}) Γ (π β {π}))) |
53 | 51, 6, 52 | exidresid 36341 |
. . . . . . . . . . . 12
β’ (((π» β (Magma β© ExId )
β§ (π β {π}) β ran π» β§ π β (π β {π})) β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β Magma) β (GIdβ(π» βΎ ((π β {π}) Γ (π β {π})))) = π) |
54 | 36, 40, 46, 50, 53 | syl31anc 1374 |
. . . . . . . . . . 11
β’ ((π
β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp) β (GIdβ(π» βΎ ((π β {π}) Γ (π β {π})))) = π) |
55 | 54 | adantr 482 |
. . . . . . . . . 10
β’ (((π
β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp) β§ π₯ β ran (π» βΎ ((π β {π}) Γ (π β {π})))) β (GIdβ(π» βΎ ((π β {π}) Γ (π β {π})))) = π) |
56 | 32, 55 | eqtrd 2777 |
. . . . . . . . 9
β’ (((π
β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp) β§ π₯ β ran (π» βΎ ((π β {π}) Γ (π β {π})))) β (((invβ(π» βΎ ((π β {π}) Γ (π β {π}))))βπ₯)(π» βΎ ((π β {π}) Γ (π β {π})))π₯) = π) |
57 | | oveq1 7365 |
. . . . . . . . . . 11
β’ (π¦ = ((invβ(π» βΎ ((π β {π}) Γ (π β {π}))))βπ₯) β (π¦(π» βΎ ((π β {π}) Γ (π β {π})))π₯) = (((invβ(π» βΎ ((π β {π}) Γ (π β {π}))))βπ₯)(π» βΎ ((π β {π}) Γ (π β {π})))π₯)) |
58 | 57 | eqeq1d 2739 |
. . . . . . . . . 10
β’ (π¦ = ((invβ(π» βΎ ((π β {π}) Γ (π β {π}))))βπ₯) β ((π¦(π» βΎ ((π β {π}) Γ (π β {π})))π₯) = π β (((invβ(π» βΎ ((π β {π}) Γ (π β {π}))))βπ₯)(π» βΎ ((π β {π}) Γ (π β {π})))π₯) = π)) |
59 | 58 | rspcev 3582 |
. . . . . . . . 9
β’
((((invβ(π»
βΎ ((π β {π}) Γ (π β {π}))))βπ₯) β ran (π» βΎ ((π β {π}) Γ (π β {π}))) β§ (((invβ(π» βΎ ((π β {π}) Γ (π β {π}))))βπ₯)(π» βΎ ((π β {π}) Γ (π β {π})))π₯) = π) β βπ¦ β ran (π» βΎ ((π β {π}) Γ (π β {π})))(π¦(π» βΎ ((π β {π}) Γ (π β {π})))π₯) = π) |
60 | 29, 56, 59 | syl2anc 585 |
. . . . . . . 8
β’ (((π
β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp) β§ π₯ β ran (π» βΎ ((π β {π}) Γ (π β {π})))) β βπ¦ β ran (π» βΎ ((π β {π}) Γ (π β {π})))(π¦(π» βΎ ((π β {π}) Γ (π β {π})))π₯) = π) |
61 | 25, 60 | syldan 592 |
. . . . . . 7
β’ (((π
β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp) β§ π₯ β (π β {π})) β βπ¦ β ran (π» βΎ ((π β {π}) Γ (π β {π})))(π¦(π» βΎ ((π β {π}) Γ (π β {π})))π₯) = π) |
62 | 23 | adantr 482 |
. . . . . . . . 9
β’ (((π
β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp) β§ π₯ β (π β {π})) β ran (π» βΎ ((π β {π}) Γ (π β {π}))) = (π β {π})) |
63 | 62 | rexeqdv 3315 |
. . . . . . . 8
β’ (((π
β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp) β§ π₯ β (π β {π})) β (βπ¦ β ran (π» βΎ ((π β {π}) Γ (π β {π})))(π¦(π» βΎ ((π β {π}) Γ (π β {π})))π₯) = π β βπ¦ β (π β {π})(π¦(π» βΎ ((π β {π}) Γ (π β {π})))π₯) = π)) |
64 | | ovres 7521 |
. . . . . . . . . . . 12
β’ ((π¦ β (π β {π}) β§ π₯ β (π β {π})) β (π¦(π» βΎ ((π β {π}) Γ (π β {π})))π₯) = (π¦π»π₯)) |
65 | 64 | ancoms 460 |
. . . . . . . . . . 11
β’ ((π₯ β (π β {π}) β§ π¦ β (π β {π})) β (π¦(π» βΎ ((π β {π}) Γ (π β {π})))π₯) = (π¦π»π₯)) |
66 | 65 | eqeq1d 2739 |
. . . . . . . . . 10
β’ ((π₯ β (π β {π}) β§ π¦ β (π β {π})) β ((π¦(π» βΎ ((π β {π}) Γ (π β {π})))π₯) = π β (π¦π»π₯) = π)) |
67 | 66 | rexbidva 3174 |
. . . . . . . . 9
β’ (π₯ β (π β {π}) β (βπ¦ β (π β {π})(π¦(π» βΎ ((π β {π}) Γ (π β {π})))π₯) = π β βπ¦ β (π β {π})(π¦π»π₯) = π)) |
68 | 67 | adantl 483 |
. . . . . . . 8
β’ (((π
β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp) β§ π₯ β (π β {π})) β (βπ¦ β (π β {π})(π¦(π» βΎ ((π β {π}) Γ (π β {π})))π₯) = π β βπ¦ β (π β {π})(π¦π»π₯) = π)) |
69 | 63, 68 | bitrd 279 |
. . . . . . 7
β’ (((π
β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp) β§ π₯ β (π β {π})) β (βπ¦ β ran (π» βΎ ((π β {π}) Γ (π β {π})))(π¦(π» βΎ ((π β {π}) Γ (π β {π})))π₯) = π β βπ¦ β (π β {π})(π¦π»π₯) = π)) |
70 | 61, 69 | mpbid 231 |
. . . . . 6
β’ (((π
β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp) β§ π₯ β (π β {π})) β βπ¦ β (π β {π})(π¦π»π₯) = π) |
71 | 70 | ralrimiva 3144 |
. . . . 5
β’ ((π
β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp) β βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π) |
72 | 8, 71 | jca 513 |
. . . 4
β’ ((π
β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp) β (π β π β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π)) |
73 | 1 | fvexi 6857 |
. . . . . . . 8
β’ πΊ β V |
74 | 73 | rnex 7850 |
. . . . . . 7
β’ ran πΊ β V |
75 | 4, 74 | eqeltri 2834 |
. . . . . 6
β’ π β V |
76 | | difexg 5285 |
. . . . . 6
β’ (π β V β (π β {π}) β V) |
77 | 75, 76 | mp1i 13 |
. . . . 5
β’ ((π
β RingOps β§ (π β π β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π)) β (π β {π}) β V) |
78 | 14 | ffnd 6670 |
. . . . . . . 8
β’ (π
β RingOps β π» Fn (π Γ π)) |
79 | 78 | adantr 482 |
. . . . . . 7
β’ ((π
β RingOps β§ (π β π β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π)) β π» Fn (π Γ π)) |
80 | | fnssres 6625 |
. . . . . . 7
β’ ((π» Fn (π Γ π) β§ ((π β {π}) Γ (π β {π})) β (π Γ π)) β (π» βΎ ((π β {π}) Γ (π β {π}))) Fn ((π β {π}) Γ (π β {π}))) |
81 | 79, 13, 80 | sylancl 587 |
. . . . . 6
β’ ((π
β RingOps β§ (π β π β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π)) β (π» βΎ ((π β {π}) Γ (π β {π}))) Fn ((π β {π}) Γ (π β {π}))) |
82 | | ovres 7521 |
. . . . . . . . 9
β’ ((π’ β (π β {π}) β§ π£ β (π β {π})) β (π’(π» βΎ ((π β {π}) Γ (π β {π})))π£) = (π’π»π£)) |
83 | 82 | adantl 483 |
. . . . . . . 8
β’ (((π
β RingOps β§ (π β π β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π)) β§ (π’ β (π β {π}) β§ π£ β (π β {π}))) β (π’(π» βΎ ((π β {π}) Γ (π β {π})))π£) = (π’π»π£)) |
84 | | eldifi 4087 |
. . . . . . . . . . . 12
β’ (π’ β (π β {π}) β π’ β π) |
85 | | eldifi 4087 |
. . . . . . . . . . . 12
β’ (π£ β (π β {π}) β π£ β π) |
86 | 84, 85 | anim12i 614 |
. . . . . . . . . . 11
β’ ((π’ β (π β {π}) β§ π£ β (π β {π})) β (π’ β π β§ π£ β π)) |
87 | 1, 2, 4 | rngocl 36363 |
. . . . . . . . . . . 12
β’ ((π
β RingOps β§ π’ β π β§ π£ β π) β (π’π»π£) β π) |
88 | 87 | 3expb 1121 |
. . . . . . . . . . 11
β’ ((π
β RingOps β§ (π’ β π β§ π£ β π)) β (π’π»π£) β π) |
89 | 86, 88 | sylan2 594 |
. . . . . . . . . 10
β’ ((π
β RingOps β§ (π’ β (π β {π}) β§ π£ β (π β {π}))) β (π’π»π£) β π) |
90 | 89 | adantlr 714 |
. . . . . . . . 9
β’ (((π
β RingOps β§ (π β π β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π)) β§ (π’ β (π β {π}) β§ π£ β (π β {π}))) β (π’π»π£) β π) |
91 | | oveq2 7366 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π’ β (π¦π»π₯) = (π¦π»π’)) |
92 | 91 | eqeq1d 2739 |
. . . . . . . . . . . . . . 15
β’ (π₯ = π’ β ((π¦π»π₯) = π β (π¦π»π’) = π)) |
93 | 92 | rexbidv 3176 |
. . . . . . . . . . . . . 14
β’ (π₯ = π’ β (βπ¦ β (π β {π})(π¦π»π₯) = π β βπ¦ β (π β {π})(π¦π»π’) = π)) |
94 | 93 | rspcv 3578 |
. . . . . . . . . . . . 13
β’ (π’ β (π β {π}) β (βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π β βπ¦ β (π β {π})(π¦π»π’) = π)) |
95 | 94 | imdistanri 571 |
. . . . . . . . . . . 12
β’
((βπ₯ β
(π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π β§ π’ β (π β {π})) β (βπ¦ β (π β {π})(π¦π»π’) = π β§ π’ β (π β {π}))) |
96 | | eldifsn 4748 |
. . . . . . . . . . . . . . 15
β’ (π£ β (π β {π}) β (π£ β π β§ π£ β π)) |
97 | | ssrexv 4012 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β {π}) β π β (βπ¦ β (π β {π})(π¦π»π’) = π β βπ¦ β π (π¦π»π’) = π)) |
98 | 11, 97 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(βπ¦ β
(π β {π})(π¦π»π’) = π β βπ¦ β π (π¦π»π’) = π) |
99 | 1, 2, 3, 4, 6 | zerdivemp1x 36409 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π
β RingOps β§ π’ β π β§ βπ¦ β π (π¦π»π’) = π) β (π£ β π β ((π’π»π£) = π β π£ = π))) |
100 | 98, 99 | syl3an3 1166 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π
β RingOps β§ π’ β π β§ βπ¦ β (π β {π})(π¦π»π’) = π) β (π£ β π β ((π’π»π£) = π β π£ = π))) |
101 | 84, 100 | syl3an2 1165 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π
β RingOps β§ π’ β (π β {π}) β§ βπ¦ β (π β {π})(π¦π»π’) = π) β (π£ β π β ((π’π»π£) = π β π£ = π))) |
102 | 101 | 3expb 1121 |
. . . . . . . . . . . . . . . . . 18
β’ ((π
β RingOps β§ (π’ β (π β {π}) β§ βπ¦ β (π β {π})(π¦π»π’) = π)) β (π£ β π β ((π’π»π£) = π β π£ = π))) |
103 | 102 | imp 408 |
. . . . . . . . . . . . . . . . 17
β’ (((π
β RingOps β§ (π’ β (π β {π}) β§ βπ¦ β (π β {π})(π¦π»π’) = π)) β§ π£ β π) β ((π’π»π£) = π β π£ = π)) |
104 | 103 | necon3d 2965 |
. . . . . . . . . . . . . . . 16
β’ (((π
β RingOps β§ (π’ β (π β {π}) β§ βπ¦ β (π β {π})(π¦π»π’) = π)) β§ π£ β π) β (π£ β π β (π’π»π£) β π)) |
105 | 104 | impr 456 |
. . . . . . . . . . . . . . 15
β’ (((π
β RingOps β§ (π’ β (π β {π}) β§ βπ¦ β (π β {π})(π¦π»π’) = π)) β§ (π£ β π β§ π£ β π)) β (π’π»π£) β π) |
106 | 96, 105 | sylan2b 595 |
. . . . . . . . . . . . . 14
β’ (((π
β RingOps β§ (π’ β (π β {π}) β§ βπ¦ β (π β {π})(π¦π»π’) = π)) β§ π£ β (π β {π})) β (π’π»π£) β π) |
107 | 106 | an32s 651 |
. . . . . . . . . . . . 13
β’ (((π
β RingOps β§ π£ β (π β {π})) β§ (π’ β (π β {π}) β§ βπ¦ β (π β {π})(π¦π»π’) = π)) β (π’π»π£) β π) |
108 | 107 | ancom2s 649 |
. . . . . . . . . . . 12
β’ (((π
β RingOps β§ π£ β (π β {π})) β§ (βπ¦ β (π β {π})(π¦π»π’) = π β§ π’ β (π β {π}))) β (π’π»π£) β π) |
109 | 95, 108 | sylan2 594 |
. . . . . . . . . . 11
β’ (((π
β RingOps β§ π£ β (π β {π})) β§ (βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π β§ π’ β (π β {π}))) β (π’π»π£) β π) |
110 | 109 | an42s 660 |
. . . . . . . . . 10
β’ (((π
β RingOps β§
βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π) β§ (π’ β (π β {π}) β§ π£ β (π β {π}))) β (π’π»π£) β π) |
111 | 110 | adantlrl 719 |
. . . . . . . . 9
β’ (((π
β RingOps β§ (π β π β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π)) β§ (π’ β (π β {π}) β§ π£ β (π β {π}))) β (π’π»π£) β π) |
112 | | eldifsn 4748 |
. . . . . . . . 9
β’ ((π’π»π£) β (π β {π}) β ((π’π»π£) β π β§ (π’π»π£) β π)) |
113 | 90, 111, 112 | sylanbrc 584 |
. . . . . . . 8
β’ (((π
β RingOps β§ (π β π β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π)) β§ (π’ β (π β {π}) β§ π£ β (π β {π}))) β (π’π»π£) β (π β {π})) |
114 | 83, 113 | eqeltrd 2838 |
. . . . . . 7
β’ (((π
β RingOps β§ (π β π β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π)) β§ (π’ β (π β {π}) β§ π£ β (π β {π}))) β (π’(π» βΎ ((π β {π}) Γ (π β {π})))π£) β (π β {π})) |
115 | 114 | ralrimivva 3198 |
. . . . . 6
β’ ((π
β RingOps β§ (π β π β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π)) β βπ’ β (π β {π})βπ£ β (π β {π})(π’(π» βΎ ((π β {π}) Γ (π β {π})))π£) β (π β {π})) |
116 | | ffnov 7484 |
. . . . . 6
β’ ((π» βΎ ((π β {π}) Γ (π β {π}))):((π β {π}) Γ (π β {π}))βΆ(π β {π}) β ((π» βΎ ((π β {π}) Γ (π β {π}))) Fn ((π β {π}) Γ (π β {π})) β§ βπ’ β (π β {π})βπ£ β (π β {π})(π’(π» βΎ ((π β {π}) Γ (π β {π})))π£) β (π β {π}))) |
117 | 81, 115, 116 | sylanbrc 584 |
. . . . 5
β’ ((π
β RingOps β§ (π β π β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π)) β (π» βΎ ((π β {π}) Γ (π β {π}))):((π β {π}) Γ (π β {π}))βΆ(π β {π})) |
118 | 113 | 3adantr3 1172 |
. . . . . . 7
β’ (((π
β RingOps β§ (π β π β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π)) β§ (π’ β (π β {π}) β§ π£ β (π β {π}) β§ π€ β (π β {π}))) β (π’π»π£) β (π β {π})) |
119 | | simpr3 1197 |
. . . . . . 7
β’ (((π
β RingOps β§ (π β π β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π)) β§ (π’ β (π β {π}) β§ π£ β (π β {π}) β§ π€ β (π β {π}))) β π€ β (π β {π})) |
120 | 118, 119 | ovresd 7522 |
. . . . . 6
β’ (((π
β RingOps β§ (π β π β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π)) β§ (π’ β (π β {π}) β§ π£ β (π β {π}) β§ π€ β (π β {π}))) β ((π’π»π£)(π» βΎ ((π β {π}) Γ (π β {π})))π€) = ((π’π»π£)π»π€)) |
121 | 82 | 3adant3 1133 |
. . . . . . . 8
β’ ((π’ β (π β {π}) β§ π£ β (π β {π}) β§ π€ β (π β {π})) β (π’(π» βΎ ((π β {π}) Γ (π β {π})))π£) = (π’π»π£)) |
122 | 121 | adantl 483 |
. . . . . . 7
β’ (((π
β RingOps β§ (π β π β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π)) β§ (π’ β (π β {π}) β§ π£ β (π β {π}) β§ π€ β (π β {π}))) β (π’(π» βΎ ((π β {π}) Γ (π β {π})))π£) = (π’π»π£)) |
123 | 122 | oveq1d 7373 |
. . . . . 6
β’ (((π
β RingOps β§ (π β π β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π)) β§ (π’ β (π β {π}) β§ π£ β (π β {π}) β§ π€ β (π β {π}))) β ((π’(π» βΎ ((π β {π}) Γ (π β {π})))π£)(π» βΎ ((π β {π}) Γ (π β {π})))π€) = ((π’π»π£)(π» βΎ ((π β {π}) Γ (π β {π})))π€)) |
124 | | ovres 7521 |
. . . . . . . . . 10
β’ ((π£ β (π β {π}) β§ π€ β (π β {π})) β (π£(π» βΎ ((π β {π}) Γ (π β {π})))π€) = (π£π»π€)) |
125 | 124 | 3adant1 1131 |
. . . . . . . . 9
β’ ((π’ β (π β {π}) β§ π£ β (π β {π}) β§ π€ β (π β {π})) β (π£(π» βΎ ((π β {π}) Γ (π β {π})))π€) = (π£π»π€)) |
126 | 125 | adantl 483 |
. . . . . . . 8
β’ (((π
β RingOps β§ (π β π β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π)) β§ (π’ β (π β {π}) β§ π£ β (π β {π}) β§ π€ β (π β {π}))) β (π£(π» βΎ ((π β {π}) Γ (π β {π})))π€) = (π£π»π€)) |
127 | 126 | oveq2d 7374 |
. . . . . . 7
β’ (((π
β RingOps β§ (π β π β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π)) β§ (π’ β (π β {π}) β§ π£ β (π β {π}) β§ π€ β (π β {π}))) β (π’π»(π£(π» βΎ ((π β {π}) Γ (π β {π})))π€)) = (π’π»(π£π»π€))) |
128 | | simpr1 1195 |
. . . . . . . 8
β’ (((π
β RingOps β§ (π β π β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π)) β§ (π’ β (π β {π}) β§ π£ β (π β {π}) β§ π€ β (π β {π}))) β π’ β (π β {π})) |
129 | | fovcdm 7525 |
. . . . . . . . . 10
β’ (((π» βΎ ((π β {π}) Γ (π β {π}))):((π β {π}) Γ (π β {π}))βΆ(π β {π}) β§ π£ β (π β {π}) β§ π€ β (π β {π})) β (π£(π» βΎ ((π β {π}) Γ (π β {π})))π€) β (π β {π})) |
130 | 129 | 3adant3r1 1183 |
. . . . . . . . 9
β’ (((π» βΎ ((π β {π}) Γ (π β {π}))):((π β {π}) Γ (π β {π}))βΆ(π β {π}) β§ (π’ β (π β {π}) β§ π£ β (π β {π}) β§ π€ β (π β {π}))) β (π£(π» βΎ ((π β {π}) Γ (π β {π})))π€) β (π β {π})) |
131 | 117, 130 | sylan 581 |
. . . . . . . 8
β’ (((π
β RingOps β§ (π β π β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π)) β§ (π’ β (π β {π}) β§ π£ β (π β {π}) β§ π€ β (π β {π}))) β (π£(π» βΎ ((π β {π}) Γ (π β {π})))π€) β (π β {π})) |
132 | 128, 131 | ovresd 7522 |
. . . . . . 7
β’ (((π
β RingOps β§ (π β π β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π)) β§ (π’ β (π β {π}) β§ π£ β (π β {π}) β§ π€ β (π β {π}))) β (π’(π» βΎ ((π β {π}) Γ (π β {π})))(π£(π» βΎ ((π β {π}) Γ (π β {π})))π€)) = (π’π»(π£(π» βΎ ((π β {π}) Γ (π β {π})))π€))) |
133 | | eldifi 4087 |
. . . . . . . . . 10
β’ (π€ β (π β {π}) β π€ β π) |
134 | 84, 85, 133 | 3anim123i 1152 |
. . . . . . . . 9
β’ ((π’ β (π β {π}) β§ π£ β (π β {π}) β§ π€ β (π β {π})) β (π’ β π β§ π£ β π β§ π€ β π)) |
135 | 1, 2, 4 | rngoass 36368 |
. . . . . . . . 9
β’ ((π
β RingOps β§ (π’ β π β§ π£ β π β§ π€ β π)) β ((π’π»π£)π»π€) = (π’π»(π£π»π€))) |
136 | 134, 135 | sylan2 594 |
. . . . . . . 8
β’ ((π
β RingOps β§ (π’ β (π β {π}) β§ π£ β (π β {π}) β§ π€ β (π β {π}))) β ((π’π»π£)π»π€) = (π’π»(π£π»π€))) |
137 | 136 | adantlr 714 |
. . . . . . 7
β’ (((π
β RingOps β§ (π β π β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π)) β§ (π’ β (π β {π}) β§ π£ β (π β {π}) β§ π€ β (π β {π}))) β ((π’π»π£)π»π€) = (π’π»(π£π»π€))) |
138 | 127, 132,
137 | 3eqtr4d 2787 |
. . . . . 6
β’ (((π
β RingOps β§ (π β π β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π)) β§ (π’ β (π β {π}) β§ π£ β (π β {π}) β§ π€ β (π β {π}))) β (π’(π» βΎ ((π β {π}) Γ (π β {π})))(π£(π» βΎ ((π β {π}) Γ (π β {π})))π€)) = ((π’π»π£)π»π€)) |
139 | 120, 123,
138 | 3eqtr4d 2787 |
. . . . 5
β’ (((π
β RingOps β§ (π β π β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π)) β§ (π’ β (π β {π}) β§ π£ β (π β {π}) β§ π€ β (π β {π}))) β ((π’(π» βΎ ((π β {π}) Γ (π β {π})))π£)(π» βΎ ((π β {π}) Γ (π β {π})))π€) = (π’(π» βΎ ((π β {π}) Γ (π β {π})))(π£(π» βΎ ((π β {π}) Γ (π β {π})))π€))) |
140 | 43 | anim1i 616 |
. . . . . . 7
β’ ((π
β RingOps β§ π β π) β (π β π β§ π β π)) |
141 | 140, 45 | sylibr 233 |
. . . . . 6
β’ ((π
β RingOps β§ π β π) β π β (π β {π})) |
142 | 141 | adantrr 716 |
. . . . 5
β’ ((π
β RingOps β§ (π β π β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π)) β π β (π β {π})) |
143 | | ovres 7521 |
. . . . . . . 8
β’ ((π β (π β {π}) β§ π’ β (π β {π})) β (π(π» βΎ ((π β {π}) Γ (π β {π})))π’) = (ππ»π’)) |
144 | 141, 143 | sylan 581 |
. . . . . . 7
β’ (((π
β RingOps β§ π β π) β§ π’ β (π β {π})) β (π(π» βΎ ((π β {π}) Γ (π β {π})))π’) = (ππ»π’)) |
145 | 2, 42, 6 | rngolidm 36399 |
. . . . . . . . 9
β’ ((π
β RingOps β§ π’ β π) β (ππ»π’) = π’) |
146 | 84, 145 | sylan2 594 |
. . . . . . . 8
β’ ((π
β RingOps β§ π’ β (π β {π})) β (ππ»π’) = π’) |
147 | 146 | adantlr 714 |
. . . . . . 7
β’ (((π
β RingOps β§ π β π) β§ π’ β (π β {π})) β (ππ»π’) = π’) |
148 | 144, 147 | eqtrd 2777 |
. . . . . 6
β’ (((π
β RingOps β§ π β π) β§ π’ β (π β {π})) β (π(π» βΎ ((π β {π}) Γ (π β {π})))π’) = π’) |
149 | 148 | adantlrr 720 |
. . . . 5
β’ (((π
β RingOps β§ (π β π β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π)) β§ π’ β (π β {π})) β (π(π» βΎ ((π β {π}) Γ (π β {π})))π’) = π’) |
150 | 93 | rspcva 3580 |
. . . . . . . . 9
β’ ((π’ β (π β {π}) β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π) β βπ¦ β (π β {π})(π¦π»π’) = π) |
151 | | oveq1 7365 |
. . . . . . . . . . . 12
β’ (π¦ = π§ β (π¦π»π’) = (π§π»π’)) |
152 | 151 | eqeq1d 2739 |
. . . . . . . . . . 11
β’ (π¦ = π§ β ((π¦π»π’) = π β (π§π»π’) = π)) |
153 | 152 | cbvrexvw 3227 |
. . . . . . . . . 10
β’
(βπ¦ β
(π β {π})(π¦π»π’) = π β βπ§ β (π β {π})(π§π»π’) = π) |
154 | | ovres 7521 |
. . . . . . . . . . . . . 14
β’ ((π§ β (π β {π}) β§ π’ β (π β {π})) β (π§(π» βΎ ((π β {π}) Γ (π β {π})))π’) = (π§π»π’)) |
155 | 154 | eqeq1d 2739 |
. . . . . . . . . . . . 13
β’ ((π§ β (π β {π}) β§ π’ β (π β {π})) β ((π§(π» βΎ ((π β {π}) Γ (π β {π})))π’) = π β (π§π»π’) = π)) |
156 | 155 | ancoms 460 |
. . . . . . . . . . . 12
β’ ((π’ β (π β {π}) β§ π§ β (π β {π})) β ((π§(π» βΎ ((π β {π}) Γ (π β {π})))π’) = π β (π§π»π’) = π)) |
157 | 156 | rexbidva 3174 |
. . . . . . . . . . 11
β’ (π’ β (π β {π}) β (βπ§ β (π β {π})(π§(π» βΎ ((π β {π}) Γ (π β {π})))π’) = π β βπ§ β (π β {π})(π§π»π’) = π)) |
158 | 157 | biimpar 479 |
. . . . . . . . . 10
β’ ((π’ β (π β {π}) β§ βπ§ β (π β {π})(π§π»π’) = π) β βπ§ β (π β {π})(π§(π» βΎ ((π β {π}) Γ (π β {π})))π’) = π) |
159 | 153, 158 | sylan2b 595 |
. . . . . . . . 9
β’ ((π’ β (π β {π}) β§ βπ¦ β (π β {π})(π¦π»π’) = π) β βπ§ β (π β {π})(π§(π» βΎ ((π β {π}) Γ (π β {π})))π’) = π) |
160 | 150, 159 | syldan 592 |
. . . . . . . 8
β’ ((π’ β (π β {π}) β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π) β βπ§ β (π β {π})(π§(π» βΎ ((π β {π}) Γ (π β {π})))π’) = π) |
161 | 160 | ancoms 460 |
. . . . . . 7
β’
((βπ₯ β
(π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π β§ π’ β (π β {π})) β βπ§ β (π β {π})(π§(π» βΎ ((π β {π}) Γ (π β {π})))π’) = π) |
162 | 161 | adantll 713 |
. . . . . 6
β’ (((π
β RingOps β§
βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π) β§ π’ β (π β {π})) β βπ§ β (π β {π})(π§(π» βΎ ((π β {π}) Γ (π β {π})))π’) = π) |
163 | 162 | adantlrl 719 |
. . . . 5
β’ (((π
β RingOps β§ (π β π β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π)) β§ π’ β (π β {π})) β βπ§ β (π β {π})(π§(π» βΎ ((π β {π}) Γ (π β {π})))π’) = π) |
164 | 77, 117, 139, 142, 149, 163 | isgrpda 36417 |
. . . 4
β’ ((π
β RingOps β§ (π β π β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π)) β (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp) |
165 | 72, 164 | impbida 800 |
. . 3
β’ (π
β RingOps β ((π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp β (π β π β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π))) |
166 | 165 | pm5.32i 576 |
. 2
β’ ((π
β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp) β (π
β RingOps β§ (π β π β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π))) |
167 | 5, 166 | bitri 275 |
1
β’ (π
β DivRingOps β (π
β RingOps β§ (π β π β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π))) |