Metamath Proof Explorer

Theorem pwssplit4

Description: Splitting for structure powers 4: maps isomorphically onto the other half. (Contributed by Stefan O'Rear, 25-Jan-2015)

Ref Expression
Hypotheses pwssplit4.e 
|- E = ( R ^s ( A u. B ) )
pwssplit4.g 
|- G = ( Base ` E )
pwssplit4.z 
|- .0. = ( 0g ` R )
pwssplit4.k 
|- K = { y e. G | ( y |` A ) = ( A X. { .0. } ) }
pwssplit4.f 
|- F = ( x e. K |-> ( x |` B ) )
pwssplit4.c 
|- C = ( R ^s A )
pwssplit4.d 
|- D = ( R ^s B )
pwssplit4.l 
|- L = ( E |`s K )
Assertion pwssplit4 
|- ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> F e. ( L LMIso D ) )

Proof

Step Hyp Ref Expression
1 pwssplit4.e 
 |-  E = ( R ^s ( A u. B ) )
2 pwssplit4.g 
 |-  G = ( Base ` E )
3 pwssplit4.z 
 |-  .0. = ( 0g ` R )
4 pwssplit4.k 
 |-  K = { y e. G | ( y |` A ) = ( A X. { .0. } ) }
5 pwssplit4.f 
 |-  F = ( x e. K |-> ( x |` B ) )
6 pwssplit4.c 
 |-  C = ( R ^s A )
7 pwssplit4.d 
 |-  D = ( R ^s B )
8 pwssplit4.l 
 |-  L = ( E |`s K )
9 ssrab2 
 |-  { y e. G | ( y |` A ) = ( A X. { .0. } ) } C_ G
10 4 9 eqsstri 
 |-  K C_ G
11 resmpt 
 |-  ( K C_ G -> ( ( x e. G |-> ( x |` B ) ) |` K ) = ( x e. K |-> ( x |` B ) ) )
12 10 11 ax-mp 
 |-  ( ( x e. G |-> ( x |` B ) ) |` K ) = ( x e. K |-> ( x |` B ) )
13 5 12 eqtr4i 
 |-  F = ( ( x e. G |-> ( x |` B ) ) |` K )
14 ssun2 
 |-  B C_ ( A u. B )
15 14 a1i 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> B C_ ( A u. B ) )
16 eqid 
 |-  ( Base ` D ) = ( Base ` D )
17 eqid 
 |-  ( x e. G |-> ( x |` B ) ) = ( x e. G |-> ( x |` B ) )
18 1 7 2 16 17 pwssplit3 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ B C_ ( A u. B ) ) -> ( x e. G |-> ( x |` B ) ) e. ( E LMHom D ) )
19 15 18 syld3an3 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> ( x e. G |-> ( x |` B ) ) e. ( E LMHom D ) )
20 simp1 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> R e. LMod )
21 lmodgrp 
 |-  ( R e. LMod -> R e. Grp )
22 grpmnd 
 |-  ( R e. Grp -> R e. Mnd )
23 20 21 22 3syl 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> R e. Mnd )
24 ssun1 
 |-  A C_ ( A u. B )
25 ssexg 
 |-  ( ( A C_ ( A u. B ) /\ ( A u. B ) e. V ) -> A e. _V )
26 24 25 mpan 
 |-  ( ( A u. B ) e. V -> A e. _V )
27 26 3ad2ant2 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> A e. _V )
28 6 3 pws0g 
 |-  ( ( R e. Mnd /\ A e. _V ) -> ( A X. { .0. } ) = ( 0g ` C ) )
29 23 27 28 syl2anc 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> ( A X. { .0. } ) = ( 0g ` C ) )
30 29 eqeq2d 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> ( ( y |` A ) = ( A X. { .0. } ) <-> ( y |` A ) = ( 0g ` C ) ) )
31 30 rabbidv 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> { y e. G | ( y |` A ) = ( A X. { .0. } ) } = { y e. G | ( y |` A ) = ( 0g ` C ) } )
32 4 31 syl5eq 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> K = { y e. G | ( y |` A ) = ( 0g ` C ) } )
33 24 a1i 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> A C_ ( A u. B ) )
34 eqid 
 |-  ( Base ` C ) = ( Base ` C )
35 eqid 
 |-  ( y e. G |-> ( y |` A ) ) = ( y e. G |-> ( y |` A ) )
36 1 6 2 34 35 pwssplit3 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ A C_ ( A u. B ) ) -> ( y e. G |-> ( y |` A ) ) e. ( E LMHom C ) )
37 33 36 syld3an3 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> ( y e. G |-> ( y |` A ) ) e. ( E LMHom C ) )
38 fvex 
 |-  ( 0g ` C ) e. _V
39 35 mptiniseg 
 |-  ( ( 0g ` C ) e. _V -> ( `' ( y e. G |-> ( y |` A ) ) " { ( 0g ` C ) } ) = { y e. G | ( y |` A ) = ( 0g ` C ) } )
40 38 39 ax-mp 
 |-  ( `' ( y e. G |-> ( y |` A ) ) " { ( 0g ` C ) } ) = { y e. G | ( y |` A ) = ( 0g ` C ) }
41 40 eqcomi 
 |-  { y e. G | ( y |` A ) = ( 0g ` C ) } = ( `' ( y e. G |-> ( y |` A ) ) " { ( 0g ` C ) } )
42 eqid 
 |-  ( 0g ` C ) = ( 0g ` C )
43 eqid 
 |-  ( LSubSp ` E ) = ( LSubSp ` E )
44 41 42 43 lmhmkerlss 
 |-  ( ( y e. G |-> ( y |` A ) ) e. ( E LMHom C ) -> { y e. G | ( y |` A ) = ( 0g ` C ) } e. ( LSubSp ` E ) )
45 37 44 syl 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> { y e. G | ( y |` A ) = ( 0g ` C ) } e. ( LSubSp ` E ) )
46 32 45 eqeltrd 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> K e. ( LSubSp ` E ) )
47 43 8 reslmhm 
 |-  ( ( ( x e. G |-> ( x |` B ) ) e. ( E LMHom D ) /\ K e. ( LSubSp ` E ) ) -> ( ( x e. G |-> ( x |` B ) ) |` K ) e. ( L LMHom D ) )
48 19 46 47 syl2anc 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> ( ( x e. G |-> ( x |` B ) ) |` K ) e. ( L LMHom D ) )
49 13 48 eqeltrid 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> F e. ( L LMHom D ) )
50 5 fvtresfn 
 |-  ( a e. K -> ( F ` a ) = ( a |` B ) )
51 ssexg 
 |-  ( ( B C_ ( A u. B ) /\ ( A u. B ) e. V ) -> B e. _V )
52 14 51 mpan 
 |-  ( ( A u. B ) e. V -> B e. _V )
53 52 3ad2ant2 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> B e. _V )
54 7 3 pws0g 
 |-  ( ( R e. Mnd /\ B e. _V ) -> ( B X. { .0. } ) = ( 0g ` D ) )
55 23 53 54 syl2anc 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> ( B X. { .0. } ) = ( 0g ` D ) )
56 55 eqcomd 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> ( 0g ` D ) = ( B X. { .0. } ) )
57 50 56 eqeqan12rd 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. K ) -> ( ( F ` a ) = ( 0g ` D ) <-> ( a |` B ) = ( B X. { .0. } ) ) )
58 reseq1 
 |-  ( y = a -> ( y |` A ) = ( a |` A ) )
59 58 eqeq1d 
 |-  ( y = a -> ( ( y |` A ) = ( A X. { .0. } ) <-> ( a |` A ) = ( A X. { .0. } ) ) )
60 59 4 elrab2 
 |-  ( a e. K <-> ( a e. G /\ ( a |` A ) = ( A X. { .0. } ) ) )
61 uneq12 
 |-  ( ( ( a |` A ) = ( A X. { .0. } ) /\ ( a |` B ) = ( B X. { .0. } ) ) -> ( ( a |` A ) u. ( a |` B ) ) = ( ( A X. { .0. } ) u. ( B X. { .0. } ) ) )
62 resundi 
 |-  ( a |` ( A u. B ) ) = ( ( a |` A ) u. ( a |` B ) )
63 xpundir 
 |-  ( ( A u. B ) X. { .0. } ) = ( ( A X. { .0. } ) u. ( B X. { .0. } ) )
64 61 62 63 3eqtr4g 
 |-  ( ( ( a |` A ) = ( A X. { .0. } ) /\ ( a |` B ) = ( B X. { .0. } ) ) -> ( a |` ( A u. B ) ) = ( ( A u. B ) X. { .0. } ) )
65 64 adantll 
 |-  ( ( ( a e. G /\ ( a |` A ) = ( A X. { .0. } ) ) /\ ( a |` B ) = ( B X. { .0. } ) ) -> ( a |` ( A u. B ) ) = ( ( A u. B ) X. { .0. } ) )
66 65 adantl 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ ( ( a e. G /\ ( a |` A ) = ( A X. { .0. } ) ) /\ ( a |` B ) = ( B X. { .0. } ) ) ) -> ( a |` ( A u. B ) ) = ( ( A u. B ) X. { .0. } ) )
67 eqid 
 |-  ( Base ` R ) = ( Base ` R )
68 simpl1 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ ( ( a e. G /\ ( a |` A ) = ( A X. { .0. } ) ) /\ ( a |` B ) = ( B X. { .0. } ) ) ) -> R e. LMod )
69 simp2 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> ( A u. B ) e. V )
70 69 adantr 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ ( ( a e. G /\ ( a |` A ) = ( A X. { .0. } ) ) /\ ( a |` B ) = ( B X. { .0. } ) ) ) -> ( A u. B ) e. V )
71 simprll 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ ( ( a e. G /\ ( a |` A ) = ( A X. { .0. } ) ) /\ ( a |` B ) = ( B X. { .0. } ) ) ) -> a e. G )
72 1 67 2 68 70 71 pwselbas 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ ( ( a e. G /\ ( a |` A ) = ( A X. { .0. } ) ) /\ ( a |` B ) = ( B X. { .0. } ) ) ) -> a : ( A u. B ) --> ( Base ` R ) )
73 ffn 
 |-  ( a : ( A u. B ) --> ( Base ` R ) -> a Fn ( A u. B ) )
74 fnresdm 
 |-  ( a Fn ( A u. B ) -> ( a |` ( A u. B ) ) = a )
75 72 73 74 3syl 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ ( ( a e. G /\ ( a |` A ) = ( A X. { .0. } ) ) /\ ( a |` B ) = ( B X. { .0. } ) ) ) -> ( a |` ( A u. B ) ) = a )
76 1 3 pws0g 
 |-  ( ( R e. Mnd /\ ( A u. B ) e. V ) -> ( ( A u. B ) X. { .0. } ) = ( 0g ` E ) )
77 23 69 76 syl2anc 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> ( ( A u. B ) X. { .0. } ) = ( 0g ` E ) )
78 1 pwslmod 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V ) -> E e. LMod )
79 78 3adant3 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> E e. LMod )
80 43 lsssubg 
 |-  ( ( E e. LMod /\ K e. ( LSubSp ` E ) ) -> K e. ( SubGrp ` E ) )
81 79 46 80 syl2anc 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> K e. ( SubGrp ` E ) )
82 eqid 
 |-  ( 0g ` E ) = ( 0g ` E )
83 8 82 subg0 
 |-  ( K e. ( SubGrp ` E ) -> ( 0g ` E ) = ( 0g ` L ) )
84 81 83 syl 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> ( 0g ` E ) = ( 0g ` L ) )
85 77 84 eqtrd 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> ( ( A u. B ) X. { .0. } ) = ( 0g ` L ) )
86 85 adantr 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ ( ( a e. G /\ ( a |` A ) = ( A X. { .0. } ) ) /\ ( a |` B ) = ( B X. { .0. } ) ) ) -> ( ( A u. B ) X. { .0. } ) = ( 0g ` L ) )
87 66 75 86 3eqtr3d 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ ( ( a e. G /\ ( a |` A ) = ( A X. { .0. } ) ) /\ ( a |` B ) = ( B X. { .0. } ) ) ) -> a = ( 0g ` L ) )
88 87 exp32 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> ( ( a e. G /\ ( a |` A ) = ( A X. { .0. } ) ) -> ( ( a |` B ) = ( B X. { .0. } ) -> a = ( 0g ` L ) ) ) )
89 60 88 syl5bi 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> ( a e. K -> ( ( a |` B ) = ( B X. { .0. } ) -> a = ( 0g ` L ) ) ) )
90 89 imp 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. K ) -> ( ( a |` B ) = ( B X. { .0. } ) -> a = ( 0g ` L ) ) )
91 57 90 sylbid 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. K ) -> ( ( F ` a ) = ( 0g ` D ) -> a = ( 0g ` L ) ) )
92 91 ralrimiva 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> A. a e. K ( ( F ` a ) = ( 0g ` D ) -> a = ( 0g ` L ) ) )
93 lmghm 
 |-  ( F e. ( L LMHom D ) -> F e. ( L GrpHom D ) )
94 8 2 ressbas2 
 |-  ( K C_ G -> K = ( Base ` L ) )
95 10 94 ax-mp 
 |-  K = ( Base ` L )
96 eqid 
 |-  ( 0g ` L ) = ( 0g ` L )
97 eqid 
 |-  ( 0g ` D ) = ( 0g ` D )
98 95 16 96 97 ghmf1 
 |-  ( F e. ( L GrpHom D ) -> ( F : K -1-1-> ( Base ` D ) <-> A. a e. K ( ( F ` a ) = ( 0g ` D ) -> a = ( 0g ` L ) ) ) )
99 49 93 98 3syl 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> ( F : K -1-1-> ( Base ` D ) <-> A. a e. K ( ( F ` a ) = ( 0g ` D ) -> a = ( 0g ` L ) ) ) )
100 92 99 mpbird 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> F : K -1-1-> ( Base ` D ) )
101 eqid 
 |-  ( Base ` L ) = ( Base ` L )
102 101 16 lmhmf 
 |-  ( F e. ( L LMHom D ) -> F : ( Base ` L ) --> ( Base ` D ) )
103 frn 
 |-  ( F : ( Base ` L ) --> ( Base ` D ) -> ran F C_ ( Base ` D ) )
104 49 102 103 3syl 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> ran F C_ ( Base ` D ) )
105 reseq1 
 |-  ( x = ( a u. ( A X. { .0. } ) ) -> ( x |` B ) = ( ( a u. ( A X. { .0. } ) ) |` B ) )
106 7 67 16 pwselbasb 
 |-  ( ( R e. LMod /\ B e. _V ) -> ( a e. ( Base ` D ) <-> a : B --> ( Base ` R ) ) )
107 20 53 106 syl2anc 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> ( a e. ( Base ` D ) <-> a : B --> ( Base ` R ) ) )
108 107 biimpa 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. ( Base ` D ) ) -> a : B --> ( Base ` R ) )
109 3 fvexi 
 |-  .0. e. _V
110 109 fconst 
 |-  ( A X. { .0. } ) : A --> { .0. }
111 110 a1i 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. ( Base ` D ) ) -> ( A X. { .0. } ) : A --> { .0. } )
112 23 adantr 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. ( Base ` D ) ) -> R e. Mnd )
113 67 3 mndidcl 
 |-  ( R e. Mnd -> .0. e. ( Base ` R ) )
114 112 113 syl 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. ( Base ` D ) ) -> .0. e. ( Base ` R ) )
115 114 snssd 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. ( Base ` D ) ) -> { .0. } C_ ( Base ` R ) )
116 111 115 fssd 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. ( Base ` D ) ) -> ( A X. { .0. } ) : A --> ( Base ` R ) )
117 incom 
 |-  ( B i^i A ) = ( A i^i B )
118 simp3 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> ( A i^i B ) = (/) )
119 117 118 syl5eq 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> ( B i^i A ) = (/) )
120 119 adantr 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. ( Base ` D ) ) -> ( B i^i A ) = (/) )
121 fun 
 |-  ( ( ( a : B --> ( Base ` R ) /\ ( A X. { .0. } ) : A --> ( Base ` R ) ) /\ ( B i^i A ) = (/) ) -> ( a u. ( A X. { .0. } ) ) : ( B u. A ) --> ( ( Base ` R ) u. ( Base ` R ) ) )
122 108 116 120 121 syl21anc 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. ( Base ` D ) ) -> ( a u. ( A X. { .0. } ) ) : ( B u. A ) --> ( ( Base ` R ) u. ( Base ` R ) ) )
123 uncom 
 |-  ( B u. A ) = ( A u. B )
124 unidm 
 |-  ( ( Base ` R ) u. ( Base ` R ) ) = ( Base ` R )
125 123 124 feq23i 
 |-  ( ( a u. ( A X. { .0. } ) ) : ( B u. A ) --> ( ( Base ` R ) u. ( Base ` R ) ) <-> ( a u. ( A X. { .0. } ) ) : ( A u. B ) --> ( Base ` R ) )
126 122 125 sylib 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. ( Base ` D ) ) -> ( a u. ( A X. { .0. } ) ) : ( A u. B ) --> ( Base ` R ) )
127 1 67 2 pwselbasb 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V ) -> ( ( a u. ( A X. { .0. } ) ) e. G <-> ( a u. ( A X. { .0. } ) ) : ( A u. B ) --> ( Base ` R ) ) )
128 127 3adant3 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> ( ( a u. ( A X. { .0. } ) ) e. G <-> ( a u. ( A X. { .0. } ) ) : ( A u. B ) --> ( Base ` R ) ) )
129 128 adantr 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. ( Base ` D ) ) -> ( ( a u. ( A X. { .0. } ) ) e. G <-> ( a u. ( A X. { .0. } ) ) : ( A u. B ) --> ( Base ` R ) ) )
130 126 129 mpbird 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. ( Base ` D ) ) -> ( a u. ( A X. { .0. } ) ) e. G )
131 simpl3 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. ( Base ` D ) ) -> ( A i^i B ) = (/) )
132 117 131 syl5eq 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. ( Base ` D ) ) -> ( B i^i A ) = (/) )
133 ffn 
 |-  ( a : B --> ( Base ` R ) -> a Fn B )
134 fnresdisj 
 |-  ( a Fn B -> ( ( B i^i A ) = (/) <-> ( a |` A ) = (/) ) )
135 108 133 134 3syl 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. ( Base ` D ) ) -> ( ( B i^i A ) = (/) <-> ( a |` A ) = (/) ) )
136 132 135 mpbid 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. ( Base ` D ) ) -> ( a |` A ) = (/) )
137 fnconstg 
 |-  ( .0. e. _V -> ( A X. { .0. } ) Fn A )
138 fnresdm 
 |-  ( ( A X. { .0. } ) Fn A -> ( ( A X. { .0. } ) |` A ) = ( A X. { .0. } ) )
139 109 137 138 mp2b 
 |-  ( ( A X. { .0. } ) |` A ) = ( A X. { .0. } )
140 139 a1i 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. ( Base ` D ) ) -> ( ( A X. { .0. } ) |` A ) = ( A X. { .0. } ) )
141 136 140 uneq12d 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. ( Base ` D ) ) -> ( ( a |` A ) u. ( ( A X. { .0. } ) |` A ) ) = ( (/) u. ( A X. { .0. } ) ) )
142 resundir 
 |-  ( ( a u. ( A X. { .0. } ) ) |` A ) = ( ( a |` A ) u. ( ( A X. { .0. } ) |` A ) )
143 uncom 
 |-  ( (/) u. ( A X. { .0. } ) ) = ( ( A X. { .0. } ) u. (/) )
144 un0 
 |-  ( ( A X. { .0. } ) u. (/) ) = ( A X. { .0. } )
145 143 144 eqtr2i 
 |-  ( A X. { .0. } ) = ( (/) u. ( A X. { .0. } ) )
146 141 142 145 3eqtr4g 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. ( Base ` D ) ) -> ( ( a u. ( A X. { .0. } ) ) |` A ) = ( A X. { .0. } ) )
147 reseq1 
 |-  ( y = ( a u. ( A X. { .0. } ) ) -> ( y |` A ) = ( ( a u. ( A X. { .0. } ) ) |` A ) )
148 147 eqeq1d 
 |-  ( y = ( a u. ( A X. { .0. } ) ) -> ( ( y |` A ) = ( A X. { .0. } ) <-> ( ( a u. ( A X. { .0. } ) ) |` A ) = ( A X. { .0. } ) ) )
149 148 4 elrab2 
 |-  ( ( a u. ( A X. { .0. } ) ) e. K <-> ( ( a u. ( A X. { .0. } ) ) e. G /\ ( ( a u. ( A X. { .0. } ) ) |` A ) = ( A X. { .0. } ) ) )
150 130 146 149 sylanbrc 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. ( Base ` D ) ) -> ( a u. ( A X. { .0. } ) ) e. K )
151 130 resexd 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. ( Base ` D ) ) -> ( ( a u. ( A X. { .0. } ) ) |` B ) e. _V )
152 5 105 150 151 fvmptd3 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. ( Base ` D ) ) -> ( F ` ( a u. ( A X. { .0. } ) ) ) = ( ( a u. ( A X. { .0. } ) ) |` B ) )
153 resundir 
 |-  ( ( a u. ( A X. { .0. } ) ) |` B ) = ( ( a |` B ) u. ( ( A X. { .0. } ) |` B ) )
154 fnresdm 
 |-  ( a Fn B -> ( a |` B ) = a )
155 108 133 154 3syl 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. ( Base ` D ) ) -> ( a |` B ) = a )
156 ffn 
 |-  ( ( A X. { .0. } ) : A --> { .0. } -> ( A X. { .0. } ) Fn A )
157 fnresdisj 
 |-  ( ( A X. { .0. } ) Fn A -> ( ( A i^i B ) = (/) <-> ( ( A X. { .0. } ) |` B ) = (/) ) )
158 110 156 157 mp2b 
 |-  ( ( A i^i B ) = (/) <-> ( ( A X. { .0. } ) |` B ) = (/) )
159 158 biimpi 
 |-  ( ( A i^i B ) = (/) -> ( ( A X. { .0. } ) |` B ) = (/) )
160 159 3ad2ant3 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> ( ( A X. { .0. } ) |` B ) = (/) )
161 160 adantr 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. ( Base ` D ) ) -> ( ( A X. { .0. } ) |` B ) = (/) )
162 155 161 uneq12d 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. ( Base ` D ) ) -> ( ( a |` B ) u. ( ( A X. { .0. } ) |` B ) ) = ( a u. (/) ) )
163 un0 
 |-  ( a u. (/) ) = a
164 162 163 eqtrdi 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. ( Base ` D ) ) -> ( ( a |` B ) u. ( ( A X. { .0. } ) |` B ) ) = a )
165 153 164 syl5eq 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. ( Base ` D ) ) -> ( ( a u. ( A X. { .0. } ) ) |` B ) = a )
166 152 165 eqtrd 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. ( Base ` D ) ) -> ( F ` ( a u. ( A X. { .0. } ) ) ) = a )
167 95 16 lmhmf 
 |-  ( F e. ( L LMHom D ) -> F : K --> ( Base ` D ) )
168 ffn 
 |-  ( F : K --> ( Base ` D ) -> F Fn K )
169 49 167 168 3syl 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> F Fn K )
170 169 adantr 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. ( Base ` D ) ) -> F Fn K )
171 fnfvelrn 
 |-  ( ( F Fn K /\ ( a u. ( A X. { .0. } ) ) e. K ) -> ( F ` ( a u. ( A X. { .0. } ) ) ) e. ran F )
172 170 150 171 syl2anc 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. ( Base ` D ) ) -> ( F ` ( a u. ( A X. { .0. } ) ) ) e. ran F )
173 166 172 eqeltrrd 
 |-  ( ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) /\ a e. ( Base ` D ) ) -> a e. ran F )
174 104 173 eqelssd 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> ran F = ( Base ` D ) )
175 dff1o5 
 |-  ( F : K -1-1-onto-> ( Base ` D ) <-> ( F : K -1-1-> ( Base ` D ) /\ ran F = ( Base ` D ) ) )
176 100 174 175 sylanbrc 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> F : K -1-1-onto-> ( Base ` D ) )
177 95 16 islmim 
 |-  ( F e. ( L LMIso D ) <-> ( F e. ( L LMHom D ) /\ F : K -1-1-onto-> ( Base ` D ) ) )
178 49 176 177 sylanbrc 
 |-  ( ( R e. LMod /\ ( A u. B ) e. V /\ ( A i^i B ) = (/) ) -> F e. ( L LMIso D ) )