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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
djhlj.k ⊢ ∨ = ( join ‘ 𝐾 )
djhlj.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
djhlj.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
djhlj.j ⊢ 𝐽 = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
Assertion djhlj ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐼 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐼 ‘ 𝑋 ) 𝐽 ( 𝐼 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 djhlj.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 djhlj.k ⊢ ∨ = ( join ‘ 𝐾 )
3 djhlj.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 djhlj.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
5 djhlj.j ⊢ 𝐽 = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
6 simpl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7 simprl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
8 eqid ⊢ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
9 eqid ⊢ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
10 1 3 4 8 9 dihss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑋 ) ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
11 7 10 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐼 ‘ 𝑋 ) ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
12 simprr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
13 1 3 4 8 9 dihss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑌 ) ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
14 12 13 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐼 ‘ 𝑌 ) ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
15 eqid ⊢ ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
16 3 8 9 15 5 djhval ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝐼 ‘ 𝑋 ) ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ ( 𝐼 ‘ 𝑌 ) ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) → ( ( 𝐼 ‘ 𝑋 ) 𝐽 ( 𝐼 ‘ 𝑌 ) ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝐼 ‘ 𝑋 ) ) ∩ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝐼 ‘ 𝑌 ) ) ) ) )
17 6 11 14 16 syl12anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝐼 ‘ 𝑋 ) 𝐽 ( 𝐼 ‘ 𝑌 ) ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝐼 ‘ 𝑋 ) ) ∩ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝐼 ‘ 𝑌 ) ) ) ) )
18 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
19 18 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐾 ∈ OP )
20 eqid ⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
21 1 20 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 )
22 19 7 21 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 )
23 1 20 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 )
24 19 12 23 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 )
25 eqid ⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
26 1 25 3 4 dihmeet ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 ) → ( 𝐼 ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ∩ ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) )
27 6 22 24 26 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐼 ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ∩ ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) )
28 1 20 3 4 15 dochvalr2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝐼 ‘ 𝑋 ) ) = ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
29 7 28 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝐼 ‘ 𝑋 ) ) = ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
30 1 20 3 4 15 dochvalr2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝐵 ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝐼 ‘ 𝑌 ) ) = ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
31 12 30 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝐼 ‘ 𝑌 ) ) = ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
32 29 31 ineq12d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝐼 ‘ 𝑋 ) ) ∩ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝐼 ‘ 𝑌 ) ) ) = ( ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ∩ ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) )
33 27 32 eqtr4d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐼 ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝐼 ‘ 𝑋 ) ) ∩ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝐼 ‘ 𝑌 ) ) ) )
34 33 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝐼 ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝐼 ‘ 𝑋 ) ) ∩ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝐼 ‘ 𝑌 ) ) ) ) )
35 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
36 35 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐾 ∈ Lat )
37 1 25 latmcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∈ 𝐵 )
38 36 22 24 37 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∈ 𝐵 )
39 1 20 3 4 15 dochvalr2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ∈ 𝐵 ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝐼 ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) = ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) )
40 38 39 syldan ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝐼 ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) = ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) )
41 34 40 eqtr3d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝐼 ‘ 𝑋 ) ) ∩ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝐼 ‘ 𝑌 ) ) ) ) = ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) )
42 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
43 42 ad2antrr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝐾 ∈ OL )
44 1 2 25 20 oldmm4 ⊢ ( ( 𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( 𝑋 ∨ 𝑌 ) )
45 43 7 12 44 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( 𝑋 ∨ 𝑌 ) )
46 45 fveq2d ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐼 ‘ ( ( oc ‘ 𝐾 ) ‘ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( meet ‘ 𝐾 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) ) = ( 𝐼 ‘ ( 𝑋 ∨ 𝑌 ) ) )
47 17 41 46 3eqtrrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐼 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐼 ‘ 𝑋 ) 𝐽 ( 𝐼 ‘ 𝑌 ) ) )