This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem djh02

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 djh02 ( 𝜑 → ( { 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 ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
9 1 4 2 3 dih0rn ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → { 0 } ∈ ran 𝐼 )
10 1 2 4 8 dihrnss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { 0 } ∈ ran 𝐼 ) → { 0 } ⊆ ( Base ‘ 𝑈 ) )
11 6 9 10 syl2anc2 ⊢ ( 𝜑 → { 0 } ⊆ ( Base ‘ 𝑈 ) )
12 1 2 4 8 dihrnss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → 𝑋 ⊆ ( Base ‘ 𝑈 ) )
13 6 7 12 syl2anc ⊢ ( 𝜑 → 𝑋 ⊆ ( Base ‘ 𝑈 ) )
14 1 2 8 5 6 11 13 djhcom ⊢ ( 𝜑 → ( { 0 } ∨ 𝑋 ) = ( 𝑋 ∨ { 0 } ) )
15 1 2 3 4 5 6 7 djh01 ⊢ ( 𝜑 → ( 𝑋 ∨ { 0 } ) = 𝑋 )
16 14 15 eqtrd ⊢ ( 𝜑 → ( { 0 } ∨ 𝑋 ) = 𝑋 )