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 ( 𝐼𝑋 ) )