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 ⊢BaseK=BaseK
10 9 1 2 dihcnvcl ⊢K∈HL∧W∈H∧X∈ran⁡I→I-1⁡X∈BaseK
11 10 adantrr ⊢K∈HL∧W∈H∧X∈ran⁡I∧Y∈ran⁡I→I-1⁡X∈BaseK
12 9 1 2 dihcnvcl ⊢K∈HL∧W∈H∧Y∈ran⁡I→I-1⁡Y∈BaseK
13 12 adantrl ⊢K∈HL∧W∈H∧X∈ran⁡I∧Y∈ran⁡I→I-1⁡Y∈BaseK
14 eqid ⊢meet⁡K=meet⁡K
15 9 14 1 2 dihmeet ⊢K∈HL∧W∈H∧I-1⁡X∈BaseK∧I-1⁡Y∈BaseK→I⁡I-1⁡Xmeet⁡KI-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⁡Xmeet⁡KI-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∈BaseK∧I-1⁡Y∈BaseK→I-1⁡Xmeet⁡KI-1⁡Y∈BaseK
20 18 11 13 19 syl3anc ⊢K∈HL∧W∈H∧X∈ran⁡I∧Y∈ran⁡I→I-1⁡Xmeet⁡KI-1⁡Y∈BaseK
21 9 1 2 dihcl ⊢K∈HL∧W∈H∧I-1⁡Xmeet⁡KI-1⁡Y∈BaseK→I⁡I-1⁡Xmeet⁡KI-1⁡Y∈ran⁡I
22 20 21 syldan ⊢K∈HL∧W∈H∧X∈ran⁡I∧Y∈ran⁡I→I⁡I-1⁡Xmeet⁡KI-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