Metamath Proof Explorer


Theorem dia1dimid

Description: A vector (translation) belongs to the 1-dim subspace it generates. (Contributed by NM, 8-Sep-2014)

Ref Expression
Hypotheses dia1dimid.h 𝐻 = ( LHyp ‘ 𝐾 )
dia1dimid.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dia1dimid.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
dia1dimid.i 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
Assertion dia1dimid ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → 𝐹 ∈ ( 𝐼 ‘ ( 𝑅𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 dia1dimid.h 𝐻 = ( LHyp ‘ 𝐾 )
2 dia1dimid.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 dia1dimid.r 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
4 dia1dimid.i 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
5 eqid ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
6 1 5 dvalvec ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) ∈ LVec )
7 lveclmod ( ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) ∈ LVec → ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) ∈ LMod )
8 6 7 syl ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) ∈ LMod )
9 8 adantr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) ∈ LMod )
10 eqid ( Base ‘ ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) )
11 1 2 5 10 dvavbase ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( Base ‘ ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) ) = 𝑇 )
12 11 eleq2d ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( 𝐹 ∈ ( Base ‘ ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) ) ↔ 𝐹𝑇 ) )
13 12 biimpar ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → 𝐹 ∈ ( Base ‘ ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) ) )
14 eqid ( LSpan ‘ ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) ) = ( LSpan ‘ ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) )
15 10 14 lspsnid ( ( ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) ∈ LMod ∧ 𝐹 ∈ ( Base ‘ ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) ) ) → 𝐹 ∈ ( ( LSpan ‘ ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ { 𝐹 } ) )
16 9 13 15 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → 𝐹 ∈ ( ( LSpan ‘ ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ { 𝐹 } ) )
17 1 2 3 5 4 14 dia1dim2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → ( 𝐼 ‘ ( 𝑅𝐹 ) ) = ( ( LSpan ‘ ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 ) ) ‘ { 𝐹 } ) )
18 16 17 eleqtrrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → 𝐹 ∈ ( 𝐼 ‘ ( 𝑅𝐹 ) ) )