Metamath Proof Explorer

Theorem djhlj

Description: Transfer lattice join to DVecH vector space closed subspace join. (Contributed by NM, 19-Jul-2014)

Ref Expression
Hypotheses djhlj.b ⊢B=BaseK
djhlj.k ⊢∨˙=join⁡K
djhlj.h ⊢H=LHyp⁡K
djhlj.i ⊢I=DIsoH⁡K⁡W
djhlj.j ⊢J=joinH⁡K⁡W
Assertion djhlj ⊢K∈HL∧W∈H∧X∈B∧Y∈B→I⁡X∨˙Y=I⁡XJI⁡Y

Proof

Step Hyp Ref Expression
1 djhlj.b ⊢B=BaseK
2 djhlj.k ⊢∨˙=join⁡K
3 djhlj.h ⊢H=LHyp⁡K
4 djhlj.i ⊢I=DIsoH⁡K⁡W
5 djhlj.j ⊢J=joinH⁡K⁡W
6 simpl ⊢K∈HL∧W∈H∧X∈B∧Y∈B→K∈HL∧W∈H
7 simprl ⊢K∈HL∧W∈H∧X∈B∧Y∈B→X∈B
8 eqid ⊢DVecH⁡K⁡W=DVecH⁡K⁡W
9 eqid ⊢BaseDVecH⁡K⁡W=BaseDVecH⁡K⁡W
10 1 3 4 8 9 dihss ⊢K∈HL∧W∈H∧X∈B→I⁡X⊆BaseDVecH⁡K⁡W
11 7 10 syldan ⊢K∈HL∧W∈H∧X∈B∧Y∈B→I⁡X⊆BaseDVecH⁡K⁡W
12 simprr ⊢K∈HL∧W∈H∧X∈B∧Y∈B→Y∈B
13 1 3 4 8 9 dihss ⊢K∈HL∧W∈H∧Y∈B→I⁡Y⊆BaseDVecH⁡K⁡W
14 12 13 syldan ⊢K∈HL∧W∈H∧X∈B∧Y∈B→I⁡Y⊆BaseDVecH⁡K⁡W
15 eqid ⊢ocH⁡K⁡W=ocH⁡K⁡W
16 3 8 9 15 5 djhval ⊢K∈HL∧W∈H∧I⁡X⊆BaseDVecH⁡K⁡W∧I⁡Y⊆BaseDVecH⁡K⁡W→I⁡XJI⁡Y=ocH⁡K⁡W⁡ocH⁡K⁡W⁡I⁡X∩ocH⁡K⁡W⁡I⁡Y
17 6 11 14 16 syl12anc ⊢K∈HL∧W∈H∧X∈B∧Y∈B→I⁡XJI⁡Y=ocH⁡K⁡W⁡ocH⁡K⁡W⁡I⁡X∩ocH⁡K⁡W⁡I⁡Y
18 hlop ⊢K∈HL→K∈OP
19 18 ad2antrr ⊢K∈HL∧W∈H∧X∈B∧Y∈B→K∈OP
20 eqid ⊢oc⁡K=oc⁡K
21 1 20 opoccl ⊢K∈OP∧X∈B→oc⁡K⁡X∈B
22 19 7 21 syl2anc ⊢K∈HL∧W∈H∧X∈B∧Y∈B→oc⁡K⁡X∈B
23 1 20 opoccl ⊢K∈OP∧Y∈B→oc⁡K⁡Y∈B
24 19 12 23 syl2anc ⊢K∈HL∧W∈H∧X∈B∧Y∈B→oc⁡K⁡Y∈B
25 eqid ⊢meet⁡K=meet⁡K
26 1 25 3 4 dihmeet ⊢K∈HL∧W∈H∧oc⁡K⁡X∈B∧oc⁡K⁡Y∈B→I⁡oc⁡K⁡Xmeet⁡Koc⁡K⁡Y=I⁡oc⁡K⁡X∩I⁡oc⁡K⁡Y
27 6 22 24 26 syl3anc ⊢K∈HL∧W∈H∧X∈B∧Y∈B→I⁡oc⁡K⁡Xmeet⁡Koc⁡K⁡Y=I⁡oc⁡K⁡X∩I⁡oc⁡K⁡Y
28 1 20 3 4 15 dochvalr2 ⊢K∈HL∧W∈H∧X∈B→ocH⁡K⁡W⁡I⁡X=I⁡oc⁡K⁡X
29 7 28 syldan ⊢K∈HL∧W∈H∧X∈B∧Y∈B→ocH⁡K⁡W⁡I⁡X=I⁡oc⁡K⁡X
30 1 20 3 4 15 dochvalr2 ⊢K∈HL∧W∈H∧Y∈B→ocH⁡K⁡W⁡I⁡Y=I⁡oc⁡K⁡Y
31 12 30 syldan ⊢K∈HL∧W∈H∧X∈B∧Y∈B→ocH⁡K⁡W⁡I⁡Y=I⁡oc⁡K⁡Y
32 29 31 ineq12d ⊢K∈HL∧W∈H∧X∈B∧Y∈B→ocH⁡K⁡W⁡I⁡X∩ocH⁡K⁡W⁡I⁡Y=I⁡oc⁡K⁡X∩I⁡oc⁡K⁡Y
33 27 32 eqtr4d ⊢K∈HL∧W∈H∧X∈B∧Y∈B→I⁡oc⁡K⁡Xmeet⁡Koc⁡K⁡Y=ocH⁡K⁡W⁡I⁡X∩ocH⁡K⁡W⁡I⁡Y
34 33 fveq2d ⊢K∈HL∧W∈H∧X∈B∧Y∈B→ocH⁡K⁡W⁡I⁡oc⁡K⁡Xmeet⁡Koc⁡K⁡Y=ocH⁡K⁡W⁡ocH⁡K⁡W⁡I⁡X∩ocH⁡K⁡W⁡I⁡Y
35 hllat ⊢K∈HL→K∈Lat
36 35 ad2antrr ⊢K∈HL∧W∈H∧X∈B∧Y∈B→K∈Lat
37 1 25 latmcl ⊢K∈Lat∧oc⁡K⁡X∈B∧oc⁡K⁡Y∈B→oc⁡K⁡Xmeet⁡Koc⁡K⁡Y∈B
38 36 22 24 37 syl3anc ⊢K∈HL∧W∈H∧X∈B∧Y∈B→oc⁡K⁡Xmeet⁡Koc⁡K⁡Y∈B
39 1 20 3 4 15 dochvalr2 ⊢K∈HL∧W∈H∧oc⁡K⁡Xmeet⁡Koc⁡K⁡Y∈B→ocH⁡K⁡W⁡I⁡oc⁡K⁡Xmeet⁡Koc⁡K⁡Y=I⁡oc⁡K⁡oc⁡K⁡Xmeet⁡Koc⁡K⁡Y
40 38 39 syldan ⊢K∈HL∧W∈H∧X∈B∧Y∈B→ocH⁡K⁡W⁡I⁡oc⁡K⁡Xmeet⁡Koc⁡K⁡Y=I⁡oc⁡K⁡oc⁡K⁡Xmeet⁡Koc⁡K⁡Y
41 34 40 eqtr3d ⊢K∈HL∧W∈H∧X∈B∧Y∈B→ocH⁡K⁡W⁡ocH⁡K⁡W⁡I⁡X∩ocH⁡K⁡W⁡I⁡Y=I⁡oc⁡K⁡oc⁡K⁡Xmeet⁡Koc⁡K⁡Y
42 hlol ⊢K∈HL→K∈OL
43 42 ad2antrr ⊢K∈HL∧W∈H∧X∈B∧Y∈B→K∈OL
44 1 2 25 20 oldmm4 ⊢K∈OL∧X∈B∧Y∈B→oc⁡K⁡oc⁡K⁡Xmeet⁡Koc⁡K⁡Y=X∨˙Y
45 43 7 12 44 syl3anc ⊢K∈HL∧W∈H∧X∈B∧Y∈B→oc⁡K⁡oc⁡K⁡Xmeet⁡Koc⁡K⁡Y=X∨˙Y
46 45 fveq2d ⊢K∈HL∧W∈H∧X∈B∧Y∈B→I⁡oc⁡K⁡oc⁡K⁡Xmeet⁡Koc⁡K⁡Y=I⁡X∨˙Y
47 17 41 46 3eqtrrd ⊢K∈HL∧W∈H∧X∈B∧Y∈B→I⁡X∨˙Y=I⁡XJI⁡Y