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 = Base K
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 ⁡ X J I ⁡ Y

Proof

Step Hyp Ref Expression
1 djhlj.b ⊢ B = Base K
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 ⊢ Base DVecH ⁡ K ⁡ W = Base DVecH ⁡ K ⁡ W
10 1 3 4 8 9 dihss ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B → I ⁡ X ⊆ Base DVecH ⁡ K ⁡ W
11 7 10 syldan ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ Y ∈ B → I ⁡ X ⊆ Base DVecH ⁡ 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 ⊆ Base DVecH ⁡ K ⁡ W
14 12 13 syldan ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ Y ∈ B → I ⁡ Y ⊆ Base DVecH ⁡ K ⁡ W
15 eqid ⊢ ocH ⁡ K ⁡ W = ocH ⁡ K ⁡ W
16 3 8 9 15 5 djhval ⊢ K ∈ HL ∧ W ∈ H ∧ I ⁡ X ⊆ Base DVecH ⁡ K ⁡ W ∧ I ⁡ Y ⊆ Base DVecH ⁡ K ⁡ W → I ⁡ X J I ⁡ 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 ⁡ X J I ⁡ 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 ⁡ X meet ⁡ K oc ⁡ 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 ⁡ X meet ⁡ K oc ⁡ 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 ⁡ X meet ⁡ K oc ⁡ 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 ⁡ X meet ⁡ K oc ⁡ 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 ⁡ X meet ⁡ K oc ⁡ K ⁡ Y ∈ B
38 36 22 24 37 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ Y ∈ B → oc ⁡ K ⁡ X meet ⁡ K oc ⁡ K ⁡ Y ∈ B
39 1 20 3 4 15 dochvalr2 ⊢ K ∈ HL ∧ W ∈ H ∧ oc ⁡ K ⁡ X meet ⁡ K oc ⁡ K ⁡ Y ∈ B → ocH ⁡ K ⁡ W ⁡ I ⁡ oc ⁡ K ⁡ X meet ⁡ K oc ⁡ K ⁡ Y = I ⁡ oc ⁡ K ⁡ oc ⁡ K ⁡ X meet ⁡ K oc ⁡ K ⁡ Y
40 38 39 syldan ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ Y ∈ B → ocH ⁡ K ⁡ W ⁡ I ⁡ oc ⁡ K ⁡ X meet ⁡ K oc ⁡ K ⁡ Y = I ⁡ oc ⁡ K ⁡ oc ⁡ K ⁡ X meet ⁡ K oc ⁡ 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 ⁡ X meet ⁡ K oc ⁡ 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 ⁡ X meet ⁡ K oc ⁡ K ⁡ Y = X ∨ ˙ Y
45 43 7 12 44 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ Y ∈ B → oc ⁡ K ⁡ oc ⁡ K ⁡ X meet ⁡ K oc ⁡ K ⁡ Y = X ∨ ˙ Y
46 45 fveq2d ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ Y ∈ B → I ⁡ oc ⁡ K ⁡ oc ⁡ K ⁡ X meet ⁡ K oc ⁡ K ⁡ Y = I ⁡ X ∨ ˙ Y
47 17 41 46 3eqtrrd ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ B ∧ Y ∈ B → I ⁡ X ∨ ˙ Y = I ⁡ X J I ⁡ Y