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