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 𝑠 A B
pwssplit4.g G = Base E
pwssplit4.z 0 ˙ = 0 R
pwssplit4.k K = y G | y A = A × 0 ˙
pwssplit4.f F = x K x B
pwssplit4.c C = R 𝑠 A
pwssplit4.d D = R 𝑠 B
pwssplit4.l L = E 𝑠 K
Assertion pwssplit4 R LMod A B V A B = F L LMIso D

Proof

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