Metamath Proof Explorer

Theorem djhj

Description: DVecH vector space closed subspace join in terms of lattice join. (Contributed by NM, 17-Aug-2014)

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

Proof

Step Hyp Ref Expression
1 djhj.k ⊢ ∨ = ( join ‘ 𝐾 )
2 djhj.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 djhj.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
4 djhj.j ⊢ 𝐽 = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
5 djhj.w ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
6 djhj.x ⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 )
7 djhj.y ⊢ ( 𝜑 → 𝑌 ∈ ran 𝐼 )
8 1 2 3 4 5 6 7 djhjlj ⊢ ( 𝜑 → ( 𝑋 𝐽 𝑌 ) = ( 𝐼 ‘ ( ( ◡ 𝐼 ‘ 𝑋 ) ∨ ( ◡ 𝐼 ‘ 𝑌 ) ) ) )
9 8 fveq2d ⊢ ( 𝜑 → ( ◡ 𝐼 ‘ ( 𝑋 𝐽 𝑌 ) ) = ( ◡ 𝐼 ‘ ( 𝐼 ‘ ( ( ◡ 𝐼 ‘ 𝑋 ) ∨ ( ◡ 𝐼 ‘ 𝑌 ) ) ) ) )
10 5 simpld ⊢ ( 𝜑 → 𝐾 ∈ HL )
11 10 hllatd ⊢ ( 𝜑 → 𝐾 ∈ Lat )
12 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
13 12 2 3 dihcnvcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) )
14 5 6 13 syl2anc ⊢ ( 𝜑 → ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) )
15 12 2 3 dihcnvcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
16 5 7 15 syl2anc ⊢ ( 𝜑 → ( ◡ 𝐼 ‘ 𝑌 ) ∈ ( Base ‘ 𝐾 ) )
17 12 1 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ◡ 𝐼 ‘ 𝑌 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( ◡ 𝐼 ‘ 𝑋 ) ∨ ( ◡ 𝐼 ‘ 𝑌 ) ) ∈ ( Base ‘ 𝐾 ) )
18 11 14 16 17 syl3anc ⊢ ( 𝜑 → ( ( ◡ 𝐼 ‘ 𝑋 ) ∨ ( ◡ 𝐼 ‘ 𝑌 ) ) ∈ ( Base ‘ 𝐾 ) )
19 12 2 3 dihcnvid1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( ◡ 𝐼 ‘ 𝑋 ) ∨ ( ◡ 𝐼 ‘ 𝑌 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ◡ 𝐼 ‘ ( 𝐼 ‘ ( ( ◡ 𝐼 ‘ 𝑋 ) ∨ ( ◡ 𝐼 ‘ 𝑌 ) ) ) ) = ( ( ◡ 𝐼 ‘ 𝑋 ) ∨ ( ◡ 𝐼 ‘ 𝑌 ) ) )
20 5 18 19 syl2anc ⊢ ( 𝜑 → ( ◡ 𝐼 ‘ ( 𝐼 ‘ ( ( ◡ 𝐼 ‘ 𝑋 ) ∨ ( ◡ 𝐼 ‘ 𝑌 ) ) ) ) = ( ( ◡ 𝐼 ‘ 𝑋 ) ∨ ( ◡ 𝐼 ‘ 𝑌 ) ) )
21 9 20 eqtrd ⊢ ( 𝜑 → ( ◡ 𝐼 ‘ ( 𝑋 𝐽 𝑌 ) ) = ( ( ◡ 𝐼 ‘ 𝑋 ) ∨ ( ◡ 𝐼 ‘ 𝑌 ) ) )