Metamath Proof Explorer


Theorem djhjlj

Description: DVecH vector space closed subspace join in terms of lattice join. (Contributed by NM, 9-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 djhjlj ( 𝜑 → ( 𝑋 𝐽 𝑌 ) = ( 𝐼 ‘ ( ( 𝐼𝑋 ) ( 𝐼𝑌 ) ) ) )

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 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
9 8 2 3 dihcnvcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( 𝐼𝑋 ) ∈ ( Base ‘ 𝐾 ) )
10 5 6 9 syl2anc ( 𝜑 → ( 𝐼𝑋 ) ∈ ( Base ‘ 𝐾 ) )
11 8 2 3 dihcnvcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑌 ∈ ran 𝐼 ) → ( 𝐼𝑌 ) ∈ ( Base ‘ 𝐾 ) )
12 5 7 11 syl2anc ( 𝜑 → ( 𝐼𝑌 ) ∈ ( Base ‘ 𝐾 ) )
13 8 1 2 3 4 djhlj ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝐼𝑋 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝐼𝑌 ) ∈ ( Base ‘ 𝐾 ) ) ) → ( 𝐼 ‘ ( ( 𝐼𝑋 ) ( 𝐼𝑌 ) ) ) = ( ( 𝐼 ‘ ( 𝐼𝑋 ) ) 𝐽 ( 𝐼 ‘ ( 𝐼𝑌 ) ) ) )
14 5 10 12 13 syl12anc ( 𝜑 → ( 𝐼 ‘ ( ( 𝐼𝑋 ) ( 𝐼𝑌 ) ) ) = ( ( 𝐼 ‘ ( 𝐼𝑋 ) ) 𝐽 ( 𝐼 ‘ ( 𝐼𝑌 ) ) ) )
15 2 3 dihcnvid2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( 𝐼 ‘ ( 𝐼𝑋 ) ) = 𝑋 )
16 5 6 15 syl2anc ( 𝜑 → ( 𝐼 ‘ ( 𝐼𝑋 ) ) = 𝑋 )
17 2 3 dihcnvid2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑌 ∈ ran 𝐼 ) → ( 𝐼 ‘ ( 𝐼𝑌 ) ) = 𝑌 )
18 5 7 17 syl2anc ( 𝜑 → ( 𝐼 ‘ ( 𝐼𝑌 ) ) = 𝑌 )
19 16 18 oveq12d ( 𝜑 → ( ( 𝐼 ‘ ( 𝐼𝑋 ) ) 𝐽 ( 𝐼 ‘ ( 𝐼𝑌 ) ) ) = ( 𝑋 𝐽 𝑌 ) )
20 14 19 eqtr2d ( 𝜑 → ( 𝑋 𝐽 𝑌 ) = ( 𝐼 ‘ ( ( 𝐼𝑋 ) ( 𝐼𝑌 ) ) ) )