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 ( 𝜑 → ( 𝑋 𝑄 ) = ( 𝑋 𝑄 ) )