# 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 )`