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 ⊢ H = LHyp ⁡ K
djh01.u ⊢ U = DVecH ⁡ K ⁡ W
djh01.o ⊢ 0 ˙ = 0 U
djh01.i ⊢ I = DIsoH ⁡ K ⁡ W
djh01.j ⊢ ∨ ˙ = joinH ⁡ K ⁡ W
djh01.k ⊢ φ → K ∈ HL ∧ W ∈ H
djh01.x ⊢ φ → X ∈ ran ⁡ I
Assertion djh02 ⊢ φ → 0 ˙ ∨ ˙ X = X

Proof

Step Hyp Ref Expression
1 djh01.h ⊢ H = LHyp ⁡ K
2 djh01.u ⊢ U = DVecH ⁡ K ⁡ W
3 djh01.o ⊢ 0 ˙ = 0 U
4 djh01.i ⊢ I = DIsoH ⁡ K ⁡ W
5 djh01.j ⊢ ∨ ˙ = joinH ⁡ K ⁡ W
6 djh01.k ⊢ φ → K ∈ HL ∧ W ∈ H
7 djh01.x ⊢ φ → X ∈ ran ⁡ I
8 eqid ⊢ Base U = Base U
9 1 4 2 3 dih0rn ⊢ K ∈ HL ∧ W ∈ H → 0 ˙ ∈ ran ⁡ I
10 1 2 4 8 dihrnss ⊢ K ∈ HL ∧ W ∈ H ∧ 0 ˙ ∈ ran ⁡ I → 0 ˙ ⊆ Base U
11 6 9 10 syl2anc2 ⊢ φ → 0 ˙ ⊆ Base U
12 1 2 4 8 dihrnss ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → X ⊆ Base U
13 6 7 12 syl2anc ⊢ φ → X ⊆ Base U
14 1 2 8 5 6 11 13 djhcom ⊢ φ → 0 ˙ ∨ ˙ X = X ∨ ˙ 0 ˙
15 1 2 3 4 5 6 7 djh01 ⊢ φ → X ∨ ˙ 0 ˙ = X
16 14 15 eqtrd ⊢ φ → 0 ˙ ∨ ˙ X = X