Theorem diatrl

Description: Trace of a member of the partial isomorphism A. (Contributed by NM, 17-Jan-2014)

	Ref	Expression
Hypotheses	diatrl.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	diatrl.l	⊢ ≤ = ( le ‘ 𝐾 )
	diatrl.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	diatrl.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	diatrl.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
	diatrl.i	⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
Assertion	diatrl	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ ( 𝐼 ‘ 𝑋 ) ) → ( 𝑅 ‘ 𝐹 ) ≤ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		diatrl.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		diatrl.l	⊢ ≤ = ( le ‘ 𝐾 )
3		diatrl.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4		diatrl.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
5		diatrl.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
6		diatrl.i	⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
7	1 2 3 4 5 6	diaelval	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝐹 ∈ ( 𝐼 ‘ 𝑋 ) ↔ ( 𝐹 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) ≤ 𝑋 ) ) )
8		simpr	⊢ ( ( 𝐹 ∈ 𝑇 ∧ ( 𝑅 ‘ 𝐹 ) ≤ 𝑋 ) → ( 𝑅 ‘ 𝐹 ) ≤ 𝑋 )
9	7 8	syl6bi	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝐹 ∈ ( 𝐼 ‘ 𝑋 ) → ( 𝑅 ‘ 𝐹 ) ≤ 𝑋 ) )
10	9	3impia	⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ ( 𝐼 ‘ 𝑋 ) ) → ( 𝑅 ‘ 𝐹 ) ≤ 𝑋 )