Metamath Proof Explorer

Theorem djhlsmat

Description: The sum of two subspace atoms equals their join. TODO: seems convoluted to go via dihprrn ; should we directly use dihjat ? (Contributed by NM, 13-Aug-2014)

Ref Expression
Hypotheses djhlsmat.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
djhlsmat.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
djhlsmat.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
djhlsmat.p ⊢ ⊕ = ( LSSum ‘ 𝑈 )
djhlsmat.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
djhlsmat.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
djhlsmat.j ⊢ ∨ = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
djhlsmat.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
djhlsmat.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
djhlsmat.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
Assertion djhlsmat ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) = ( ( 𝑁 ‘ { 𝑋 } ) ∨ ( 𝑁 ‘ { 𝑌 } ) ) )

Proof

Step Hyp Ref Expression
1 djhlsmat.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 djhlsmat.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 djhlsmat.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 djhlsmat.p ⊢ ⊕ = ( LSSum ‘ 𝑈 )
5 djhlsmat.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
6 djhlsmat.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
7 djhlsmat.j ⊢ ∨ = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
8 djhlsmat.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 djhlsmat.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
10 djhlsmat.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
11 1 2 8 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
12 9 snssd ⊢ ( 𝜑 → { 𝑋 } ⊆ 𝑉 )
13 10 snssd ⊢ ( 𝜑 → { 𝑌 } ⊆ 𝑉 )
14 3 5 4 lsmsp2 ⊢ ( ( 𝑈 ∈ LMod ∧ { 𝑋 } ⊆ 𝑉 ∧ { 𝑌 } ⊆ 𝑉 ) → ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝑁 ‘ ( { 𝑋 } ∪ { 𝑌 } ) ) )
15 11 12 13 14 syl3anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝑁 ‘ ( { 𝑋 } ∪ { 𝑌 } ) ) )
16 df-pr ⊢ { 𝑋 , 𝑌 } = ( { 𝑋 } ∪ { 𝑌 } )
17 16 fveq2i ⊢ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( 𝑁 ‘ ( { 𝑋 } ∪ { 𝑌 } ) )
18 15 17 eqtr4di ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
19 1 2 3 5 6 8 9 10 dihprrn ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ran 𝐼 )
20 18 19 eqeltrd ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∈ ran 𝐼 )
21 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
22 3 21 5 lspsncl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑈 ) )
23 11 9 22 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑈 ) )
24 3 21 5 lspsncl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) )
25 11 10 24 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) )
26 1 2 3 21 4 6 7 8 23 25 djhlsmcl ⊢ ( 𝜑 → ( ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ∈ ran 𝐼 ↔ ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) = ( ( 𝑁 ‘ { 𝑋 } ) ∨ ( 𝑁 ‘ { 𝑌 } ) ) ) )
27 20 26 mpbid ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) = ( ( 𝑁 ‘ { 𝑋 } ) ∨ ( 𝑁 ‘ { 𝑌 } ) ) )