Theorem dih1dimb

Description: Two expressions for a 1-dimensional subspace of vector space H (when F is a nonzero vector i.e. non-identity translation). (Contributed by NM, 27-Apr-2014)

	Ref	Expression
Hypotheses	dih1dimb.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	dih1dimb.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dih1dimb.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	dih1dimb.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
	dih1dimb.o	⊢ 𝑂 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
	dih1dimb.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dih1dimb.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
	dih1dimb.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
Assertion	dih1dimb	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝐹 ) ) = ( 𝑁 ‘ { ⟨ 𝐹 , 𝑂 ⟩ } ) )

Proof

Step	Hyp	Ref	Expression
1		dih1dimb.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		dih1dimb.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3		dih1dimb.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4		dih1dimb.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
5		dih1dimb.o	⊢ 𝑂 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
6		dih1dimb.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
7		dih1dimb.i	⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
8		dih1dimb.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
9		simpl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10	1 2 3 4	trlcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐹 ) ∈ 𝐵 )
11		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
12	11 2 3 4	trlle	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑅 ‘ 𝐹 ) ( le ‘ 𝐾 ) 𝑊 )
13		eqid	⊢ ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
14	1 11 2 7 13	dihvalb	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑅 ‘ 𝐹 ) ∈ 𝐵 ∧ ( 𝑅 ‘ 𝐹 ) ( le ‘ 𝐾 ) 𝑊 ) ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝐹 ) ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑅 ‘ 𝐹 ) ) )
15	9 10 12 14	syl12anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝐹 ) ) = ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑅 ‘ 𝐹 ) ) )
16	1 2 3 4 5 6 13 8	dib1dim2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑅 ‘ 𝐹 ) ) = ( 𝑁 ‘ { ⟨ 𝐹 , 𝑂 ⟩ } ) )
17	15 16	eqtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝐹 ) ) = ( 𝑁 ‘ { ⟨ 𝐹 , 𝑂 ⟩ } ) )