Description: Reverse isomorphism H of a closed subspace intersection. (Contributed by NM, 15-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dihmeet2.m | |
|
dihmeet2.h | |
||
dihmeet2.i | |
||
dihmeet2.k | |
||
dihmeet2.x | |
||
dihmeet2.y | |
||
Assertion | dihmeet2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dihmeet2.m | |
|
2 | dihmeet2.h | |
|
3 | dihmeet2.i | |
|
4 | dihmeet2.k | |
|
5 | dihmeet2.x | |
|
6 | dihmeet2.y | |
|
7 | 2 3 | dihcnvid2 | |
8 | 4 5 7 | syl2anc | |
9 | 2 3 | dihcnvid2 | |
10 | 4 6 9 | syl2anc | |
11 | 8 10 | ineq12d | |
12 | eqid | |
|
13 | 12 2 3 | dihcnvcl | |
14 | 4 5 13 | syl2anc | |
15 | 12 2 3 | dihcnvcl | |
16 | 4 6 15 | syl2anc | |
17 | 12 1 2 3 | dihmeet | |
18 | 4 14 16 17 | syl3anc | |
19 | 2 3 | dihmeetcl | |
20 | 4 5 6 19 | syl12anc | |
21 | 2 3 | dihcnvid2 | |
22 | 4 20 21 | syl2anc | |
23 | 11 18 22 | 3eqtr4rd | |
24 | 12 2 3 | dihcnvcl | |
25 | 4 20 24 | syl2anc | |
26 | 4 | simpld | |
27 | 26 | hllatd | |
28 | 12 1 | latmcl | |
29 | 27 14 16 28 | syl3anc | |
30 | 12 2 3 | dih11 | |
31 | 4 25 29 30 | syl3anc | |
32 | 23 31 | mpbid | |