Step | Hyp | Ref
| Expression |
1 | | rngunsnply.s |
. . 3
β’ (π β π =
((RingSpanββfld)β(π΅ βͺ {π}))) |
2 | 1 | eleq2d 2820 |
. 2
β’ (π β (π β π β π β
((RingSpanββfld)β(π΅ βͺ {π})))) |
3 | | cnring 20835 |
. . . . . . 7
β’
βfld β Ring |
4 | 3 | a1i 11 |
. . . . . 6
β’ (π β βfld
β Ring) |
5 | | cnfldbas 20816 |
. . . . . . 7
β’ β =
(Baseββfld) |
6 | 5 | a1i 11 |
. . . . . 6
β’ (π β β =
(Baseββfld)) |
7 | | rngunsnply.b |
. . . . . . . 8
β’ (π β π΅ β
(SubRingββfld)) |
8 | 5 | subrgss 20237 |
. . . . . . . 8
β’ (π΅ β
(SubRingββfld) β π΅ β β) |
9 | 7, 8 | syl 17 |
. . . . . . 7
β’ (π β π΅ β β) |
10 | | rngunsnply.x |
. . . . . . . 8
β’ (π β π β β) |
11 | 10 | snssd 4770 |
. . . . . . 7
β’ (π β {π} β β) |
12 | 9, 11 | unssd 4147 |
. . . . . 6
β’ (π β (π΅ βͺ {π}) β β) |
13 | | eqidd 2734 |
. . . . . 6
β’ (π β
(RingSpanββfld) =
(RingSpanββfld)) |
14 | | eqidd 2734 |
. . . . . 6
β’ (π β
((RingSpanββfld)β(π΅ βͺ {π})) =
((RingSpanββfld)β(π΅ βͺ {π}))) |
15 | | eqidd 2734 |
. . . . . . 7
β’ (π β (βfld
βΎs {π
β£ βπ β
(Polyβπ΅)π = (πβπ)}) = (βfld
βΎs {π
β£ βπ β
(Polyβπ΅)π = (πβπ)})) |
16 | | cnfld0 20837 |
. . . . . . . 8
β’ 0 =
(0gββfld) |
17 | 16 | a1i 11 |
. . . . . . 7
β’ (π β 0 =
(0gββfld)) |
18 | | cnfldadd 20817 |
. . . . . . . 8
β’ + =
(+gββfld) |
19 | 18 | a1i 11 |
. . . . . . 7
β’ (π β + =
(+gββfld)) |
20 | | plyf 25575 |
. . . . . . . . . . . 12
β’ (π β (Polyβπ΅) β π:ββΆβ) |
21 | | ffvelcdm 7033 |
. . . . . . . . . . . 12
β’ ((π:ββΆβ β§
π β β) β
(πβπ) β β) |
22 | 20, 10, 21 | syl2anr 598 |
. . . . . . . . . . 11
β’ ((π β§ π β (Polyβπ΅)) β (πβπ) β β) |
23 | | eleq1 2822 |
. . . . . . . . . . 11
β’ (π = (πβπ) β (π β β β (πβπ) β β)) |
24 | 22, 23 | syl5ibrcom 247 |
. . . . . . . . . 10
β’ ((π β§ π β (Polyβπ΅)) β (π = (πβπ) β π β β)) |
25 | 24 | rexlimdva 3149 |
. . . . . . . . 9
β’ (π β (βπ β (Polyβπ΅)π = (πβπ) β π β β)) |
26 | 25 | ss2abdv 4021 |
. . . . . . . 8
β’ (π β {π β£ βπ β (Polyβπ΅)π = (πβπ)} β {π β£ π β β}) |
27 | | abid2 2872 |
. . . . . . . . 9
β’ {π β£ π β β} = β |
28 | 27, 5 | eqtri 2761 |
. . . . . . . 8
β’ {π β£ π β β} =
(Baseββfld) |
29 | 26, 28 | sseqtrdi 3995 |
. . . . . . 7
β’ (π β {π β£ βπ β (Polyβπ΅)π = (πβπ)} β
(Baseββfld)) |
30 | | abid2 2872 |
. . . . . . . . 9
β’ {π β£ π β π΅} = π΅ |
31 | | plyconst 25583 |
. . . . . . . . . . . . 13
β’ ((π΅ β β β§ π β π΅) β (β Γ {π}) β (Polyβπ΅)) |
32 | 9, 31 | sylan 581 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΅) β (β Γ {π}) β (Polyβπ΅)) |
33 | 10 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΅) β π β β) |
34 | | vex 3448 |
. . . . . . . . . . . . . . 15
β’ π β V |
35 | 34 | fvconst2 7154 |
. . . . . . . . . . . . . 14
β’ (π β β β ((β
Γ {π})βπ) = π) |
36 | 33, 35 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π΅) β ((β Γ {π})βπ) = π) |
37 | 36 | eqcomd 2739 |
. . . . . . . . . . . 12
β’ ((π β§ π β π΅) β π = ((β Γ {π})βπ)) |
38 | | fveq1 6842 |
. . . . . . . . . . . . 13
β’ (π = (β Γ {π}) β (πβπ) = ((β Γ {π})βπ)) |
39 | 38 | rspceeqv 3596 |
. . . . . . . . . . . 12
β’
(((β Γ {π}) β (Polyβπ΅) β§ π = ((β Γ {π})βπ)) β βπ β (Polyβπ΅)π = (πβπ)) |
40 | 32, 37, 39 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ π β π΅) β βπ β (Polyβπ΅)π = (πβπ)) |
41 | 40 | ex 414 |
. . . . . . . . . 10
β’ (π β (π β π΅ β βπ β (Polyβπ΅)π = (πβπ))) |
42 | 41 | ss2abdv 4021 |
. . . . . . . . 9
β’ (π β {π β£ π β π΅} β {π β£ βπ β (Polyβπ΅)π = (πβπ)}) |
43 | 30, 42 | eqsstrrid 3994 |
. . . . . . . 8
β’ (π β π΅ β {π β£ βπ β (Polyβπ΅)π = (πβπ)}) |
44 | | subrgsubg 20242 |
. . . . . . . . . 10
β’ (π΅ β
(SubRingββfld) β π΅ β
(SubGrpββfld)) |
45 | 7, 44 | syl 17 |
. . . . . . . . 9
β’ (π β π΅ β
(SubGrpββfld)) |
46 | 16 | subg0cl 18941 |
. . . . . . . . 9
β’ (π΅ β
(SubGrpββfld) β 0 β π΅) |
47 | 45, 46 | syl 17 |
. . . . . . . 8
β’ (π β 0 β π΅) |
48 | 43, 47 | sseldd 3946 |
. . . . . . 7
β’ (π β 0 β {π β£ βπ β (Polyβπ΅)π = (πβπ)}) |
49 | | biid 261 |
. . . . . . . . 9
β’ (π β π) |
50 | | vex 3448 |
. . . . . . . . . 10
β’ π β V |
51 | | eqeq1 2737 |
. . . . . . . . . . . 12
β’ (π = π β (π = (πβπ) β π = (πβπ))) |
52 | 51 | rexbidv 3172 |
. . . . . . . . . . 11
β’ (π = π β (βπ β (Polyβπ΅)π = (πβπ) β βπ β (Polyβπ΅)π = (πβπ))) |
53 | | fveq1 6842 |
. . . . . . . . . . . . 13
β’ (π = π β (πβπ) = (πβπ)) |
54 | 53 | eqeq2d 2744 |
. . . . . . . . . . . 12
β’ (π = π β (π = (πβπ) β π = (πβπ))) |
55 | 54 | cbvrexvw 3225 |
. . . . . . . . . . 11
β’
(βπ β
(Polyβπ΅)π = (πβπ) β βπ β (Polyβπ΅)π = (πβπ)) |
56 | 52, 55 | bitrdi 287 |
. . . . . . . . . 10
β’ (π = π β (βπ β (Polyβπ΅)π = (πβπ) β βπ β (Polyβπ΅)π = (πβπ))) |
57 | 50, 56 | elab 3631 |
. . . . . . . . 9
β’ (π β {π β£ βπ β (Polyβπ΅)π = (πβπ)} β βπ β (Polyβπ΅)π = (πβπ)) |
58 | | vex 3448 |
. . . . . . . . . 10
β’ π β V |
59 | | eqeq1 2737 |
. . . . . . . . . . . 12
β’ (π = π β (π = (πβπ) β π = (πβπ))) |
60 | 59 | rexbidv 3172 |
. . . . . . . . . . 11
β’ (π = π β (βπ β (Polyβπ΅)π = (πβπ) β βπ β (Polyβπ΅)π = (πβπ))) |
61 | | fveq1 6842 |
. . . . . . . . . . . . 13
β’ (π = π β (πβπ) = (πβπ)) |
62 | 61 | eqeq2d 2744 |
. . . . . . . . . . . 12
β’ (π = π β (π = (πβπ) β π = (πβπ))) |
63 | 62 | cbvrexvw 3225 |
. . . . . . . . . . 11
β’
(βπ β
(Polyβπ΅)π = (πβπ) β βπ β (Polyβπ΅)π = (πβπ)) |
64 | 60, 63 | bitrdi 287 |
. . . . . . . . . 10
β’ (π = π β (βπ β (Polyβπ΅)π = (πβπ) β βπ β (Polyβπ΅)π = (πβπ))) |
65 | 58, 64 | elab 3631 |
. . . . . . . . 9
β’ (π β {π β£ βπ β (Polyβπ΅)π = (πβπ)} β βπ β (Polyβπ΅)π = (πβπ)) |
66 | | simplr 768 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (Polyβπ΅)) β§ π β (Polyβπ΅)) β π β (Polyβπ΅)) |
67 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (Polyβπ΅)) β§ π β (Polyβπ΅)) β π β (Polyβπ΅)) |
68 | 18 | subrgacl 20247 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π΅ β
(SubRingββfld) β§ π β π΅ β§ π β π΅) β (π + π) β π΅) |
69 | 68 | 3expb 1121 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π΅ β
(SubRingββfld) β§ (π β π΅ β§ π β π΅)) β (π + π) β π΅) |
70 | 7, 69 | sylan 581 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π + π) β π΅) |
71 | 70 | adantlr 714 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (Polyβπ΅)) β§ (π β π΅ β§ π β π΅)) β (π + π) β π΅) |
72 | 71 | adantlr 714 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (Polyβπ΅)) β§ π β (Polyβπ΅)) β§ (π β π΅ β§ π β π΅)) β (π + π) β π΅) |
73 | 66, 67, 72 | plyadd 25594 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (Polyβπ΅)) β§ π β (Polyβπ΅)) β (π βf + π) β (Polyβπ΅)) |
74 | | plyf 25575 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (Polyβπ΅) β π:ββΆβ) |
75 | 74 | ffnd 6670 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (Polyβπ΅) β π Fn β) |
76 | 75 | ad2antlr 726 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (Polyβπ΅)) β§ π β (Polyβπ΅)) β π Fn β) |
77 | | plyf 25575 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (Polyβπ΅) β π:ββΆβ) |
78 | 77 | ffnd 6670 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (Polyβπ΅) β π Fn β) |
79 | 78 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (Polyβπ΅)) β§ π β (Polyβπ΅)) β π Fn β) |
80 | | cnex 11137 |
. . . . . . . . . . . . . . . . . 18
β’ β
β V |
81 | 80 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (Polyβπ΅)) β§ π β (Polyβπ΅)) β β β V) |
82 | 10 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β (Polyβπ΅)) β§ π β (Polyβπ΅)) β π β β) |
83 | | fnfvof 7635 |
. . . . . . . . . . . . . . . . 17
β’ (((π Fn β β§ π Fn β) β§ (β
β V β§ π β
β)) β ((π
βf + π)βπ) = ((πβπ) + (πβπ))) |
84 | 76, 79, 81, 82, 83 | syl22anc 838 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (Polyβπ΅)) β§ π β (Polyβπ΅)) β ((π βf + π)βπ) = ((πβπ) + (πβπ))) |
85 | 84 | eqcomd 2739 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (Polyβπ΅)) β§ π β (Polyβπ΅)) β ((πβπ) + (πβπ)) = ((π βf + π)βπ)) |
86 | | fveq1 6842 |
. . . . . . . . . . . . . . . 16
β’ (π = (π βf + π) β (πβπ) = ((π βf + π)βπ)) |
87 | 86 | rspceeqv 3596 |
. . . . . . . . . . . . . . 15
β’ (((π βf + π) β (Polyβπ΅) β§ ((πβπ) + (πβπ)) = ((π βf + π)βπ)) β βπ β (Polyβπ΅)((πβπ) + (πβπ)) = (πβπ)) |
88 | 73, 85, 87 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (Polyβπ΅)) β§ π β (Polyβπ΅)) β βπ β (Polyβπ΅)((πβπ) + (πβπ)) = (πβπ)) |
89 | | oveq2 7366 |
. . . . . . . . . . . . . . . 16
β’ (π = (πβπ) β ((πβπ) + π) = ((πβπ) + (πβπ))) |
90 | 89 | eqeq1d 2735 |
. . . . . . . . . . . . . . 15
β’ (π = (πβπ) β (((πβπ) + π) = (πβπ) β ((πβπ) + (πβπ)) = (πβπ))) |
91 | 90 | rexbidv 3172 |
. . . . . . . . . . . . . 14
β’ (π = (πβπ) β (βπ β (Polyβπ΅)((πβπ) + π) = (πβπ) β βπ β (Polyβπ΅)((πβπ) + (πβπ)) = (πβπ))) |
92 | 88, 91 | syl5ibrcom 247 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (Polyβπ΅)) β§ π β (Polyβπ΅)) β (π = (πβπ) β βπ β (Polyβπ΅)((πβπ) + π) = (πβπ))) |
93 | 92 | rexlimdva 3149 |
. . . . . . . . . . . 12
β’ ((π β§ π β (Polyβπ΅)) β (βπ β (Polyβπ΅)π = (πβπ) β βπ β (Polyβπ΅)((πβπ) + π) = (πβπ))) |
94 | | oveq1 7365 |
. . . . . . . . . . . . . . 15
β’ (π = (πβπ) β (π + π) = ((πβπ) + π)) |
95 | 94 | eqeq1d 2735 |
. . . . . . . . . . . . . 14
β’ (π = (πβπ) β ((π + π) = (πβπ) β ((πβπ) + π) = (πβπ))) |
96 | 95 | rexbidv 3172 |
. . . . . . . . . . . . 13
β’ (π = (πβπ) β (βπ β (Polyβπ΅)(π + π) = (πβπ) β βπ β (Polyβπ΅)((πβπ) + π) = (πβπ))) |
97 | 96 | imbi2d 341 |
. . . . . . . . . . . 12
β’ (π = (πβπ) β ((βπ β (Polyβπ΅)π = (πβπ) β βπ β (Polyβπ΅)(π + π) = (πβπ)) β (βπ β (Polyβπ΅)π = (πβπ) β βπ β (Polyβπ΅)((πβπ) + π) = (πβπ)))) |
98 | 93, 97 | syl5ibrcom 247 |
. . . . . . . . . . 11
β’ ((π β§ π β (Polyβπ΅)) β (π = (πβπ) β (βπ β (Polyβπ΅)π = (πβπ) β βπ β (Polyβπ΅)(π + π) = (πβπ)))) |
99 | 98 | rexlimdva 3149 |
. . . . . . . . . 10
β’ (π β (βπ β (Polyβπ΅)π = (πβπ) β (βπ β (Polyβπ΅)π = (πβπ) β βπ β (Polyβπ΅)(π + π) = (πβπ)))) |
100 | 99 | 3imp 1112 |
. . . . . . . . 9
β’ ((π β§ βπ β (Polyβπ΅)π = (πβπ) β§ βπ β (Polyβπ΅)π = (πβπ)) β βπ β (Polyβπ΅)(π + π) = (πβπ)) |
101 | 49, 57, 65, 100 | syl3anb 1162 |
. . . . . . . 8
β’ ((π β§ π β {π β£ βπ β (Polyβπ΅)π = (πβπ)} β§ π β {π β£ βπ β (Polyβπ΅)π = (πβπ)}) β βπ β (Polyβπ΅)(π + π) = (πβπ)) |
102 | | ovex 7391 |
. . . . . . . . 9
β’ (π + π) β V |
103 | | eqeq1 2737 |
. . . . . . . . . 10
β’ (π = (π + π) β (π = (πβπ) β (π + π) = (πβπ))) |
104 | 103 | rexbidv 3172 |
. . . . . . . . 9
β’ (π = (π + π) β (βπ β (Polyβπ΅)π = (πβπ) β βπ β (Polyβπ΅)(π + π) = (πβπ))) |
105 | 102, 104 | elab 3631 |
. . . . . . . 8
β’ ((π + π) β {π β£ βπ β (Polyβπ΅)π = (πβπ)} β βπ β (Polyβπ΅)(π + π) = (πβπ)) |
106 | 101, 105 | sylibr 233 |
. . . . . . 7
β’ ((π β§ π β {π β£ βπ β (Polyβπ΅)π = (πβπ)} β§ π β {π β£ βπ β (Polyβπ΅)π = (πβπ)}) β (π + π) β {π β£ βπ β (Polyβπ΅)π = (πβπ)}) |
107 | | ax-1cn 11114 |
. . . . . . . . . . . . . . . . . 18
β’ 1 β
β |
108 | | cnfldneg 20839 |
. . . . . . . . . . . . . . . . . 18
β’ (1 β
β β ((invgββfld)β1) =
-1) |
109 | 107, 108 | mp1i 13 |
. . . . . . . . . . . . . . . . 17
β’ (π β
((invgββfld)β1) = -1) |
110 | | cnfld1 20838 |
. . . . . . . . . . . . . . . . . . . 20
β’ 1 =
(1rββfld) |
111 | 110 | subrg1cl 20244 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΅ β
(SubRingββfld) β 1 β π΅) |
112 | 7, 111 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β 1 β π΅) |
113 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . 19
β’
(invgββfld) =
(invgββfld) |
114 | 113 | subginvcl 18942 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΅ β
(SubGrpββfld) β§ 1 β π΅) β
((invgββfld)β1) β π΅) |
115 | 45, 112, 114 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ (π β
((invgββfld)β1) β π΅) |
116 | 109, 115 | eqeltrrd 2835 |
. . . . . . . . . . . . . . . 16
β’ (π β -1 β π΅) |
117 | | plyconst 25583 |
. . . . . . . . . . . . . . . 16
β’ ((π΅ β β β§ -1 β
π΅) β (β Γ
{-1}) β (Polyβπ΅)) |
118 | 9, 116, 117 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (π β (β Γ {-1})
β (Polyβπ΅)) |
119 | 118 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (Polyβπ΅)) β (β Γ {-1}) β
(Polyβπ΅)) |
120 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (Polyβπ΅)) β π β (Polyβπ΅)) |
121 | | cnfldmul 20818 |
. . . . . . . . . . . . . . . . . 18
β’ Β·
= (.rββfld) |
122 | 121 | subrgmcl 20248 |
. . . . . . . . . . . . . . . . 17
β’ ((π΅ β
(SubRingββfld) β§ π β π΅ β§ π β π΅) β (π Β· π) β π΅) |
123 | 122 | 3expb 1121 |
. . . . . . . . . . . . . . . 16
β’ ((π΅ β
(SubRingββfld) β§ (π β π΅ β§ π β π΅)) β (π Β· π) β π΅) |
124 | 7, 123 | sylan 581 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π Β· π) β π΅) |
125 | 124 | adantlr 714 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (Polyβπ΅)) β§ (π β π΅ β§ π β π΅)) β (π Β· π) β π΅) |
126 | 119, 120,
71, 125 | plymul 25595 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (Polyβπ΅)) β ((β Γ {-1})
βf Β· π) β (Polyβπ΅)) |
127 | | ffvelcdm 7033 |
. . . . . . . . . . . . . . . 16
β’ ((π:ββΆβ β§
π β β) β
(πβπ) β β) |
128 | 74, 10, 127 | syl2anr 598 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (Polyβπ΅)) β (πβπ) β β) |
129 | | cnfldneg 20839 |
. . . . . . . . . . . . . . 15
β’ ((πβπ) β β β
((invgββfld)β(πβπ)) = -(πβπ)) |
130 | 128, 129 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (Polyβπ΅)) β
((invgββfld)β(πβπ)) = -(πβπ)) |
131 | | negex 11404 |
. . . . . . . . . . . . . . . . 17
β’ -1 β
V |
132 | | fnconstg 6731 |
. . . . . . . . . . . . . . . . 17
β’ (-1
β V β (β Γ {-1}) Fn β) |
133 | 131, 132 | mp1i 13 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (Polyβπ΅)) β (β Γ {-1}) Fn
β) |
134 | 75 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (Polyβπ΅)) β π Fn β) |
135 | 80 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (Polyβπ΅)) β β β V) |
136 | 10 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (Polyβπ΅)) β π β β) |
137 | | fnfvof 7635 |
. . . . . . . . . . . . . . . 16
β’
((((β Γ {-1}) Fn β β§ π Fn β) β§ (β β V β§
π β β)) β
(((β Γ {-1}) βf Β· π)βπ) = (((β Γ {-1})βπ) Β· (πβπ))) |
138 | 133, 134,
135, 136, 137 | syl22anc 838 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (Polyβπ΅)) β (((β Γ {-1})
βf Β· π)βπ) = (((β Γ {-1})βπ) Β· (πβπ))) |
139 | 131 | fvconst2 7154 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β ((β
Γ {-1})βπ) =
-1) |
140 | 136, 139 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (Polyβπ΅)) β ((β Γ
{-1})βπ) =
-1) |
141 | 140 | oveq1d 7373 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (Polyβπ΅)) β (((β Γ
{-1})βπ) Β·
(πβπ)) = (-1 Β· (πβπ))) |
142 | 128 | mulm1d 11612 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (Polyβπ΅)) β (-1 Β· (πβπ)) = -(πβπ)) |
143 | 138, 141,
142 | 3eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (Polyβπ΅)) β (((β Γ {-1})
βf Β· π)βπ) = -(πβπ)) |
144 | 130, 143 | eqtr4d 2776 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (Polyβπ΅)) β
((invgββfld)β(πβπ)) = (((β Γ {-1})
βf Β· π)βπ)) |
145 | | fveq1 6842 |
. . . . . . . . . . . . . 14
β’ (π = ((β Γ {-1})
βf Β· π) β (πβπ) = (((β Γ {-1})
βf Β· π)βπ)) |
146 | 145 | rspceeqv 3596 |
. . . . . . . . . . . . 13
β’
((((β Γ {-1}) βf Β· π) β (Polyβπ΅) β§
((invgββfld)β(πβπ)) = (((β Γ {-1})
βf Β· π)βπ)) β βπ β (Polyβπ΅)((invgββfld)β(πβπ)) = (πβπ)) |
147 | 126, 144,
146 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π β (Polyβπ΅)) β βπ β (Polyβπ΅)((invgββfld)β(πβπ)) = (πβπ)) |
148 | | fveqeq2 6852 |
. . . . . . . . . . . . 13
β’ (π = (πβπ) β
(((invgββfld)βπ) = (πβπ) β
((invgββfld)β(πβπ)) = (πβπ))) |
149 | 148 | rexbidv 3172 |
. . . . . . . . . . . 12
β’ (π = (πβπ) β (βπ β (Polyβπ΅)((invgββfld)βπ) = (πβπ) β βπ β (Polyβπ΅)((invgββfld)β(πβπ)) = (πβπ))) |
150 | 147, 149 | syl5ibrcom 247 |
. . . . . . . . . . 11
β’ ((π β§ π β (Polyβπ΅)) β (π = (πβπ) β βπ β (Polyβπ΅)((invgββfld)βπ) = (πβπ))) |
151 | 150 | rexlimdva 3149 |
. . . . . . . . . 10
β’ (π β (βπ β (Polyβπ΅)π = (πβπ) β βπ β (Polyβπ΅)((invgββfld)βπ) = (πβπ))) |
152 | 151 | imp 408 |
. . . . . . . . 9
β’ ((π β§ βπ β (Polyβπ΅)π = (πβπ)) β βπ β (Polyβπ΅)((invgββfld)βπ) = (πβπ)) |
153 | 57, 152 | sylan2b 595 |
. . . . . . . 8
β’ ((π β§ π β {π β£ βπ β (Polyβπ΅)π = (πβπ)}) β βπ β (Polyβπ΅)((invgββfld)βπ) = (πβπ)) |
154 | | fvex 6856 |
. . . . . . . . 9
β’
((invgββfld)βπ) β V |
155 | | eqeq1 2737 |
. . . . . . . . . 10
β’ (π =
((invgββfld)βπ) β (π = (πβπ) β
((invgββfld)βπ) = (πβπ))) |
156 | 155 | rexbidv 3172 |
. . . . . . . . 9
β’ (π =
((invgββfld)βπ) β (βπ β (Polyβπ΅)π = (πβπ) β βπ β (Polyβπ΅)((invgββfld)βπ) = (πβπ))) |
157 | 154, 156 | elab 3631 |
. . . . . . . 8
β’
(((invgββfld)βπ) β {π β£ βπ β (Polyβπ΅)π = (πβπ)} β βπ β (Polyβπ΅)((invgββfld)βπ) = (πβπ)) |
158 | 153, 157 | sylibr 233 |
. . . . . . 7
β’ ((π β§ π β {π β£ βπ β (Polyβπ΅)π = (πβπ)}) β
((invgββfld)βπ) β {π β£ βπ β (Polyβπ΅)π = (πβπ)}) |
159 | 110 | a1i 11 |
. . . . . . 7
β’ (π β 1 =
(1rββfld)) |
160 | 121 | a1i 11 |
. . . . . . 7
β’ (π β Β· =
(.rββfld)) |
161 | 43, 112 | sseldd 3946 |
. . . . . . 7
β’ (π β 1 β {π β£ βπ β (Polyβπ΅)π = (πβπ)}) |
162 | 125 | adantlr 714 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β (Polyβπ΅)) β§ π β (Polyβπ΅)) β§ (π β π΅ β§ π β π΅)) β (π Β· π) β π΅) |
163 | 66, 67, 72, 162 | plymul 25595 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (Polyβπ΅)) β§ π β (Polyβπ΅)) β (π βf Β· π) β (Polyβπ΅)) |
164 | | fnfvof 7635 |
. . . . . . . . . . . . . . . . 17
β’ (((π Fn β β§ π Fn β) β§ (β
β V β§ π β
β)) β ((π
βf Β· π)βπ) = ((πβπ) Β· (πβπ))) |
165 | 76, 79, 81, 82, 164 | syl22anc 838 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (Polyβπ΅)) β§ π β (Polyβπ΅)) β ((π βf Β· π)βπ) = ((πβπ) Β· (πβπ))) |
166 | 165 | eqcomd 2739 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (Polyβπ΅)) β§ π β (Polyβπ΅)) β ((πβπ) Β· (πβπ)) = ((π βf Β· π)βπ)) |
167 | | fveq1 6842 |
. . . . . . . . . . . . . . . 16
β’ (π = (π βf Β· π) β (πβπ) = ((π βf Β· π)βπ)) |
168 | 167 | rspceeqv 3596 |
. . . . . . . . . . . . . . 15
β’ (((π βf Β·
π) β (Polyβπ΅) β§ ((πβπ) Β· (πβπ)) = ((π βf Β· π)βπ)) β βπ β (Polyβπ΅)((πβπ) Β· (πβπ)) = (πβπ)) |
169 | 163, 166,
168 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (Polyβπ΅)) β§ π β (Polyβπ΅)) β βπ β (Polyβπ΅)((πβπ) Β· (πβπ)) = (πβπ)) |
170 | | oveq2 7366 |
. . . . . . . . . . . . . . . 16
β’ (π = (πβπ) β ((πβπ) Β· π) = ((πβπ) Β· (πβπ))) |
171 | 170 | eqeq1d 2735 |
. . . . . . . . . . . . . . 15
β’ (π = (πβπ) β (((πβπ) Β· π) = (πβπ) β ((πβπ) Β· (πβπ)) = (πβπ))) |
172 | 171 | rexbidv 3172 |
. . . . . . . . . . . . . 14
β’ (π = (πβπ) β (βπ β (Polyβπ΅)((πβπ) Β· π) = (πβπ) β βπ β (Polyβπ΅)((πβπ) Β· (πβπ)) = (πβπ))) |
173 | 169, 172 | syl5ibrcom 247 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (Polyβπ΅)) β§ π β (Polyβπ΅)) β (π = (πβπ) β βπ β (Polyβπ΅)((πβπ) Β· π) = (πβπ))) |
174 | 173 | rexlimdva 3149 |
. . . . . . . . . . . 12
β’ ((π β§ π β (Polyβπ΅)) β (βπ β (Polyβπ΅)π = (πβπ) β βπ β (Polyβπ΅)((πβπ) Β· π) = (πβπ))) |
175 | | oveq1 7365 |
. . . . . . . . . . . . . . 15
β’ (π = (πβπ) β (π Β· π) = ((πβπ) Β· π)) |
176 | 175 | eqeq1d 2735 |
. . . . . . . . . . . . . 14
β’ (π = (πβπ) β ((π Β· π) = (πβπ) β ((πβπ) Β· π) = (πβπ))) |
177 | 176 | rexbidv 3172 |
. . . . . . . . . . . . 13
β’ (π = (πβπ) β (βπ β (Polyβπ΅)(π Β· π) = (πβπ) β βπ β (Polyβπ΅)((πβπ) Β· π) = (πβπ))) |
178 | 177 | imbi2d 341 |
. . . . . . . . . . . 12
β’ (π = (πβπ) β ((βπ β (Polyβπ΅)π = (πβπ) β βπ β (Polyβπ΅)(π Β· π) = (πβπ)) β (βπ β (Polyβπ΅)π = (πβπ) β βπ β (Polyβπ΅)((πβπ) Β· π) = (πβπ)))) |
179 | 174, 178 | syl5ibrcom 247 |
. . . . . . . . . . 11
β’ ((π β§ π β (Polyβπ΅)) β (π = (πβπ) β (βπ β (Polyβπ΅)π = (πβπ) β βπ β (Polyβπ΅)(π Β· π) = (πβπ)))) |
180 | 179 | rexlimdva 3149 |
. . . . . . . . . 10
β’ (π β (βπ β (Polyβπ΅)π = (πβπ) β (βπ β (Polyβπ΅)π = (πβπ) β βπ β (Polyβπ΅)(π Β· π) = (πβπ)))) |
181 | 180 | 3imp 1112 |
. . . . . . . . 9
β’ ((π β§ βπ β (Polyβπ΅)π = (πβπ) β§ βπ β (Polyβπ΅)π = (πβπ)) β βπ β (Polyβπ΅)(π Β· π) = (πβπ)) |
182 | 49, 57, 65, 181 | syl3anb 1162 |
. . . . . . . 8
β’ ((π β§ π β {π β£ βπ β (Polyβπ΅)π = (πβπ)} β§ π β {π β£ βπ β (Polyβπ΅)π = (πβπ)}) β βπ β (Polyβπ΅)(π Β· π) = (πβπ)) |
183 | | ovex 7391 |
. . . . . . . . 9
β’ (π Β· π) β V |
184 | | eqeq1 2737 |
. . . . . . . . . 10
β’ (π = (π Β· π) β (π = (πβπ) β (π Β· π) = (πβπ))) |
185 | 184 | rexbidv 3172 |
. . . . . . . . 9
β’ (π = (π Β· π) β (βπ β (Polyβπ΅)π = (πβπ) β βπ β (Polyβπ΅)(π Β· π) = (πβπ))) |
186 | 183, 185 | elab 3631 |
. . . . . . . 8
β’ ((π Β· π) β {π β£ βπ β (Polyβπ΅)π = (πβπ)} β βπ β (Polyβπ΅)(π Β· π) = (πβπ)) |
187 | 182, 186 | sylibr 233 |
. . . . . . 7
β’ ((π β§ π β {π β£ βπ β (Polyβπ΅)π = (πβπ)} β§ π β {π β£ βπ β (Polyβπ΅)π = (πβπ)}) β (π Β· π) β {π β£ βπ β (Polyβπ΅)π = (πβπ)}) |
188 | 15, 17, 19, 29, 48, 106, 158, 159, 160, 161, 187, 4 | issubrngd2 20674 |
. . . . . 6
β’ (π β {π β£ βπ β (Polyβπ΅)π = (πβπ)} β
(SubRingββfld)) |
189 | | plyid 25586 |
. . . . . . . . . . 11
β’ ((π΅ β β β§ 1 β
π΅) β
Xp β (Polyβπ΅)) |
190 | 9, 112, 189 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β Xp
β (Polyβπ΅)) |
191 | | df-idp 25566 |
. . . . . . . . . . . 12
β’
Xp = ( I βΎ β) |
192 | 191 | fveq1i 6844 |
. . . . . . . . . . 11
β’
(Xpβπ) = (( I βΎ β)βπ) |
193 | | fvresi 7120 |
. . . . . . . . . . . 12
β’ (π β β β (( I
βΎ β)βπ) =
π) |
194 | 10, 193 | syl 17 |
. . . . . . . . . . 11
β’ (π β (( I βΎ
β)βπ) = π) |
195 | 192, 194 | eqtr2id 2786 |
. . . . . . . . . 10
β’ (π β π = (Xpβπ)) |
196 | | fveq1 6842 |
. . . . . . . . . . 11
β’ (π = Xp β
(πβπ) = (Xpβπ)) |
197 | 196 | rspceeqv 3596 |
. . . . . . . . . 10
β’
((Xp β (Polyβπ΅) β§ π = (Xpβπ)) β βπ β (Polyβπ΅)π = (πβπ)) |
198 | 190, 195,
197 | syl2anc 585 |
. . . . . . . . 9
β’ (π β βπ β (Polyβπ΅)π = (πβπ)) |
199 | | eqeq1 2737 |
. . . . . . . . . 10
β’ (π = π β (π = (πβπ) β π = (πβπ))) |
200 | 199 | rexbidv 3172 |
. . . . . . . . 9
β’ (π = π β (βπ β (Polyβπ΅)π = (πβπ) β βπ β (Polyβπ΅)π = (πβπ))) |
201 | 10, 198, 200 | elabd 3634 |
. . . . . . . 8
β’ (π β π β {π β£ βπ β (Polyβπ΅)π = (πβπ)}) |
202 | 201 | snssd 4770 |
. . . . . . 7
β’ (π β {π} β {π β£ βπ β (Polyβπ΅)π = (πβπ)}) |
203 | 43, 202 | unssd 4147 |
. . . . . 6
β’ (π β (π΅ βͺ {π}) β {π β£ βπ β (Polyβπ΅)π = (πβπ)}) |
204 | 4, 6, 12, 13, 14, 188, 203 | rgspnmin 41541 |
. . . . 5
β’ (π β
((RingSpanββfld)β(π΅ βͺ {π})) β {π β£ βπ β (Polyβπ΅)π = (πβπ)}) |
205 | 204 | sseld 3944 |
. . . 4
β’ (π β (π β
((RingSpanββfld)β(π΅ βͺ {π})) β π β {π β£ βπ β (Polyβπ΅)π = (πβπ)})) |
206 | | fvex 6856 |
. . . . . . 7
β’ (πβπ) β V |
207 | | eleq1 2822 |
. . . . . . 7
β’ (π = (πβπ) β (π β V β (πβπ) β V)) |
208 | 206, 207 | mpbiri 258 |
. . . . . 6
β’ (π = (πβπ) β π β V) |
209 | 208 | rexlimivw 3145 |
. . . . 5
β’
(βπ β
(Polyβπ΅)π = (πβπ) β π β V) |
210 | | eqeq1 2737 |
. . . . . 6
β’ (π = π β (π = (πβπ) β π = (πβπ))) |
211 | 210 | rexbidv 3172 |
. . . . 5
β’ (π = π β (βπ β (Polyβπ΅)π = (πβπ) β βπ β (Polyβπ΅)π = (πβπ))) |
212 | 209, 211 | elab3 3639 |
. . . 4
β’ (π β {π β£ βπ β (Polyβπ΅)π = (πβπ)} β βπ β (Polyβπ΅)π = (πβπ)) |
213 | 205, 212 | syl6ib 251 |
. . 3
β’ (π β (π β
((RingSpanββfld)β(π΅ βͺ {π})) β βπ β (Polyβπ΅)π = (πβπ))) |
214 | 4, 6, 12, 13, 14 | rgspncl 41539 |
. . . . . . 7
β’ (π β
((RingSpanββfld)β(π΅ βͺ {π})) β
(SubRingββfld)) |
215 | 214 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (Polyβπ΅)) β
((RingSpanββfld)β(π΅ βͺ {π})) β
(SubRingββfld)) |
216 | | simpr 486 |
. . . . . 6
β’ ((π β§ π β (Polyβπ΅)) β π β (Polyβπ΅)) |
217 | 4, 6, 12, 13, 14 | rgspnssid 41540 |
. . . . . . . . 9
β’ (π β (π΅ βͺ {π}) β
((RingSpanββfld)β(π΅ βͺ {π}))) |
218 | 217 | unssbd 4149 |
. . . . . . . 8
β’ (π β {π} β
((RingSpanββfld)β(π΅ βͺ {π}))) |
219 | | snidg 4621 |
. . . . . . . . 9
β’ (π β β β π β {π}) |
220 | 10, 219 | syl 17 |
. . . . . . . 8
β’ (π β π β {π}) |
221 | 218, 220 | sseldd 3946 |
. . . . . . 7
β’ (π β π β
((RingSpanββfld)β(π΅ βͺ {π}))) |
222 | 221 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (Polyβπ΅)) β π β
((RingSpanββfld)β(π΅ βͺ {π}))) |
223 | 217 | unssad 4148 |
. . . . . . 7
β’ (π β π΅ β
((RingSpanββfld)β(π΅ βͺ {π}))) |
224 | 223 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (Polyβπ΅)) β π΅ β
((RingSpanββfld)β(π΅ βͺ {π}))) |
225 | 215, 216,
222, 224 | cnsrplycl 41537 |
. . . . 5
β’ ((π β§ π β (Polyβπ΅)) β (πβπ) β
((RingSpanββfld)β(π΅ βͺ {π}))) |
226 | | eleq1 2822 |
. . . . 5
β’ (π = (πβπ) β (π β
((RingSpanββfld)β(π΅ βͺ {π})) β (πβπ) β
((RingSpanββfld)β(π΅ βͺ {π})))) |
227 | 225, 226 | syl5ibrcom 247 |
. . . 4
β’ ((π β§ π β (Polyβπ΅)) β (π = (πβπ) β π β
((RingSpanββfld)β(π΅ βͺ {π})))) |
228 | 227 | rexlimdva 3149 |
. . 3
β’ (π β (βπ β (Polyβπ΅)π = (πβπ) β π β
((RingSpanββfld)β(π΅ βͺ {π})))) |
229 | 213, 228 | impbid 211 |
. 2
β’ (π β (π β
((RingSpanββfld)β(π΅ βͺ {π})) β βπ β (Polyβπ΅)π = (πβπ))) |
230 | 2, 229 | bitrd 279 |
1
β’ (π β (π β π β βπ β (Polyβπ΅)π = (πβπ))) |