Description: Obsolete version of tdeglem1 as of 7-Aug-2024. (Contributed by Stefan O'Rear, 19-Mar-2015) (Proof shortened by AV, 27-Jul-2019) (New usage is discouraged.) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | tdeglem.a | |
|
tdeglem.h | |
||
Assertion | tdeglem1OLD | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tdeglem.a | |
|
2 | tdeglem.h | |
|
3 | cnfld0 | |
|
4 | cnring | |
|
5 | ringcmn | |
|
6 | 4 5 | mp1i | |
7 | simpl | |
|
8 | nn0subm | |
|
9 | 8 | a1i | |
10 | 1 | psrbagfOLD | |
11 | 1 | psrbagfsuppOLD | |
12 | 11 | ancoms | |
13 | 3 6 7 9 10 12 | gsumsubmcl | |
14 | 13 2 | fmptd | |