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 } ∨ 𝑋 ) = 𝑋 )