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

Metamath Proof Explorer

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 biimtrdi ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝐹 ∈ ( 𝐼 ‘ 𝑋 ) → ( 𝑅 ‘ 𝐹 ) ≤ 𝑋 ) )
10 9 3impia ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ 𝐹 ∈ ( 𝐼 ‘ 𝑋 ) ) → ( 𝑅 ‘ 𝐹 ) ≤ 𝑋 )