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

Metamath Proof Explorer

Theorem dihsmatrn

Description: The subspace sum of a closed subspace and an atom is closed. TODO: see if proof at https://math.stackexchange.com/a/1233211/50776 and Mon, 13 Apr 2015 20:44:07 -0400 email could be used instead of this and dihjat2 . (Contributed by NM, 15-Jan-2015)

Ref Expression
Hypotheses dihsmatrn.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihsmatrn.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dihsmatrn.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dihsmatrn.p ⊢ ⊕ = ( LSSum ‘ 𝑈 )
dihsmatrn.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
dihsmatrn.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dihsmatrn.x ⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 )
dihsmatrn.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
Assertion dihsmatrn ( 𝜑 → ( 𝑋 ⊕ 𝑄 ) ∈ ran 𝐼 )

Proof

Step Hyp Ref Expression
1 dihsmatrn.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dihsmatrn.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
3 dihsmatrn.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dihsmatrn.p ⊢ ⊕ = ( LSSum ‘ 𝑈 )
5 dihsmatrn.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
6 dihsmatrn.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7 dihsmatrn.x ⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 )
8 dihsmatrn.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
9 eqid ⊢ ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
10 1 2 9 3 4 5 6 7 8 dihjat2 ⊢ ( 𝜑 → ( 𝑋 ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) 𝑄 ) = ( 𝑋 ⊕ 𝑄 ) )
11 10 eqcomd ⊢ ( 𝜑 → ( 𝑋 ⊕ 𝑄 ) = ( 𝑋 ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) 𝑄 ) )
12 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
13 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
14 1 3 2 13 dihrnlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → 𝑋 ∈ ( LSubSp ‘ 𝑈 ) )
15 6 7 14 syl2anc ⊢ ( 𝜑 → 𝑋 ∈ ( LSubSp ‘ 𝑈 ) )
16 1 3 6 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
17 13 5 16 8 lsatlssel ⊢ ( 𝜑 → 𝑄 ∈ ( LSubSp ‘ 𝑈 ) )
18 1 3 12 13 4 2 9 6 15 17 djhlsmcl ⊢ ( 𝜑 → ( ( 𝑋 ⊕ 𝑄 ) ∈ ran 𝐼 ↔ ( 𝑋 ⊕ 𝑄 ) = ( 𝑋 ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) 𝑄 ) ) )
19 11 18 mpbird ⊢ ( 𝜑 → ( 𝑋 ⊕ 𝑄 ) ∈ ran 𝐼 )