Metamath Proof Explorer

Theorem mapdunirnN

Description: Union of the range of the map defined by df-mapd . (Contributed by NM, 13-Mar-2015) (New usage is discouraged.)

Ref Expression
Hypotheses mapdrn.h 
|- H = ( LHyp ` K )
mapdrn.o 
|- O = ( ( ocH ` K ) ` W )
mapdrn.m 
|- M = ( ( mapd ` K ) ` W )
mapdrn.u 
|- U = ( ( DVecH ` K ) ` W )
mapdrn.f 
|- F = ( LFnl ` U )
mapdrn.l 
|- L = ( LKer ` U )
mapdunirn.c 
|- C = { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) }
mapdunirn.k 
|- ( ph -> ( K e. HL /\ W e. H ) )
Assertion mapdunirnN 
|- ( ph -> U. ran M = C )

Proof

Step Hyp Ref Expression
1 mapdrn.h 
 |-  H = ( LHyp ` K )
2 mapdrn.o 
 |-  O = ( ( ocH ` K ) ` W )
3 mapdrn.m 
 |-  M = ( ( mapd ` K ) ` W )
4 mapdrn.u 
 |-  U = ( ( DVecH ` K ) ` W )
5 mapdrn.f 
 |-  F = ( LFnl ` U )
6 mapdrn.l 
 |-  L = ( LKer ` U )
7 mapdunirn.c 
 |-  C = { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) }
8 mapdunirn.k 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
9 eqid 
 |-  ( LDual ` U ) = ( LDual ` U )
10 eqid 
 |-  ( LSubSp ` ( LDual ` U ) ) = ( LSubSp ` ( LDual ` U ) )
11 1 2 3 4 5 6 9 10 7 8 mapdrn 
 |-  ( ph -> ran M = ( ( LSubSp ` ( LDual ` U ) ) i^i ~P C ) )
12 11 unieqd 
 |-  ( ph -> U. ran M = U. ( ( LSubSp ` ( LDual ` U ) ) i^i ~P C ) )
13 uniin 
 |-  U. ( ( LSubSp ` ( LDual ` U ) ) i^i ~P C ) C_ ( U. ( LSubSp ` ( LDual ` U ) ) i^i U. ~P C )
14 eqid 
 |-  ( Base ` ( LDual ` U ) ) = ( Base ` ( LDual ` U ) )
15 1 4 8 dvhlmod 
 |-  ( ph -> U e. LMod )
16 9 15 lduallmod 
 |-  ( ph -> ( LDual ` U ) e. LMod )
17 14 10 16 lssuni 
 |-  ( ph -> U. ( LSubSp ` ( LDual ` U ) ) = ( Base ` ( LDual ` U ) ) )
18 5 9 14 15 ldualvbase 
 |-  ( ph -> ( Base ` ( LDual ` U ) ) = F )
19 17 18 eqtrd 
 |-  ( ph -> U. ( LSubSp ` ( LDual ` U ) ) = F )
20 unipw 
 |-  U. ~P C = C
21 20 a1i 
 |-  ( ph -> U. ~P C = C )
22 19 21 ineq12d 
 |-  ( ph -> ( U. ( LSubSp ` ( LDual ` U ) ) i^i U. ~P C ) = ( F i^i C ) )
23 ssrab2 
 |-  { g e. F | ( O ` ( O ` ( L ` g ) ) ) = ( L ` g ) } C_ F
24 7 23 eqsstri 
 |-  C C_ F
25 sseqin2 
 |-  ( C C_ F <-> ( F i^i C ) = C )
26 24 25 mpbi 
 |-  ( F i^i C ) = C
27 26 a1i 
 |-  ( ph -> ( F i^i C ) = C )
28 22 27 eqtrd 
 |-  ( ph -> ( U. ( LSubSp ` ( LDual ` U ) ) i^i U. ~P C ) = C )
29 13 28 sseqtrid 
 |-  ( ph -> U. ( ( LSubSp ` ( LDual ` U ) ) i^i ~P C ) C_ C )
30 1 4 2 5 6 9 10 7 8 lclkr 
 |-  ( ph -> C e. ( LSubSp ` ( LDual ` U ) ) )
31 5 fvexi 
 |-  F e. _V
32 7 31 rabex2 
 |-  C e. _V
33 32 pwid 
 |-  C e. ~P C
34 33 a1i 
 |-  ( ph -> C e. ~P C )
35 30 34 elind 
 |-  ( ph -> C e. ( ( LSubSp ` ( LDual ` U ) ) i^i ~P C ) )
36 elssuni 
 |-  ( C e. ( ( LSubSp ` ( LDual ` U ) ) i^i ~P C ) -> C C_ U. ( ( LSubSp ` ( LDual ` U ) ) i^i ~P C ) )
37 35 36 syl 
 |-  ( ph -> C C_ U. ( ( LSubSp ` ( LDual ` U ) ) i^i ~P C ) )
38 29 37 eqssd 
 |-  ( ph -> U. ( ( LSubSp ` ( LDual ` U ) ) i^i ~P C ) = C )
39 12 38 eqtrd 
 |-  ( ph -> U. ran M = C )