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

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 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝐹 ∈ ( 𝐼 ‘ ( 𝑅 ‘ 𝐹 ) ) )