Metamath Proof Explorer


Theorem dihmeet2

Description: Reverse isomorphism H of a closed subspace intersection. (Contributed by NM, 15-Jan-2015)

Ref Expression
Hypotheses dihmeet2.m ˙=meetK
dihmeet2.h H=LHypK
dihmeet2.i I=DIsoHKW
dihmeet2.k φKHLWH
dihmeet2.x φXranI
dihmeet2.y φYranI
Assertion dihmeet2 φI-1XY=I-1X˙I-1Y

Proof

Step Hyp Ref Expression
1 dihmeet2.m ˙=meetK
2 dihmeet2.h H=LHypK
3 dihmeet2.i I=DIsoHKW
4 dihmeet2.k φKHLWH
5 dihmeet2.x φXranI
6 dihmeet2.y φYranI
7 2 3 dihcnvid2 KHLWHXranIII-1X=X
8 4 5 7 syl2anc φII-1X=X
9 2 3 dihcnvid2 KHLWHYranIII-1Y=Y
10 4 6 9 syl2anc φII-1Y=Y
11 8 10 ineq12d φII-1XII-1Y=XY
12 eqid BaseK=BaseK
13 12 2 3 dihcnvcl KHLWHXranII-1XBaseK
14 4 5 13 syl2anc φI-1XBaseK
15 12 2 3 dihcnvcl KHLWHYranII-1YBaseK
16 4 6 15 syl2anc φI-1YBaseK
17 12 1 2 3 dihmeet KHLWHI-1XBaseKI-1YBaseKII-1X˙I-1Y=II-1XII-1Y
18 4 14 16 17 syl3anc φII-1X˙I-1Y=II-1XII-1Y
19 2 3 dihmeetcl KHLWHXranIYranIXYranI
20 4 5 6 19 syl12anc φXYranI
21 2 3 dihcnvid2 KHLWHXYranIII-1XY=XY
22 4 20 21 syl2anc φII-1XY=XY
23 11 18 22 3eqtr4rd φII-1XY=II-1X˙I-1Y
24 12 2 3 dihcnvcl KHLWHXYranII-1XYBaseK
25 4 20 24 syl2anc φI-1XYBaseK
26 4 simpld φKHL
27 26 hllatd φKLat
28 12 1 latmcl KLatI-1XBaseKI-1YBaseKI-1X˙I-1YBaseK
29 27 14 16 28 syl3anc φI-1X˙I-1YBaseK
30 12 2 3 dih11 KHLWHI-1XYBaseKI-1X˙I-1YBaseKII-1XY=II-1X˙I-1YI-1XY=I-1X˙I-1Y
31 4 25 29 30 syl3anc φII-1XY=II-1X˙I-1YI-1XY=I-1X˙I-1Y
32 23 31 mpbid φI-1XY=I-1X˙I-1Y