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

Metamath Proof Explorer

Theorem dihjat2

Description: The subspace sum of a closed subspace and an atom is the same as their subspace join. (Contributed by NM, 1-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 dihjat2.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dihjat2.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
3 dihjat2.j ⊢ ∨ = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
4 dihjat2.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 dihjat2.p ⊢ ⊕ = ( LSSum ‘ 𝑈 )
6 dihjat2.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
7 dihjat2.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8 dihjat2.x ⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 )
9 dihjat2.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
10 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
11 eqid ⊢ ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
12 7 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑈 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13 8 adantr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑈 ) ) → 𝑋 ∈ ran 𝐼 )
14 simpr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑈 ) ) → 𝑣 ∈ ( Base ‘ 𝑈 ) )
15 1 4 10 5 11 2 3 12 13 14 dihjat1 ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑈 ) ) → ( 𝑋 ∨ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = ( 𝑋 ⊕ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) )
16 15 adantr ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑈 ) ) ∧ 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) → ( 𝑋 ∨ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) = ( 𝑋 ⊕ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) )
17 oveq2 ⊢ ( 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) → ( 𝑋 ∨ 𝑄 ) = ( 𝑋 ∨ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) )
18 17 adantl ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑈 ) ) ∧ 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) → ( 𝑋 ∨ 𝑄 ) = ( 𝑋 ∨ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) )
19 oveq2 ⊢ ( 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) → ( 𝑋 ⊕ 𝑄 ) = ( 𝑋 ⊕ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) )
20 19 adantl ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑈 ) ) ∧ 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) → ( 𝑋 ⊕ 𝑄 ) = ( 𝑋 ⊕ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) )
21 16 18 20 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( Base ‘ 𝑈 ) ) ∧ 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) ) → ( 𝑋 ∨ 𝑄 ) = ( 𝑋 ⊕ 𝑄 ) )
22 1 4 7 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
23 10 11 6 islsati ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑄 ∈ 𝐴 ) → ∃ 𝑣 ∈ ( Base ‘ 𝑈 ) 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) )
24 22 9 23 syl2anc ⊢ ( 𝜑 → ∃ 𝑣 ∈ ( Base ‘ 𝑈 ) 𝑄 = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑣 } ) )
25 21 24 r19.29a ⊢ ( 𝜑 → ( 𝑋 ∨ 𝑄 ) = ( 𝑋 ⊕ 𝑄 ) )