# 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}={\mathrm{Base}}_{{K}}$
djhlj.k
djhlj.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
djhlj.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
djhlj.j ${⊢}{J}=\mathrm{joinH}\left({K}\right)\left({W}\right)$
Assertion djhlj

### Proof

Step Hyp Ref Expression
1 djhlj.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 djhlj.k
3 djhlj.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
4 djhlj.i ${⊢}{I}=\mathrm{DIsoH}\left({K}\right)\left({W}\right)$
5 djhlj.j ${⊢}{J}=\mathrm{joinH}\left({K}\right)\left({W}\right)$
6 simpl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
7 simprl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {X}\in {B}$
8 eqid ${⊢}\mathrm{DVecH}\left({K}\right)\left({W}\right)=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
9 eqid ${⊢}{\mathrm{Base}}_{\mathrm{DVecH}\left({K}\right)\left({W}\right)}={\mathrm{Base}}_{\mathrm{DVecH}\left({K}\right)\left({W}\right)}$
10 1 3 4 8 9 dihss ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {B}\right)\to {I}\left({X}\right)\subseteq {\mathrm{Base}}_{\mathrm{DVecH}\left({K}\right)\left({W}\right)}$
11 7 10 syldan ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {I}\left({X}\right)\subseteq {\mathrm{Base}}_{\mathrm{DVecH}\left({K}\right)\left({W}\right)}$
12 simprr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {Y}\in {B}$
13 1 3 4 8 9 dihss ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {Y}\in {B}\right)\to {I}\left({Y}\right)\subseteq {\mathrm{Base}}_{\mathrm{DVecH}\left({K}\right)\left({W}\right)}$
14 12 13 syldan ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {I}\left({Y}\right)\subseteq {\mathrm{Base}}_{\mathrm{DVecH}\left({K}\right)\left({W}\right)}$
15 eqid ${⊢}\mathrm{ocH}\left({K}\right)\left({W}\right)=\mathrm{ocH}\left({K}\right)\left({W}\right)$
16 3 8 9 15 5 djhval ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({I}\left({X}\right)\subseteq {\mathrm{Base}}_{\mathrm{DVecH}\left({K}\right)\left({W}\right)}\wedge {I}\left({Y}\right)\subseteq {\mathrm{Base}}_{\mathrm{DVecH}\left({K}\right)\left({W}\right)}\right)\right)\to {I}\left({X}\right){J}{I}\left({Y}\right)=\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left({I}\left({X}\right)\right)\cap \mathrm{ocH}\left({K}\right)\left({W}\right)\left({I}\left({Y}\right)\right)\right)$
17 6 11 14 16 syl12anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {I}\left({X}\right){J}{I}\left({Y}\right)=\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left({I}\left({X}\right)\right)\cap \mathrm{ocH}\left({K}\right)\left({W}\right)\left({I}\left({Y}\right)\right)\right)$
18 hlop ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OP}$
19 18 ad2antrr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {K}\in \mathrm{OP}$
20 eqid ${⊢}\mathrm{oc}\left({K}\right)=\mathrm{oc}\left({K}\right)$
21 1 20 opoccl ${⊢}\left({K}\in \mathrm{OP}\wedge {X}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({X}\right)\in {B}$
22 19 7 21 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \mathrm{oc}\left({K}\right)\left({X}\right)\in {B}$
23 1 20 opoccl ${⊢}\left({K}\in \mathrm{OP}\wedge {Y}\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({Y}\right)\in {B}$
24 19 12 23 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \mathrm{oc}\left({K}\right)\left({Y}\right)\in {B}$
25 eqid ${⊢}\mathrm{meet}\left({K}\right)=\mathrm{meet}\left({K}\right)$
26 1 25 3 4 dihmeet ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \mathrm{oc}\left({K}\right)\left({X}\right)\in {B}\wedge \mathrm{oc}\left({K}\right)\left({Y}\right)\in {B}\right)\to {I}\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)={I}\left(\mathrm{oc}\left({K}\right)\left({X}\right)\right)\cap {I}\left(\mathrm{oc}\left({K}\right)\left({Y}\right)\right)$
27 6 22 24 26 syl3anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {I}\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)={I}\left(\mathrm{oc}\left({K}\right)\left({X}\right)\right)\cap {I}\left(\mathrm{oc}\left({K}\right)\left({Y}\right)\right)$
28 1 20 3 4 15 dochvalr2 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {X}\in {B}\right)\to \mathrm{ocH}\left({K}\right)\left({W}\right)\left({I}\left({X}\right)\right)={I}\left(\mathrm{oc}\left({K}\right)\left({X}\right)\right)$
29 7 28 syldan ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \mathrm{ocH}\left({K}\right)\left({W}\right)\left({I}\left({X}\right)\right)={I}\left(\mathrm{oc}\left({K}\right)\left({X}\right)\right)$
30 1 20 3 4 15 dochvalr2 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {Y}\in {B}\right)\to \mathrm{ocH}\left({K}\right)\left({W}\right)\left({I}\left({Y}\right)\right)={I}\left(\mathrm{oc}\left({K}\right)\left({Y}\right)\right)$
31 12 30 syldan ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \mathrm{ocH}\left({K}\right)\left({W}\right)\left({I}\left({Y}\right)\right)={I}\left(\mathrm{oc}\left({K}\right)\left({Y}\right)\right)$
32 29 31 ineq12d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \mathrm{ocH}\left({K}\right)\left({W}\right)\left({I}\left({X}\right)\right)\cap \mathrm{ocH}\left({K}\right)\left({W}\right)\left({I}\left({Y}\right)\right)={I}\left(\mathrm{oc}\left({K}\right)\left({X}\right)\right)\cap {I}\left(\mathrm{oc}\left({K}\right)\left({Y}\right)\right)$
33 27 32 eqtr4d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {I}\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)=\mathrm{ocH}\left({K}\right)\left({W}\right)\left({I}\left({X}\right)\right)\cap \mathrm{ocH}\left({K}\right)\left({W}\right)\left({I}\left({Y}\right)\right)$
34 33 fveq2d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \mathrm{ocH}\left({K}\right)\left({W}\right)\left({I}\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\right)=\mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left({I}\left({X}\right)\right)\cap \mathrm{ocH}\left({K}\right)\left({W}\right)\left({I}\left({Y}\right)\right)\right)$
35 hllat ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{Lat}$
36 35 ad2antrr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {K}\in \mathrm{Lat}$
37 1 25 latmcl ${⊢}\left({K}\in \mathrm{Lat}\wedge \mathrm{oc}\left({K}\right)\left({X}\right)\in {B}\wedge \mathrm{oc}\left({K}\right)\left({Y}\right)\in {B}\right)\to \mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\in {B}$
38 36 22 24 37 syl3anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\in {B}$
39 1 20 3 4 15 dochvalr2 ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\in {B}\right)\to \mathrm{ocH}\left({K}\right)\left({W}\right)\left({I}\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\right)={I}\left(\mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\right)$
40 38 39 syldan ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \mathrm{ocH}\left({K}\right)\left({W}\right)\left({I}\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\right)={I}\left(\mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\right)$
41 34 40 eqtr3d ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \mathrm{ocH}\left({K}\right)\left({W}\right)\left(\mathrm{ocH}\left({K}\right)\left({W}\right)\left({I}\left({X}\right)\right)\cap \mathrm{ocH}\left({K}\right)\left({W}\right)\left({I}\left({Y}\right)\right)\right)={I}\left(\mathrm{oc}\left({K}\right)\left(\mathrm{oc}\left({K}\right)\left({X}\right)\mathrm{meet}\left({K}\right)\mathrm{oc}\left({K}\right)\left({Y}\right)\right)\right)$
42 hlol ${⊢}{K}\in \mathrm{HL}\to {K}\in \mathrm{OL}$
43 42 ad2antrr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {K}\in \mathrm{OL}$
44 1 2 25 20 oldmm4
45 43 7 12 44 syl3anc
46 45 fveq2d
47 17 41 46 3eqtrrd