Metamath Proof Explorer

Theorem djhljjN

Description: Lattice join in terms of DVecH vector space closed subspace join. (Contributed by NM, 17-Aug-2014) (New usage is discouraged.)

Ref Expression
Hypotheses djhlj.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
djhlj.k ⊢ ∨ = ( join ‘ 𝐾 )
djhlj.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
djhlj.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
djhlj.j ⊢ 𝐽 = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
djhljj.w ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
djhljj.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
djhljj.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion djhljjN ( 𝜑 → ( 𝑋 ∨ 𝑌 ) = ( ◡ 𝐼 ‘ ( ( 𝐼 ‘ 𝑋 ) 𝐽 ( 𝐼 ‘ 𝑌 ) ) ) )

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 djhljj.w ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7 djhljj.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8 djhljj.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
9 1 2 3 4 5 djhlj ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐼 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐼 ‘ 𝑋 ) 𝐽 ( 𝐼 ‘ 𝑌 ) ) )
10 6 7 8 9 syl12anc ⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( ( 𝐼 ‘ 𝑋 ) 𝐽 ( 𝐼 ‘ 𝑌 ) ) )
11 1 3 4 dihcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑋 ) ∈ ran 𝐼 )
12 6 7 11 syl2anc ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑋 ) ∈ ran 𝐼 )
13 eqid ⊢ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
14 eqid ⊢ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) )
15 3 13 4 14 dihrnss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐼 ‘ 𝑋 ) ∈ ran 𝐼 ) → ( 𝐼 ‘ 𝑋 ) ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
16 6 12 15 syl2anc ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑋 ) ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
17 1 3 4 dihcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑌 ) ∈ ran 𝐼 )
18 6 8 17 syl2anc ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑌 ) ∈ ran 𝐼 )
19 3 13 4 14 dihrnss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐼 ‘ 𝑌 ) ∈ ran 𝐼 ) → ( 𝐼 ‘ 𝑌 ) ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
20 6 18 19 syl2anc ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑌 ) ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) )
21 3 4 13 14 5 djhcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝐼 ‘ 𝑋 ) ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ ( 𝐼 ‘ 𝑌 ) ⊆ ( Base ‘ ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) → ( ( 𝐼 ‘ 𝑋 ) 𝐽 ( 𝐼 ‘ 𝑌 ) ) ∈ ran 𝐼 )
22 6 16 20 21 syl12anc ⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑋 ) 𝐽 ( 𝐼 ‘ 𝑌 ) ) ∈ ran 𝐼 )
23 3 4 dihcnvid2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝐼 ‘ 𝑋 ) 𝐽 ( 𝐼 ‘ 𝑌 ) ) ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( ( 𝐼 ‘ 𝑋 ) 𝐽 ( 𝐼 ‘ 𝑌 ) ) ) ) = ( ( 𝐼 ‘ 𝑋 ) 𝐽 ( 𝐼 ‘ 𝑌 ) ) )
24 6 22 23 syl2anc ⊢ ( 𝜑 → ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( ( 𝐼 ‘ 𝑋 ) 𝐽 ( 𝐼 ‘ 𝑌 ) ) ) ) = ( ( 𝐼 ‘ 𝑋 ) 𝐽 ( 𝐼 ‘ 𝑌 ) ) )
25 10 24 eqtr4d ⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( ( 𝐼 ‘ 𝑋 ) 𝐽 ( 𝐼 ‘ 𝑌 ) ) ) ) )
26 6 simpld ⊢ ( 𝜑 → 𝐾 ∈ HL )
27 26 hllatd ⊢ ( 𝜑 → 𝐾 ∈ Lat )
28 1 2 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
29 27 7 8 28 syl3anc ⊢ ( 𝜑 → ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 )
30 1 3 4 dihcnvcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝐼 ‘ 𝑋 ) 𝐽 ( 𝐼 ‘ 𝑌 ) ) ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ ( ( 𝐼 ‘ 𝑋 ) 𝐽 ( 𝐼 ‘ 𝑌 ) ) ) ∈ 𝐵 )
31 6 22 30 syl2anc ⊢ ( 𝜑 → ( ◡ 𝐼 ‘ ( ( 𝐼 ‘ 𝑋 ) 𝐽 ( 𝐼 ‘ 𝑌 ) ) ) ∈ 𝐵 )
32 1 3 4 dih11 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∨ 𝑌 ) ∈ 𝐵 ∧ ( ◡ 𝐼 ‘ ( ( 𝐼 ‘ 𝑋 ) 𝐽 ( 𝐼 ‘ 𝑌 ) ) ) ∈ 𝐵 ) → ( ( 𝐼 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( ( 𝐼 ‘ 𝑋 ) 𝐽 ( 𝐼 ‘ 𝑌 ) ) ) ) ↔ ( 𝑋 ∨ 𝑌 ) = ( ◡ 𝐼 ‘ ( ( 𝐼 ‘ 𝑋 ) 𝐽 ( 𝐼 ‘ 𝑌 ) ) ) ) )
33 6 29 31 32 syl3anc ⊢ ( 𝜑 → ( ( 𝐼 ‘ ( 𝑋 ∨ 𝑌 ) ) = ( 𝐼 ‘ ( ◡ 𝐼 ‘ ( ( 𝐼 ‘ 𝑋 ) 𝐽 ( 𝐼 ‘ 𝑌 ) ) ) ) ↔ ( 𝑋 ∨ 𝑌 ) = ( ◡ 𝐼 ‘ ( ( 𝐼 ‘ 𝑋 ) 𝐽 ( 𝐼 ‘ 𝑌 ) ) ) ) )
34 25 33 mpbid ⊢ ( 𝜑 → ( 𝑋 ∨ 𝑌 ) = ( ◡ 𝐼 ‘ ( ( 𝐼 ‘ 𝑋 ) 𝐽 ( 𝐼 ‘ 𝑌 ) ) ) )