Metamath Proof Explorer

Theorem dihmeetcl

Description: Closure of closed subspace meet for DVecH vector space. (Contributed by NM, 5-Aug-2014)

Ref Expression
Hypotheses dihmeetcl.h ⊢ H = LHyp ⁡ K
dihmeetcl.i ⊢ I = DIsoH ⁡ K ⁡ W
Assertion dihmeetcl ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I ∧ Y ∈ ran ⁡ I → X ∩ Y ∈ ran ⁡ I

Proof

Step Hyp Ref Expression
1 dihmeetcl.h ⊢ H = LHyp ⁡ K
2 dihmeetcl.i ⊢ I = DIsoH ⁡ K ⁡ W
3 1 2 dihcnvid2 ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → I ⁡ I -1 ⁡ X = X
4 3 adantrr ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I ∧ Y ∈ ran ⁡ I → I ⁡ I -1 ⁡ X = X
5 1 2 dihcnvid2 ⊢ K ∈ HL ∧ W ∈ H ∧ Y ∈ ran ⁡ I → I ⁡ I -1 ⁡ Y = Y
6 5 adantrl ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I ∧ Y ∈ ran ⁡ I → I ⁡ I -1 ⁡ Y = Y
7 4 6 ineq12d ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I ∧ Y ∈ ran ⁡ I → I ⁡ I -1 ⁡ X ∩ I ⁡ I -1 ⁡ Y = X ∩ Y
8 simpl ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I ∧ Y ∈ ran ⁡ I → K ∈ HL ∧ W ∈ H
9 eqid ⊢ Base K = Base K
10 9 1 2 dihcnvcl ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → I -1 ⁡ X ∈ Base K
11 10 adantrr ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I ∧ Y ∈ ran ⁡ I → I -1 ⁡ X ∈ Base K
12 9 1 2 dihcnvcl ⊢ K ∈ HL ∧ W ∈ H ∧ Y ∈ ran ⁡ I → I -1 ⁡ Y ∈ Base K
13 12 adantrl ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I ∧ Y ∈ ran ⁡ I → I -1 ⁡ Y ∈ Base K
14 eqid ⊢ meet ⁡ K = meet ⁡ K
15 9 14 1 2 dihmeet ⊢ K ∈ HL ∧ W ∈ H ∧ I -1 ⁡ X ∈ Base K ∧ I -1 ⁡ Y ∈ Base K → I ⁡ I -1 ⁡ X meet ⁡ K I -1 ⁡ Y = I ⁡ I -1 ⁡ X ∩ I ⁡ I -1 ⁡ Y
16 8 11 13 15 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I ∧ Y ∈ ran ⁡ I → I ⁡ I -1 ⁡ X meet ⁡ K I -1 ⁡ Y = I ⁡ I -1 ⁡ X ∩ I ⁡ I -1 ⁡ Y
17 hllat ⊢ K ∈ HL → K ∈ Lat
18 17 ad2antrr ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I ∧ Y ∈ ran ⁡ I → K ∈ Lat
19 9 14 latmcl ⊢ K ∈ Lat ∧ I -1 ⁡ X ∈ Base K ∧ I -1 ⁡ Y ∈ Base K → I -1 ⁡ X meet ⁡ K I -1 ⁡ Y ∈ Base K
20 18 11 13 19 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I ∧ Y ∈ ran ⁡ I → I -1 ⁡ X meet ⁡ K I -1 ⁡ Y ∈ Base K
21 9 1 2 dihcl ⊢ K ∈ HL ∧ W ∈ H ∧ I -1 ⁡ X meet ⁡ K I -1 ⁡ Y ∈ Base K → I ⁡ I -1 ⁡ X meet ⁡ K I -1 ⁡ Y ∈ ran ⁡ I
22 20 21 syldan ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I ∧ Y ∈ ran ⁡ I → I ⁡ I -1 ⁡ X meet ⁡ K I -1 ⁡ Y ∈ ran ⁡ I
23 16 22 eqeltrrd ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I ∧ Y ∈ ran ⁡ I → I ⁡ I -1 ⁡ X ∩ I ⁡ I -1 ⁡ Y ∈ ran ⁡ I
24 7 23 eqeltrrd ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I ∧ Y ∈ ran ⁡ I → X ∩ Y ∈ ran ⁡ I