Metamath Proof Explorer

Theorem djh01

Description: Closed subspace join with zero. (Contributed by NM, 9-Aug-2014)

Ref Expression
Hypotheses djh01.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
djh01.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
djh01.o ⊢ 0 = ( 0g ‘ 𝑈 )
djh01.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
djh01.j ⊢ ∨ = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
djh01.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
djh01.x ⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 )
Assertion djh01 ( 𝜑 → ( 𝑋 ∨ { 0 } ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 djh01.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 djh01.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 djh01.o ⊢ 0 = ( 0g ‘ 𝑈 )
4 djh01.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
5 djh01.j ⊢ ∨ = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
6 djh01.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7 djh01.x ⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 )
8 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
9 1 4 2 3 dih0rn ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → { 0 } ∈ ran 𝐼 )
10 6 9 syl ⊢ ( 𝜑 → { 0 } ∈ ran 𝐼 )
11 8 1 4 5 6 7 10 djhjlj ⊢ ( 𝜑 → ( 𝑋 ∨ { 0 } ) = ( 𝐼 ‘ ( ( ◡ 𝐼 ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ { 0 } ) ) ) )
12 eqid ⊢ ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
13 1 12 4 2 3 dih0cnv ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ◡ 𝐼 ‘ { 0 } ) = ( 0. ‘ 𝐾 ) )
14 6 13 syl ⊢ ( 𝜑 → ( ◡ 𝐼 ‘ { 0 } ) = ( 0. ‘ 𝐾 ) )
15 14 oveq2d ⊢ ( 𝜑 → ( ( ◡ 𝐼 ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ { 0 } ) ) = ( ( ◡ 𝐼 ‘ 𝑋 ) ( join ‘ 𝐾 ) ( 0. ‘ 𝐾 ) ) )
16 6 simpld ⊢ ( 𝜑 → 𝐾 ∈ HL )
17 hlol ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OL )
18 16 17 syl ⊢ ( 𝜑 → 𝐾 ∈ OL )
19 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
20 19 1 4 dihcnvcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) )
21 6 7 20 syl2anc ⊢ ( 𝜑 → ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) )
22 19 8 12 olj01 ⊢ ( ( 𝐾 ∈ OL ∧ ( ◡ 𝐼 ‘ 𝑋 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( ◡ 𝐼 ‘ 𝑋 ) ( join ‘ 𝐾 ) ( 0. ‘ 𝐾 ) ) = ( ◡ 𝐼 ‘ 𝑋 ) )
23 18 21 22 syl2anc ⊢ ( 𝜑 → ( ( ◡ 𝐼 ‘ 𝑋 ) ( join ‘ 𝐾 ) ( 0. ‘ 𝐾 ) ) = ( ◡ 𝐼 ‘ 𝑋 ) )
24 15 23 eqtrd ⊢ ( 𝜑 → ( ( ◡ 𝐼 ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ { 0 } ) ) = ( ◡ 𝐼 ‘ 𝑋 ) )
25 24 fveq2d ⊢ ( 𝜑 → ( 𝐼 ‘ ( ( ◡ 𝐼 ‘ 𝑋 ) ( join ‘ 𝐾 ) ( ◡ 𝐼 ‘ { 0 } ) ) ) = ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) )
26 1 4 dihcnvid2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) = 𝑋 )
27 6 7 26 syl2anc ⊢ ( 𝜑 → ( 𝐼 ‘ ( ◡ 𝐼 ‘ 𝑋 ) ) = 𝑋 )
28 11 25 27 3eqtrd ⊢ ( 𝜑 → ( 𝑋 ∨ { 0 } ) = 𝑋 )