Description: Lemma for cphreccl . (Contributed by Mario Carneiro, 8-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cphsubrglem.k | |
|
cphsubrglem.1 | |
||
cphsubrglem.2 | |
||
Assertion | cphreccllem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cphsubrglem.k | |
|
2 | cphsubrglem.1 | |
|
3 | cphsubrglem.2 | |
|
4 | 1 2 3 | cphsubrglem | |
5 | 4 | simp3d | |
6 | 5 | 3ad2ant1 | |
7 | cnfldbas | |
|
8 | 7 | subrgss | |
9 | 6 8 | syl | |
10 | simp2 | |
|
11 | 9 10 | sseldd | |
12 | simp3 | |
|
13 | cnfldinv | |
|
14 | 11 12 13 | syl2anc | |
15 | eqid | |
|
16 | cnfld0 | |
|
17 | 15 16 | subrg0 | |
18 | 6 17 | syl | |
19 | 4 | simp1d | |
20 | 19 | 3ad2ant1 | |
21 | 20 | fveq2d | |
22 | 18 21 | eqtr4d | |
23 | 12 22 | neeqtrd | |
24 | eldifsn | |
|
25 | 10 23 24 | sylanbrc | |
26 | 3 | 3ad2ant1 | |
27 | eqid | |
|
28 | eqid | |
|
29 | 1 27 28 | isdrng | |
30 | 29 | simprbi | |
31 | 26 30 | syl | |
32 | 20 | fveq2d | |
33 | 31 32 | eqtr3d | |
34 | 25 33 | eleqtrd | |
35 | eqid | |
|
36 | eqid | |
|
37 | eqid | |
|
38 | 15 35 36 37 | subrgunit | |
39 | 6 38 | syl | |
40 | 34 39 | mpbid | |
41 | 40 | simp3d | |
42 | 14 41 | eqeltrrd | |