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 ˙ = meet K
dihmeet2.h H = LHyp K
dihmeet2.i I = DIsoH K W
dihmeet2.k φ K HL W H
dihmeet2.x φ X ran I
dihmeet2.y φ Y ran I
Assertion dihmeet2 φ I -1 X Y = I -1 X ˙ I -1 Y

Proof

Step Hyp Ref Expression
1 dihmeet2.m ˙ = meet K
2 dihmeet2.h H = LHyp K
3 dihmeet2.i I = DIsoH K W
4 dihmeet2.k φ K HL W H
5 dihmeet2.x φ X ran I
6 dihmeet2.y φ Y ran I
7 2 3 dihcnvid2 K HL W H X ran I I I -1 X = X
8 4 5 7 syl2anc φ I I -1 X = X
9 2 3 dihcnvid2 K HL W H Y ran I I I -1 Y = Y
10 4 6 9 syl2anc φ I I -1 Y = Y
11 8 10 ineq12d φ I I -1 X I I -1 Y = X Y
12 eqid Base K = Base K
13 12 2 3 dihcnvcl K HL W H X ran I I -1 X Base K
14 4 5 13 syl2anc φ I -1 X Base K
15 12 2 3 dihcnvcl K HL W H Y ran I I -1 Y Base K
16 4 6 15 syl2anc φ I -1 Y Base K
17 12 1 2 3 dihmeet K HL W H I -1 X Base K I -1 Y Base K I I -1 X ˙ I -1 Y = I I -1 X I I -1 Y
18 4 14 16 17 syl3anc φ I I -1 X ˙ I -1 Y = I I -1 X I I -1 Y
19 2 3 dihmeetcl K HL W H X ran I Y ran I X Y ran I
20 4 5 6 19 syl12anc φ X Y ran I
21 2 3 dihcnvid2 K HL W H X Y ran I I I -1 X Y = X Y
22 4 20 21 syl2anc φ I I -1 X Y = X Y
23 11 18 22 3eqtr4rd φ I I -1 X Y = I I -1 X ˙ I -1 Y
24 12 2 3 dihcnvcl K HL W H X Y ran I I -1 X Y Base K
25 4 20 24 syl2anc φ I -1 X Y Base K
26 4 simpld φ K HL
27 26 hllatd φ K Lat
28 12 1 latmcl K Lat I -1 X Base K I -1 Y Base K I -1 X ˙ I -1 Y Base K
29 27 14 16 28 syl3anc φ I -1 X ˙ I -1 Y Base K
30 12 2 3 dih11 K HL W H I -1 X Y Base K I -1 X ˙ I -1 Y Base K I I -1 X Y = I I -1 X ˙ I -1 Y I -1 X Y = I -1 X ˙ I -1 Y
31 4 25 29 30 syl3anc φ I I -1 X Y = I I -1 X ˙ I -1 Y I -1 X Y = I -1 X ˙ I -1 Y
32 23 31 mpbid φ I -1 X Y = I -1 X ˙ I -1 Y