Step |
Hyp |
Ref |
Expression |
0 |
|
cfldext |
|- /FldExt |
1 |
|
ve |
|- e |
2 |
|
vf |
|- f |
3 |
1
|
cv |
|- e |
4 |
|
cfield |
|- Field |
5 |
3 4
|
wcel |
|- e e. Field |
6 |
2
|
cv |
|- f |
7 |
6 4
|
wcel |
|- f e. Field |
8 |
5 7
|
wa |
|- ( e e. Field /\ f e. Field ) |
9 |
|
cress |
|- |`s |
10 |
|
cbs |
|- Base |
11 |
6 10
|
cfv |
|- ( Base ` f ) |
12 |
3 11 9
|
co |
|- ( e |`s ( Base ` f ) ) |
13 |
6 12
|
wceq |
|- f = ( e |`s ( Base ` f ) ) |
14 |
|
csubrg |
|- SubRing |
15 |
3 14
|
cfv |
|- ( SubRing ` e ) |
16 |
11 15
|
wcel |
|- ( Base ` f ) e. ( SubRing ` e ) |
17 |
13 16
|
wa |
|- ( f = ( e |`s ( Base ` f ) ) /\ ( Base ` f ) e. ( SubRing ` e ) ) |
18 |
8 17
|
wa |
|- ( ( e e. Field /\ f e. Field ) /\ ( f = ( e |`s ( Base ` f ) ) /\ ( Base ` f ) e. ( SubRing ` e ) ) ) |
19 |
18 1 2
|
copab |
|- { <. e , f >. | ( ( e e. Field /\ f e. Field ) /\ ( f = ( e |`s ( Base ` f ) ) /\ ( Base ` f ) e. ( SubRing ` e ) ) ) } |
20 |
0 19
|
wceq |
|- /FldExt = { <. e , f >. | ( ( e e. Field /\ f e. Field ) /\ ( f = ( e |`s ( Base ` f ) ) /\ ( Base ` f ) e. ( SubRing ` e ) ) ) } |