Metamath Proof Explorer

Theorem dihf11lem

Description: Functionality of the isomorphism H. (Contributed by NM, 6-Mar-2014)

Ref Expression
Hypotheses dihf11.b 
|- B = ( Base ` K )
dihf11.h 
|- H = ( LHyp ` K )
dihf11.i 
|- I = ( ( DIsoH ` K ) ` W )
dihf11.u 
|- U = ( ( DVecH ` K ) ` W )
dihf11.s 
|- S = ( LSubSp ` U )
Assertion dihf11lem 
|- ( ( K e. HL /\ W e. H ) -> I : B --> S )

Proof

Step Hyp Ref Expression
1 dihf11.b 
 |-  B = ( Base ` K )
2 dihf11.h 
 |-  H = ( LHyp ` K )
3 dihf11.i 
 |-  I = ( ( DIsoH ` K ) ` W )
4 dihf11.u 
 |-  U = ( ( DVecH ` K ) ` W )
5 dihf11.s 
 |-  S = ( LSubSp ` U )
6 fvex 
 |-  ( ( ( DIsoB ` K ) ` W ) ` x ) e. _V
7 riotaex 
 |-  ( iota_ u e. S A. q e. ( Atoms ` K ) ( ( -. q ( le ` K ) W /\ ( q ( join ` K ) ( x ( meet ` K ) W ) ) = x ) -> u = ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` U ) ( ( ( DIsoB ` K ) ` W ) ` ( x ( meet ` K ) W ) ) ) ) ) e. _V
8 6 7 ifex 
 |-  if ( x ( le ` K ) W , ( ( ( DIsoB ` K ) ` W ) ` x ) , ( iota_ u e. S A. q e. ( Atoms ` K ) ( ( -. q ( le ` K ) W /\ ( q ( join ` K ) ( x ( meet ` K ) W ) ) = x ) -> u = ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` U ) ( ( ( DIsoB ` K ) ` W ) ` ( x ( meet ` K ) W ) ) ) ) ) ) e. _V
9 8 rgenw 
 |-  A. x e. B if ( x ( le ` K ) W , ( ( ( DIsoB ` K ) ` W ) ` x ) , ( iota_ u e. S A. q e. ( Atoms ` K ) ( ( -. q ( le ` K ) W /\ ( q ( join ` K ) ( x ( meet ` K ) W ) ) = x ) -> u = ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` U ) ( ( ( DIsoB ` K ) ` W ) ` ( x ( meet ` K ) W ) ) ) ) ) ) e. _V
10 9 a1i 
 |-  ( ( K e. HL /\ W e. H ) -> A. x e. B if ( x ( le ` K ) W , ( ( ( DIsoB ` K ) ` W ) ` x ) , ( iota_ u e. S A. q e. ( Atoms ` K ) ( ( -. q ( le ` K ) W /\ ( q ( join ` K ) ( x ( meet ` K ) W ) ) = x ) -> u = ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` U ) ( ( ( DIsoB ` K ) ` W ) ` ( x ( meet ` K ) W ) ) ) ) ) ) e. _V )
11 eqid 
 |-  ( x e. B |-> if ( x ( le ` K ) W , ( ( ( DIsoB ` K ) ` W ) ` x ) , ( iota_ u e. S A. q e. ( Atoms ` K ) ( ( -. q ( le ` K ) W /\ ( q ( join ` K ) ( x ( meet ` K ) W ) ) = x ) -> u = ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` U ) ( ( ( DIsoB ` K ) ` W ) ` ( x ( meet ` K ) W ) ) ) ) ) ) ) = ( x e. B |-> if ( x ( le ` K ) W , ( ( ( DIsoB ` K ) ` W ) ` x ) , ( iota_ u e. S A. q e. ( Atoms ` K ) ( ( -. q ( le ` K ) W /\ ( q ( join ` K ) ( x ( meet ` K ) W ) ) = x ) -> u = ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` U ) ( ( ( DIsoB ` K ) ` W ) ` ( x ( meet ` K ) W ) ) ) ) ) ) )
12 11 mptfng 
 |-  ( A. x e. B if ( x ( le ` K ) W , ( ( ( DIsoB ` K ) ` W ) ` x ) , ( iota_ u e. S A. q e. ( Atoms ` K ) ( ( -. q ( le ` K ) W /\ ( q ( join ` K ) ( x ( meet ` K ) W ) ) = x ) -> u = ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` U ) ( ( ( DIsoB ` K ) ` W ) ` ( x ( meet ` K ) W ) ) ) ) ) ) e. _V <-> ( x e. B |-> if ( x ( le ` K ) W , ( ( ( DIsoB ` K ) ` W ) ` x ) , ( iota_ u e. S A. q e. ( Atoms ` K ) ( ( -. q ( le ` K ) W /\ ( q ( join ` K ) ( x ( meet ` K ) W ) ) = x ) -> u = ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` U ) ( ( ( DIsoB ` K ) ` W ) ` ( x ( meet ` K ) W ) ) ) ) ) ) ) Fn B )
13 10 12 sylib 
 |-  ( ( K e. HL /\ W e. H ) -> ( x e. B |-> if ( x ( le ` K ) W , ( ( ( DIsoB ` K ) ` W ) ` x ) , ( iota_ u e. S A. q e. ( Atoms ` K ) ( ( -. q ( le ` K ) W /\ ( q ( join ` K ) ( x ( meet ` K ) W ) ) = x ) -> u = ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` U ) ( ( ( DIsoB ` K ) ` W ) ` ( x ( meet ` K ) W ) ) ) ) ) ) ) Fn B )
14 eqid 
 |-  ( le ` K ) = ( le ` K )
15 eqid 
 |-  ( join ` K ) = ( join ` K )
16 eqid 
 |-  ( meet ` K ) = ( meet ` K )
17 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
18 eqid 
 |-  ( ( DIsoB ` K ) ` W ) = ( ( DIsoB ` K ) ` W )
19 eqid 
 |-  ( ( DIsoC ` K ) ` W ) = ( ( DIsoC ` K ) ` W )
20 eqid 
 |-  ( LSSum ` U ) = ( LSSum ` U )
21 1 14 15 16 17 2 3 18 19 4 5 20 dihfval 
 |-  ( ( K e. HL /\ W e. H ) -> I = ( x e. B |-> if ( x ( le ` K ) W , ( ( ( DIsoB ` K ) ` W ) ` x ) , ( iota_ u e. S A. q e. ( Atoms ` K ) ( ( -. q ( le ` K ) W /\ ( q ( join ` K ) ( x ( meet ` K ) W ) ) = x ) -> u = ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` U ) ( ( ( DIsoB ` K ) ` W ) ` ( x ( meet ` K ) W ) ) ) ) ) ) ) )
22 21 fneq1d 
 |-  ( ( K e. HL /\ W e. H ) -> ( I Fn B <-> ( x e. B |-> if ( x ( le ` K ) W , ( ( ( DIsoB ` K ) ` W ) ` x ) , ( iota_ u e. S A. q e. ( Atoms ` K ) ( ( -. q ( le ` K ) W /\ ( q ( join ` K ) ( x ( meet ` K ) W ) ) = x ) -> u = ( ( ( ( DIsoC ` K ) ` W ) ` q ) ( LSSum ` U ) ( ( ( DIsoB ` K ) ` W ) ` ( x ( meet ` K ) W ) ) ) ) ) ) ) Fn B ) )
23 13 22 mpbird 
 |-  ( ( K e. HL /\ W e. H ) -> I Fn B )
24 1 2 3 4 5 dihlss 
 |-  ( ( ( K e. HL /\ W e. H ) /\ y e. B ) -> ( I ` y ) e. S )
25 24 ralrimiva 
 |-  ( ( K e. HL /\ W e. H ) -> A. y e. B ( I ` y ) e. S )
26 fnfvrnss 
 |-  ( ( I Fn B /\ A. y e. B ( I ` y ) e. S ) -> ran I C_ S )
27 23 25 26 syl2anc 
 |-  ( ( K e. HL /\ W e. H ) -> ran I C_ S )
28 df-f 
 |-  ( I : B --> S <-> ( I Fn B /\ ran I C_ S ) )
29 23 27 28 sylanbrc 
 |-  ( ( K e. HL /\ W e. H ) -> I : B --> S )