Step |
Hyp |
Ref |
Expression |
0 |
|
cdchr |
โข DChr |
1 |
|
vn |
โข ๐ |
2 |
|
cn |
โข โ |
3 |
|
czn |
โข โค/nโค |
4 |
1
|
cv |
โข ๐ |
5 |
4 3
|
cfv |
โข ( โค/nโค โ ๐ ) |
6 |
|
vz |
โข ๐ง |
7 |
|
vx |
โข ๐ฅ |
8 |
|
cmgp |
โข mulGrp |
9 |
6
|
cv |
โข ๐ง |
10 |
9 8
|
cfv |
โข ( mulGrp โ ๐ง ) |
11 |
|
cmhm |
โข MndHom |
12 |
|
ccnfld |
โข โfld |
13 |
12 8
|
cfv |
โข ( mulGrp โ โfld ) |
14 |
10 13 11
|
co |
โข ( ( mulGrp โ ๐ง ) MndHom ( mulGrp โ โfld ) ) |
15 |
|
cbs |
โข Base |
16 |
9 15
|
cfv |
โข ( Base โ ๐ง ) |
17 |
|
cui |
โข Unit |
18 |
9 17
|
cfv |
โข ( Unit โ ๐ง ) |
19 |
16 18
|
cdif |
โข ( ( Base โ ๐ง ) โ ( Unit โ ๐ง ) ) |
20 |
|
cc0 |
โข 0 |
21 |
20
|
csn |
โข { 0 } |
22 |
19 21
|
cxp |
โข ( ( ( Base โ ๐ง ) โ ( Unit โ ๐ง ) ) ร { 0 } ) |
23 |
7
|
cv |
โข ๐ฅ |
24 |
22 23
|
wss |
โข ( ( ( Base โ ๐ง ) โ ( Unit โ ๐ง ) ) ร { 0 } ) โ ๐ฅ |
25 |
24 7 14
|
crab |
โข { ๐ฅ โ ( ( mulGrp โ ๐ง ) MndHom ( mulGrp โ โfld ) ) โฃ ( ( ( Base โ ๐ง ) โ ( Unit โ ๐ง ) ) ร { 0 } ) โ ๐ฅ } |
26 |
|
vb |
โข ๐ |
27 |
|
cnx |
โข ndx |
28 |
27 15
|
cfv |
โข ( Base โ ndx ) |
29 |
26
|
cv |
โข ๐ |
30 |
28 29
|
cop |
โข โจ ( Base โ ndx ) , ๐ โฉ |
31 |
|
cplusg |
โข +g |
32 |
27 31
|
cfv |
โข ( +g โ ndx ) |
33 |
|
cmul |
โข ยท |
34 |
33
|
cof |
โข โf ยท |
35 |
29 29
|
cxp |
โข ( ๐ ร ๐ ) |
36 |
34 35
|
cres |
โข ( โf ยท โพ ( ๐ ร ๐ ) ) |
37 |
32 36
|
cop |
โข โจ ( +g โ ndx ) , ( โf ยท โพ ( ๐ ร ๐ ) ) โฉ |
38 |
30 37
|
cpr |
โข { โจ ( Base โ ndx ) , ๐ โฉ , โจ ( +g โ ndx ) , ( โf ยท โพ ( ๐ ร ๐ ) ) โฉ } |
39 |
26 25 38
|
csb |
โข โฆ { ๐ฅ โ ( ( mulGrp โ ๐ง ) MndHom ( mulGrp โ โfld ) ) โฃ ( ( ( Base โ ๐ง ) โ ( Unit โ ๐ง ) ) ร { 0 } ) โ ๐ฅ } / ๐ โฆ { โจ ( Base โ ndx ) , ๐ โฉ , โจ ( +g โ ndx ) , ( โf ยท โพ ( ๐ ร ๐ ) ) โฉ } |
40 |
6 5 39
|
csb |
โข โฆ ( โค/nโค โ ๐ ) / ๐ง โฆ โฆ { ๐ฅ โ ( ( mulGrp โ ๐ง ) MndHom ( mulGrp โ โfld ) ) โฃ ( ( ( Base โ ๐ง ) โ ( Unit โ ๐ง ) ) ร { 0 } ) โ ๐ฅ } / ๐ โฆ { โจ ( Base โ ndx ) , ๐ โฉ , โจ ( +g โ ndx ) , ( โf ยท โพ ( ๐ ร ๐ ) ) โฉ } |
41 |
1 2 40
|
cmpt |
โข ( ๐ โ โ โฆ โฆ ( โค/nโค โ ๐ ) / ๐ง โฆ โฆ { ๐ฅ โ ( ( mulGrp โ ๐ง ) MndHom ( mulGrp โ โfld ) ) โฃ ( ( ( Base โ ๐ง ) โ ( Unit โ ๐ง ) ) ร { 0 } ) โ ๐ฅ } / ๐ โฆ { โจ ( Base โ ndx ) , ๐ โฉ , โจ ( +g โ ndx ) , ( โf ยท โพ ( ๐ ร ๐ ) ) โฉ } ) |
42 |
0 41
|
wceq |
โข DChr = ( ๐ โ โ โฆ โฆ ( โค/nโค โ ๐ ) / ๐ง โฆ โฆ { ๐ฅ โ ( ( mulGrp โ ๐ง ) MndHom ( mulGrp โ โfld ) ) โฃ ( ( ( Base โ ๐ง ) โ ( Unit โ ๐ง ) ) ร { 0 } ) โ ๐ฅ } / ๐ โฆ { โจ ( Base โ ndx ) , ๐ โฉ , โจ ( +g โ ndx ) , ( โf ยท โพ ( ๐ ร ๐ ) ) โฉ } ) |