Description: This theorem proves Lemma 2 in BrosowskiDeutsh p. 92 when A is empty, the trivial case. Here D is used to denote the set A of Lemma 2, because the variable A is used for the subalgebra. (Contributed by Glauco Siliprandi, 20-Apr-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | stoweidlem18.1 | |
|
stoweidlem18.2 | |
||
stoweidlem18.3 | |
||
stoweidlem18.4 | |
||
stoweidlem18.5 | |
||
stoweidlem18.6 | |
||
stoweidlem18.7 | |
||
stoweidlem18.8 | |
||
Assertion | stoweidlem18 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | stoweidlem18.1 | |
|
2 | stoweidlem18.2 | |
|
3 | stoweidlem18.3 | |
|
4 | stoweidlem18.4 | |
|
5 | stoweidlem18.5 | |
|
6 | stoweidlem18.6 | |
|
7 | stoweidlem18.7 | |
|
8 | stoweidlem18.8 | |
|
9 | 1re | |
|
10 | 5 | stoweidlem4 | |
11 | 9 10 | mpan2 | |
12 | 3 11 | eqeltrid | |
13 | 0le1 | |
|
14 | simpr | |
|
15 | 3 | fvmpt2 | |
16 | 14 9 15 | sylancl | |
17 | 13 16 | breqtrrid | |
18 | 1le1 | |
|
19 | 16 18 | eqbrtrdi | |
20 | 17 19 | jca | |
21 | 20 | ex | |
22 | 2 21 | ralrimi | |
23 | nfcv | |
|
24 | 1 23 | nfeq | |
25 | 24 | rzalf | |
26 | 8 25 | syl | |
27 | 1red | |
|
28 | 27 7 | ltsubrpd | |
29 | 28 | adantr | |
30 | 4 | cldss | |
31 | 6 30 | syl | |
32 | 31 | sselda | |
33 | 32 9 15 | sylancl | |
34 | 29 33 | breqtrrd | |
35 | 34 | ex | |
36 | 2 35 | ralrimi | |
37 | nfcv | |
|
38 | nfmpt1 | |
|
39 | 3 38 | nfcxfr | |
40 | 37 39 | nfeq | |
41 | fveq1 | |
|
42 | 41 | breq2d | |
43 | 41 | breq1d | |
44 | 42 43 | anbi12d | |
45 | 40 44 | ralbid | |
46 | 41 | breq1d | |
47 | 40 46 | ralbid | |
48 | 41 | breq2d | |
49 | 40 48 | ralbid | |
50 | 45 47 49 | 3anbi123d | |
51 | 50 | rspcev | |
52 | 12 22 26 36 51 | syl13anc | |