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