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

Metamath Proof Explorer

Theorem djhlsmcl

Description: A closed subspace sum equals subspace join. ( shjshseli analog.) (Contributed by NM, 13-Aug-2014)

Ref Expression
Hypotheses djhlsmcl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
djhlsmcl.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
djhlsmcl.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
djhlsmcl.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
djhlsmcl.p ⊢ ⊕ = ( LSSum ‘ 𝑈 )
djhlsmcl.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
djhlsmcl.j ⊢ ∨ = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
djhlsmcl.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
djhlsmcl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
djhlsmcl.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
Assertion djhlsmcl ( 𝜑 → ( ( 𝑋 ⊕ 𝑌 ) ∈ ran 𝐼 ↔ ( 𝑋 ⊕ 𝑌 ) = ( 𝑋 ∨ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 djhlsmcl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 djhlsmcl.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 djhlsmcl.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 djhlsmcl.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
5 djhlsmcl.p ⊢ ⊕ = ( LSSum ‘ 𝑈 )
6 djhlsmcl.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
7 djhlsmcl.j ⊢ ∨ = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
8 djhlsmcl.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 djhlsmcl.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
10 djhlsmcl.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
11 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ⊕ 𝑌 ) ∈ ran 𝐼 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12 3 4 lssss ⊢ ( 𝑋 ∈ 𝑆 → 𝑋 ⊆ 𝑉 )
13 9 12 syl ⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
14 13 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ⊕ 𝑌 ) ∈ ran 𝐼 ) → 𝑋 ⊆ 𝑉 )
15 3 4 lssss ⊢ ( 𝑌 ∈ 𝑆 → 𝑌 ⊆ 𝑉 )
16 10 15 syl ⊢ ( 𝜑 → 𝑌 ⊆ 𝑉 )
17 16 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ⊕ 𝑌 ) ∈ ran 𝐼 ) → 𝑌 ⊆ 𝑉 )
18 eqid ⊢ ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
19 1 2 3 18 7 djhval2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ) → ( 𝑋 ∨ 𝑌 ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ∪ 𝑌 ) ) ) )
20 11 14 17 19 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑋 ⊕ 𝑌 ) ∈ ran 𝐼 ) → ( 𝑋 ∨ 𝑌 ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ∪ 𝑌 ) ) ) )
21 1 2 8 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
22 21 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ⊕ 𝑌 ) ∈ ran 𝐼 ) → 𝑈 ∈ LMod )
23 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ⊕ 𝑌 ) ∈ ran 𝐼 ) → 𝑋 ∈ 𝑆 )
24 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ⊕ 𝑌 ) ∈ ran 𝐼 ) → 𝑌 ∈ 𝑆 )
25 eqid ⊢ ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
26 4 25 5 lsmsp ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑋 ⊕ 𝑌 ) = ( ( LSpan ‘ 𝑈 ) ‘ ( 𝑋 ∪ 𝑌 ) ) )
27 22 23 24 26 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑋 ⊕ 𝑌 ) ∈ ran 𝐼 ) → ( 𝑋 ⊕ 𝑌 ) = ( ( LSpan ‘ 𝑈 ) ‘ ( 𝑋 ∪ 𝑌 ) ) )
28 27 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑋 ⊕ 𝑌 ) ∈ ran 𝐼 ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ⊕ 𝑌 ) ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LSpan ‘ 𝑈 ) ‘ ( 𝑋 ∪ 𝑌 ) ) ) )
29 13 16 unssd ⊢ ( 𝜑 → ( 𝑋 ∪ 𝑌 ) ⊆ 𝑉 )
30 29 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ⊕ 𝑌 ) ∈ ran 𝐼 ) → ( 𝑋 ∪ 𝑌 ) ⊆ 𝑉 )
31 1 2 18 3 25 11 30 dochocsp ⊢ ( ( 𝜑 ∧ ( 𝑋 ⊕ 𝑌 ) ∈ ran 𝐼 ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( LSpan ‘ 𝑈 ) ‘ ( 𝑋 ∪ 𝑌 ) ) ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ∪ 𝑌 ) ) )
32 28 31 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑋 ⊕ 𝑌 ) ∈ ran 𝐼 ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ⊕ 𝑌 ) ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ∪ 𝑌 ) ) )
33 32 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑋 ⊕ 𝑌 ) ∈ ran 𝐼 ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ⊕ 𝑌 ) ) ) = ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ∪ 𝑌 ) ) ) )
34 1 6 18 dochoc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊕ 𝑌 ) ∈ ran 𝐼 ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ⊕ 𝑌 ) ) ) = ( 𝑋 ⊕ 𝑌 ) )
35 8 34 sylan ⊢ ( ( 𝜑 ∧ ( 𝑋 ⊕ 𝑌 ) ∈ ran 𝐼 ) → ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ocH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ⊕ 𝑌 ) ) ) = ( 𝑋 ⊕ 𝑌 ) )
36 20 33 35 3eqtr2rd ⊢ ( ( 𝜑 ∧ ( 𝑋 ⊕ 𝑌 ) ∈ ran 𝐼 ) → ( 𝑋 ⊕ 𝑌 ) = ( 𝑋 ∨ 𝑌 ) )
37 36 ex ⊢ ( 𝜑 → ( ( 𝑋 ⊕ 𝑌 ) ∈ ran 𝐼 → ( 𝑋 ⊕ 𝑌 ) = ( 𝑋 ∨ 𝑌 ) ) )
38 1 6 2 3 7 djhcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ⊆ 𝑉 ∧ 𝑌 ⊆ 𝑉 ) ) → ( 𝑋 ∨ 𝑌 ) ∈ ran 𝐼 )
39 8 13 16 38 syl12anc ⊢ ( 𝜑 → ( 𝑋 ∨ 𝑌 ) ∈ ran 𝐼 )
40 eleq1a ⊢ ( ( 𝑋 ∨ 𝑌 ) ∈ ran 𝐼 → ( ( 𝑋 ⊕ 𝑌 ) = ( 𝑋 ∨ 𝑌 ) → ( 𝑋 ⊕ 𝑌 ) ∈ ran 𝐼 ) )
41 39 40 syl ⊢ ( 𝜑 → ( ( 𝑋 ⊕ 𝑌 ) = ( 𝑋 ∨ 𝑌 ) → ( 𝑋 ⊕ 𝑌 ) ∈ ran 𝐼 ) )
42 37 41 impbid ⊢ ( 𝜑 → ( ( 𝑋 ⊕ 𝑌 ) ∈ ran 𝐼 ↔ ( 𝑋 ⊕ 𝑌 ) = ( 𝑋 ∨ 𝑌 ) ) )