Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
โข
((subringAlg โ๐ธ)โ(Baseโ๐พ)) = ((subringAlg โ๐ธ)โ(Baseโ๐พ)) |
2 | | eqid 2733 |
. . 3
โข
((subringAlg โ๐ธ)โ(Baseโ๐น)) = ((subringAlg โ๐ธ)โ(Baseโ๐น)) |
3 | | eqid 2733 |
. . 3
โข
((subringAlg โ(๐ธ โพs (Baseโ๐น)))โ(Baseโ๐พ)) = ((subringAlg โ(๐ธ โพs
(Baseโ๐น)))โ(Baseโ๐พ)) |
4 | | eqid 2733 |
. . 3
โข (๐ธ โพs
(Baseโ๐น)) = (๐ธ โพs
(Baseโ๐น)) |
5 | | eqid 2733 |
. . 3
โข (๐ธ โพs
(Baseโ๐พ)) = (๐ธ โพs
(Baseโ๐พ)) |
6 | | simpl 484 |
. . . . 5
โข ((๐ธ/FldExt๐น โง ๐น/FldExt๐พ) โ ๐ธ/FldExt๐น) |
7 | | fldextfld1 32395 |
. . . . 5
โข (๐ธ/FldExt๐น โ ๐ธ โ Field) |
8 | 6, 7 | syl 17 |
. . . 4
โข ((๐ธ/FldExt๐น โง ๐น/FldExt๐พ) โ ๐ธ โ Field) |
9 | | isfld 20208 |
. . . . 5
โข (๐ธ โ Field โ (๐ธ โ DivRing โง ๐ธ โ CRing)) |
10 | 9 | simplbi 499 |
. . . 4
โข (๐ธ โ Field โ ๐ธ โ
DivRing) |
11 | 8, 10 | syl 17 |
. . 3
โข ((๐ธ/FldExt๐น โง ๐น/FldExt๐พ) โ ๐ธ โ DivRing) |
12 | | fldextfld1 32395 |
. . . . . . . 8
โข (๐น/FldExt๐พ โ ๐น โ Field) |
13 | 12 | adantl 483 |
. . . . . . 7
โข ((๐ธ/FldExt๐น โง ๐น/FldExt๐พ) โ ๐น โ Field) |
14 | | brfldext 32393 |
. . . . . . 7
โข ((๐ธ โ Field โง ๐น โ Field) โ (๐ธ/FldExt๐น โ (๐น = (๐ธ โพs (Baseโ๐น)) โง (Baseโ๐น) โ (SubRingโ๐ธ)))) |
15 | 8, 13, 14 | syl2anc 585 |
. . . . . 6
โข ((๐ธ/FldExt๐น โง ๐น/FldExt๐พ) โ (๐ธ/FldExt๐น โ (๐น = (๐ธ โพs (Baseโ๐น)) โง (Baseโ๐น) โ (SubRingโ๐ธ)))) |
16 | 6, 15 | mpbid 231 |
. . . . 5
โข ((๐ธ/FldExt๐น โง ๐น/FldExt๐พ) โ (๐น = (๐ธ โพs (Baseโ๐น)) โง (Baseโ๐น) โ (SubRingโ๐ธ))) |
17 | 16 | simpld 496 |
. . . 4
โข ((๐ธ/FldExt๐น โง ๐น/FldExt๐พ) โ ๐น = (๐ธ โพs (Baseโ๐น))) |
18 | | isfld 20208 |
. . . . . 6
โข (๐น โ Field โ (๐น โ DivRing โง ๐น โ CRing)) |
19 | 18 | simplbi 499 |
. . . . 5
โข (๐น โ Field โ ๐น โ
DivRing) |
20 | 13, 19 | syl 17 |
. . . 4
โข ((๐ธ/FldExt๐น โง ๐น/FldExt๐พ) โ ๐น โ DivRing) |
21 | 17, 20 | eqeltrrd 2835 |
. . 3
โข ((๐ธ/FldExt๐น โง ๐น/FldExt๐พ) โ (๐ธ โพs (Baseโ๐น)) โ
DivRing) |
22 | | fldexttr 32404 |
. . . . . 6
โข ((๐ธ/FldExt๐น โง ๐น/FldExt๐พ) โ ๐ธ/FldExt๐พ) |
23 | | fldextfld2 32396 |
. . . . . . . 8
โข (๐น/FldExt๐พ โ ๐พ โ Field) |
24 | 23 | adantl 483 |
. . . . . . 7
โข ((๐ธ/FldExt๐น โง ๐น/FldExt๐พ) โ ๐พ โ Field) |
25 | | brfldext 32393 |
. . . . . . 7
โข ((๐ธ โ Field โง ๐พ โ Field) โ (๐ธ/FldExt๐พ โ (๐พ = (๐ธ โพs (Baseโ๐พ)) โง (Baseโ๐พ) โ (SubRingโ๐ธ)))) |
26 | 8, 24, 25 | syl2anc 585 |
. . . . . 6
โข ((๐ธ/FldExt๐น โง ๐น/FldExt๐พ) โ (๐ธ/FldExt๐พ โ (๐พ = (๐ธ โพs (Baseโ๐พ)) โง (Baseโ๐พ) โ (SubRingโ๐ธ)))) |
27 | 22, 26 | mpbid 231 |
. . . . 5
โข ((๐ธ/FldExt๐น โง ๐น/FldExt๐พ) โ (๐พ = (๐ธ โพs (Baseโ๐พ)) โง (Baseโ๐พ) โ (SubRingโ๐ธ))) |
28 | 27 | simpld 496 |
. . . 4
โข ((๐ธ/FldExt๐น โง ๐น/FldExt๐พ) โ ๐พ = (๐ธ โพs (Baseโ๐พ))) |
29 | | isfld 20208 |
. . . . . 6
โข (๐พ โ Field โ (๐พ โ DivRing โง ๐พ โ CRing)) |
30 | 29 | simplbi 499 |
. . . . 5
โข (๐พ โ Field โ ๐พ โ
DivRing) |
31 | 24, 30 | syl 17 |
. . . 4
โข ((๐ธ/FldExt๐น โง ๐น/FldExt๐พ) โ ๐พ โ DivRing) |
32 | 28, 31 | eqeltrrd 2835 |
. . 3
โข ((๐ธ/FldExt๐น โง ๐น/FldExt๐พ) โ (๐ธ โพs (Baseโ๐พ)) โ
DivRing) |
33 | 16 | simprd 497 |
. . 3
โข ((๐ธ/FldExt๐น โง ๐น/FldExt๐พ) โ (Baseโ๐น) โ (SubRingโ๐ธ)) |
34 | | eqid 2733 |
. . . . . 6
โข
(Baseโ๐พ) =
(Baseโ๐พ) |
35 | 34 | fldextsubrg 32397 |
. . . . 5
โข (๐น/FldExt๐พ โ (Baseโ๐พ) โ (SubRingโ๐น)) |
36 | 35 | adantl 483 |
. . . 4
โข ((๐ธ/FldExt๐น โง ๐น/FldExt๐พ) โ (Baseโ๐พ) โ (SubRingโ๐น)) |
37 | 17 | fveq2d 6847 |
. . . 4
โข ((๐ธ/FldExt๐น โง ๐น/FldExt๐พ) โ (SubRingโ๐น) = (SubRingโ(๐ธ โพs (Baseโ๐น)))) |
38 | 36, 37 | eleqtrd 2836 |
. . 3
โข ((๐ธ/FldExt๐น โง ๐น/FldExt๐พ) โ (Baseโ๐พ) โ (SubRingโ(๐ธ โพs (Baseโ๐น)))) |
39 | 1, 2, 3, 4, 5, 11,
21, 32, 33, 38 | fedgmul 32383 |
. 2
โข ((๐ธ/FldExt๐น โง ๐น/FldExt๐พ) โ (dimโ((subringAlg
โ๐ธ)โ(Baseโ๐พ))) = ((dimโ((subringAlg โ๐ธ)โ(Baseโ๐น))) ยทe
(dimโ((subringAlg โ(๐ธ โพs (Baseโ๐น)))โ(Baseโ๐พ))))) |
40 | | extdgval 32400 |
. . 3
โข (๐ธ/FldExt๐พ โ (๐ธ[:]๐พ) = (dimโ((subringAlg โ๐ธ)โ(Baseโ๐พ)))) |
41 | 22, 40 | syl 17 |
. 2
โข ((๐ธ/FldExt๐น โง ๐น/FldExt๐พ) โ (๐ธ[:]๐พ) = (dimโ((subringAlg โ๐ธ)โ(Baseโ๐พ)))) |
42 | | extdgval 32400 |
. . . 4
โข (๐ธ/FldExt๐น โ (๐ธ[:]๐น) = (dimโ((subringAlg โ๐ธ)โ(Baseโ๐น)))) |
43 | 6, 42 | syl 17 |
. . 3
โข ((๐ธ/FldExt๐น โง ๐น/FldExt๐พ) โ (๐ธ[:]๐น) = (dimโ((subringAlg โ๐ธ)โ(Baseโ๐น)))) |
44 | | extdgval 32400 |
. . . . 5
โข (๐น/FldExt๐พ โ (๐น[:]๐พ) = (dimโ((subringAlg โ๐น)โ(Baseโ๐พ)))) |
45 | 44 | adantl 483 |
. . . 4
โข ((๐ธ/FldExt๐น โง ๐น/FldExt๐พ) โ (๐น[:]๐พ) = (dimโ((subringAlg โ๐น)โ(Baseโ๐พ)))) |
46 | 17 | fveq2d 6847 |
. . . . . 6
โข ((๐ธ/FldExt๐น โง ๐น/FldExt๐พ) โ (subringAlg โ๐น) = (subringAlg โ(๐ธ โพs
(Baseโ๐น)))) |
47 | 46 | fveq1d 6845 |
. . . . 5
โข ((๐ธ/FldExt๐น โง ๐น/FldExt๐พ) โ ((subringAlg โ๐น)โ(Baseโ๐พ)) = ((subringAlg โ(๐ธ โพs
(Baseโ๐น)))โ(Baseโ๐พ))) |
48 | 47 | fveq2d 6847 |
. . . 4
โข ((๐ธ/FldExt๐น โง ๐น/FldExt๐พ) โ (dimโ((subringAlg
โ๐น)โ(Baseโ๐พ))) = (dimโ((subringAlg โ(๐ธ โพs
(Baseโ๐น)))โ(Baseโ๐พ)))) |
49 | 45, 48 | eqtrd 2773 |
. . 3
โข ((๐ธ/FldExt๐น โง ๐น/FldExt๐พ) โ (๐น[:]๐พ) = (dimโ((subringAlg โ(๐ธ โพs
(Baseโ๐น)))โ(Baseโ๐พ)))) |
50 | 43, 49 | oveq12d 7376 |
. 2
โข ((๐ธ/FldExt๐น โง ๐น/FldExt๐พ) โ ((๐ธ[:]๐น) ยทe (๐น[:]๐พ)) = ((dimโ((subringAlg โ๐ธ)โ(Baseโ๐น))) ยทe
(dimโ((subringAlg โ(๐ธ โพs (Baseโ๐น)))โ(Baseโ๐พ))))) |
51 | 39, 41, 50 | 3eqtr4d 2783 |
1
โข ((๐ธ/FldExt๐น โง ๐น/FldExt๐พ) โ (๐ธ[:]๐พ) = ((๐ธ[:]๐น) ยทe (๐น[:]๐พ))) |