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

Metamath Proof Explorer

Theorem dibvalrel

Description: The value of partial isomorphism B is a relation. (Contributed by NM, 8-Mar-2014)

Ref Expression
Hypotheses dibcl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dibcl.i ⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
Assertion dibvalrel ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → Rel ( 𝐼 ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 dibcl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dibcl.i ⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
3 relxp ⊢ Rel ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) × { ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) } )
4 eqid ⊢ ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
5 1 4 2 dibdiadm ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → dom 𝐼 = dom ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) )
6 5 eleq2d ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → ( 𝑋 ∈ dom 𝐼 ↔ 𝑋 ∈ dom ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ) )
7 6 biimpa ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → 𝑋 ∈ dom ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) )
8 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
9 eqid ⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
10 eqid ⊢ ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) = ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) )
11 8 1 9 10 4 2 dibval ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝐼 ‘ 𝑋 ) = ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) × { ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) } ) )
12 7 11 syldan ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑋 ) = ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) × { ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) } ) )
13 12 releqd ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( Rel ( 𝐼 ‘ 𝑋 ) ↔ Rel ( ( ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑋 ) × { ( ℎ ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ↦ ( I ↾ ( Base ‘ 𝐾 ) ) ) } ) ) )
14 3 13 mpbiri ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ dom 𝐼 ) → Rel ( 𝐼 ‘ 𝑋 ) )
15 rel0 ⊢ Rel ∅
16 ndmfv ⊢ ( ¬ 𝑋 ∈ dom 𝐼 → ( 𝐼 ‘ 𝑋 ) = ∅ )
17 16 releqd ⊢ ( ¬ 𝑋 ∈ dom 𝐼 → ( Rel ( 𝐼 ‘ 𝑋 ) ↔ Rel ∅ ) )
18 15 17 mpbiri ⊢ ( ¬ 𝑋 ∈ dom 𝐼 → Rel ( 𝐼 ‘ 𝑋 ) )
19 18 adantl ⊢ ( ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) ∧ ¬ 𝑋 ∈ dom 𝐼 ) → Rel ( 𝐼 ‘ 𝑋 ) )
20 14 19 pm2.61dan ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑊 ∈ 𝐻 ) → Rel ( 𝐼 ‘ 𝑋 ) )