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

Metamath Proof Explorer

Theorem dihvalrel

Description: The value of isomorphism H is a relation. (Contributed by NM, 9-Mar-2014)

Ref Expression
Hypotheses dihvalrel.h 
|- H = ( LHyp ` K )
dihvalrel.i 
|- I = ( ( DIsoH ` K ) ` W )
Assertion dihvalrel 
|- ( ( K e. HL /\ W e. H ) -> Rel ( I ` X ) )

Proof

Step Hyp Ref Expression
1 dihvalrel.h 
 |-  H = ( LHyp ` K )
2 dihvalrel.i 
 |-  I = ( ( DIsoH ` K ) ` W )
3 eqid 
 |-  ( Base ` K ) = ( Base ` K )
4 3 1 2 dihdm 
 |-  ( ( K e. HL /\ W e. H ) -> dom I = ( Base ` K ) )
5 4 eleq2d 
 |-  ( ( K e. HL /\ W e. H ) -> ( X e. dom I <-> X e. ( Base ` K ) ) )
6 eqid 
 |-  ( ( DVecH ` K ) ` W ) = ( ( DVecH ` K ) ` W )
7 eqid 
 |-  ( Base ` ( ( DVecH ` K ) ` W ) ) = ( Base ` ( ( DVecH ` K ) ` W ) )
8 3 1 2 6 7 dihss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ( Base ` K ) ) -> ( I ` X ) C_ ( Base ` ( ( DVecH ` K ) ` W ) ) )
9 eqid 
 |-  ( ( LTrn ` K ) ` W ) = ( ( LTrn ` K ) ` W )
10 eqid 
 |-  ( ( TEndo ` K ) ` W ) = ( ( TEndo ` K ) ` W )
11 1 9 10 6 7 dvhvbase 
 |-  ( ( K e. HL /\ W e. H ) -> ( Base ` ( ( DVecH ` K ) ` W ) ) = ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) )
12 11 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ( Base ` K ) ) -> ( Base ` ( ( DVecH ` K ) ` W ) ) = ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) )
13 8 12 sseqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ( Base ` K ) ) -> ( I ` X ) C_ ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) )
14 xpss 
 |-  ( ( ( LTrn ` K ) ` W ) X. ( ( TEndo ` K ) ` W ) ) C_ ( _V X. _V )
15 13 14 sstrdi 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ( Base ` K ) ) -> ( I ` X ) C_ ( _V X. _V ) )
16 df-rel 
 |-  ( Rel ( I ` X ) <-> ( I ` X ) C_ ( _V X. _V ) )
17 15 16 sylibr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ X e. ( Base ` K ) ) -> Rel ( I ` X ) )
18 17 ex 
 |-  ( ( K e. HL /\ W e. H ) -> ( X e. ( Base ` K ) -> Rel ( I ` X ) ) )
19 5 18 sylbid 
 |-  ( ( K e. HL /\ W e. H ) -> ( X e. dom I -> Rel ( I ` X ) ) )
20 rel0 
 |-  Rel (/)
21 ndmfv 
 |-  ( -. X e. dom I -> ( I ` X ) = (/) )
22 21 releqd 
 |-  ( -. X e. dom I -> ( Rel ( I ` X ) <-> Rel (/) ) )
23 20 22 mpbiri 
 |-  ( -. X e. dom I -> Rel ( I ` X ) )
24 19 23 pm2.61d1 
 |-  ( ( K e. HL /\ W e. H ) -> Rel ( I ` X ) )