Metamath Proof Explorer


Theorem tsmsxplem2

Description: Lemma for tsmsxp . (Contributed by Mario Carneiro, 21-Sep-2015)

Ref Expression
Hypotheses tsmsxp.b B=BaseG
tsmsxp.g φGCMnd
tsmsxp.2 φGTopGrp
tsmsxp.a φAV
tsmsxp.c φCW
tsmsxp.f φF:A×CB
tsmsxp.h φH:AB
tsmsxp.1 φjAHjGtsumskCjFk
tsmsxp.j J=TopOpenG
tsmsxp.z 0˙=0G
tsmsxp.p +˙=+G
tsmsxp.m -˙=-G
tsmsxp.l φLJ
tsmsxp.3 φ0˙L
tsmsxp.k φK𝒫AFin
tsmsxp.4 φcSdTc+˙dU
tsmsxp.n φN𝒫CFin
tsmsxp.s φDK×N
tsmsxp.x φxKHx-˙GFx×NL
tsmsxp.5 φGFK×NS
tsmsxp.6 φgLKGgT
Assertion tsmsxplem2 φGHKU

Proof

Step Hyp Ref Expression
1 tsmsxp.b B=BaseG
2 tsmsxp.g φGCMnd
3 tsmsxp.2 φGTopGrp
4 tsmsxp.a φAV
5 tsmsxp.c φCW
6 tsmsxp.f φF:A×CB
7 tsmsxp.h φH:AB
8 tsmsxp.1 φjAHjGtsumskCjFk
9 tsmsxp.j J=TopOpenG
10 tsmsxp.z 0˙=0G
11 tsmsxp.p +˙=+G
12 tsmsxp.m -˙=-G
13 tsmsxp.l φLJ
14 tsmsxp.3 φ0˙L
15 tsmsxp.k φK𝒫AFin
16 tsmsxp.4 φcSdTc+˙dU
17 tsmsxp.n φN𝒫CFin
18 tsmsxp.s φDK×N
19 tsmsxp.x φxKHx-˙GFx×NL
20 tsmsxp.5 φGFK×NS
21 tsmsxp.6 φgLKGgT
22 tgpgrp GTopGrpGGrp
23 3 22 syl φGGrp
24 isabl GAbelGGrpGCMnd
25 23 2 24 sylanbrc φGAbel
26 15 elin2d φKFin
27 17 elin2d φNFin
28 xpfi KFinNFinK×NFin
29 26 27 28 syl2anc φK×NFin
30 elfpw K𝒫AFinKAKFin
31 30 simplbi K𝒫AFinKA
32 15 31 syl φKA
33 elfpw N𝒫CFinNCNFin
34 33 simplbi N𝒫CFinNC
35 17 34 syl φNC
36 xpss12 KANCK×NA×C
37 32 35 36 syl2anc φK×NA×C
38 6 37 fssresd φFK×N:K×NB
39 38 29 14 fdmfifsupp φfinSupp0˙FK×N
40 1 10 2 29 38 39 gsumcl φGFK×NB
41 7 32 fssresd φHK:KB
42 41 26 14 fdmfifsupp φfinSupp0˙HK
43 1 10 2 15 41 42 gsumcl φGHKB
44 1 11 12 ablpncan3 GAbelGFK×NBGHKBGFK×N+˙GHK-˙GFK×N=GHK
45 25 40 43 44 syl12anc φGFK×N+˙GHK-˙GFK×N=GHK
46 2 adantr φyKGCMnd
47 snfi yFin
48 27 adantr φyKNFin
49 xpfi yFinNFiny×NFin
50 47 48 49 sylancr φyKy×NFin
51 6 adantr φyKF:A×CB
52 32 sselda φyKyA
53 52 snssd φyKyA
54 35 adantr φyKNC
55 xpss12 yANCy×NA×C
56 53 54 55 syl2anc φyKy×NA×C
57 51 56 fssresd φyKFy×N:y×NB
58 10 fvexi 0˙V
59 58 a1i φyK0˙V
60 57 50 59 fdmfifsupp φyKfinSupp0˙Fy×N
61 1 10 46 50 57 60 gsumcl φyKGFy×NB
62 61 fmpttd φyKGFy×N:KB
63 eqid yKGFy×N=yKGFy×N
64 ovexd φyKGFy×NV
65 63 26 64 14 fsuppmptdm φfinSupp0˙yKGFy×N
66 1 10 12 25 15 41 62 42 65 gsumsub φGHK-˙fyKGFy×N=GHK-˙GyKGFy×N
67 fvexd φyKHyV
68 7 32 feqresmpt φHK=yKHy
69 eqidd φyKGFy×N=yKGFy×N
70 15 67 64 68 69 offval2 φHK-˙fyKGFy×N=yKHy-˙GFy×N
71 70 oveq2d φGHK-˙fyKGFy×N=GyKHy-˙GFy×N
72 cmnmnd GCMndGMnd
73 46 72 syl φyKGMnd
74 simpr φyKyK
75 51 adantr φyKzNF:A×CB
76 52 adantr φyKzNyA
77 54 sselda φyKzNzC
78 75 76 77 fovrnd φyKzNyFzB
79 78 fmpttd φyKzNyFz:NB
80 eqid zNyFz=zNyFz
81 ovexd φyKzNyFzV
82 80 48 81 59 fsuppmptdm φyKfinSupp0˙zNyFz
83 1 10 46 48 79 82 gsumcl φyKGzNyFzB
84 velsn wyw=y
85 ovres wyzNwFy×Nz=wFz
86 84 85 sylanbr w=yzNwFy×Nz=wFz
87 oveq1 w=ywFz=yFz
88 87 adantr w=yzNwFz=yFz
89 86 88 eqtrd w=yzNwFy×Nz=yFz
90 89 mpteq2dva w=yzNwFy×Nz=zNyFz
91 90 oveq2d w=yGzNwFy×Nz=GzNyFz
92 1 91 gsumsn GMndyKGzNyFzBGwyGzNwFy×Nz=GzNyFz
93 73 74 83 92 syl3anc φyKGwyGzNwFy×Nz=GzNyFz
94 47 a1i φyKyFin
95 1 10 46 94 48 57 60 gsumxp φyKGFy×N=GwyGzNwFy×Nz
96 ovres yKzNyFK×Nz=yFz
97 96 adantll φyKzNyFK×Nz=yFz
98 97 mpteq2dva φyKzNyFK×Nz=zNyFz
99 98 oveq2d φyKGzNyFK×Nz=GzNyFz
100 93 95 99 3eqtr4d φyKGFy×N=GzNyFK×Nz
101 100 mpteq2dva φyKGFy×N=yKGzNyFK×Nz
102 101 oveq2d φGyKGFy×N=GyKGzNyFK×Nz
103 1 10 2 26 27 38 39 gsumxp φGFK×N=GyKGzNyFK×Nz
104 102 103 eqtr4d φGyKGFy×N=GFK×N
105 104 oveq2d φGHK-˙GyKGFy×N=GHK-˙GFK×N
106 66 71 105 3eqtr3d φGyKHy-˙GFy×N=GHK-˙GFK×N
107 oveq2 g=yKHy-˙GFy×NGg=GyKHy-˙GFy×N
108 107 eleq1d g=yKHy-˙GFy×NGgTGyKHy-˙GFy×NT
109 fveq2 x=yHx=Hy
110 sneq x=yx=y
111 110 xpeq1d x=yx×N=y×N
112 111 reseq2d x=yFx×N=Fy×N
113 112 oveq2d x=yGFx×N=GFy×N
114 109 113 oveq12d x=yHx-˙GFx×N=Hy-˙GFy×N
115 114 eleq1d x=yHx-˙GFx×NLHy-˙GFy×NL
116 115 rspccva xKHx-˙GFx×NLyKHy-˙GFy×NL
117 19 116 sylan φyKHy-˙GFy×NL
118 117 fmpttd φyKHy-˙GFy×N:KL
119 13 15 elmapd φyKHy-˙GFy×NLKyKHy-˙GFy×N:KL
120 118 119 mpbird φyKHy-˙GFy×NLK
121 108 21 120 rspcdva φGyKHy-˙GFy×NT
122 106 121 eqeltrrd φGHK-˙GFK×NT
123 oveq1 c=GFK×Nc+˙d=GFK×N+˙d
124 123 eleq1d c=GFK×Nc+˙dUGFK×N+˙dU
125 oveq2 d=GHK-˙GFK×NGFK×N+˙d=GFK×N+˙GHK-˙GFK×N
126 125 eleq1d d=GHK-˙GFK×NGFK×N+˙dUGFK×N+˙GHK-˙GFK×NU
127 124 126 rspc2va GFK×NSGHK-˙GFK×NTcSdTc+˙dUGFK×N+˙GHK-˙GFK×NU
128 20 122 16 127 syl21anc φGFK×N+˙GHK-˙GFK×NU
129 45 128 eqeltrrd φGHKU