Metamath Proof Explorer


Theorem nsgqusf1olem1

Description: Lemma for nsgqusf1o . (Contributed by Thierry Arnoux, 4-Aug-2024)

Ref Expression
Hypotheses nsgqusf1o.b B=BaseG
nsgqusf1o.s S=hSubGrpG|Nh
nsgqusf1o.t T=SubGrpQ
nsgqusf1o.1 ˙=toIncS
nsgqusf1o.2 No typesetting found for |- .c_ = ( le ` ( toInc ` T ) ) with typecode |-
nsgqusf1o.q Q=G/𝑠G~QGN
nsgqusf1o.p ˙=LSSumG
nsgqusf1o.e E=hSranxhx˙N
nsgqusf1o.f F=fTaB|a˙Nf
nsgqusf1o.n φNNrmSGrpG
Assertion nsgqusf1olem1 φhSubGrpGNhranxhx˙NT

Proof

Step Hyp Ref Expression
1 nsgqusf1o.b B=BaseG
2 nsgqusf1o.s S=hSubGrpG|Nh
3 nsgqusf1o.t T=SubGrpQ
4 nsgqusf1o.1 ˙=toIncS
5 nsgqusf1o.2 Could not format .c_ = ( le ` ( toInc ` T ) ) : No typesetting found for |- .c_ = ( le ` ( toInc ` T ) ) with typecode |-
6 nsgqusf1o.q Q=G/𝑠G~QGN
7 nsgqusf1o.p ˙=LSSumG
8 nsgqusf1o.e E=hSranxhx˙N
9 nsgqusf1o.f F=fTaB|a˙Nf
10 nsgqusf1o.n φNNrmSGrpG
11 6 qusgrp NNrmSGrpGQGrp
12 10 11 syl φQGrp
13 12 ad2antrr φhSubGrpGNhQGrp
14 1 subgss hSubGrpGhB
15 14 ad2antlr φhSubGrpGNhhB
16 15 sselda φhSubGrpGNhxhxB
17 ovex G~QGNV
18 17 ecelqsi xBxG~QGNB/G~QGN
19 16 18 syl φhSubGrpGNhxhxG~QGNB/G~QGN
20 nsgsubg NNrmSGrpGNSubGrpG
21 10 20 syl φNSubGrpG
22 21 ad3antrrr φhSubGrpGNhxhNSubGrpG
23 1 7 22 16 quslsm φhSubGrpGNhxhxG~QGN=x˙N
24 6 a1i φQ=G/𝑠G~QGN
25 1 a1i φB=BaseG
26 ovexd φG~QGNV
27 subgrcl NSubGrpGGGrp
28 21 27 syl φGGrp
29 24 25 26 28 qusbas φB/G~QGN=BaseQ
30 29 ad3antrrr φhSubGrpGNhxhB/G~QGN=BaseQ
31 19 23 30 3eltr3d φhSubGrpGNhxhx˙NBaseQ
32 31 ralrimiva φhSubGrpGNhxhx˙NBaseQ
33 eqid xhx˙N=xhx˙N
34 33 rnmptss xhx˙NBaseQranxhx˙NBaseQ
35 32 34 syl φhSubGrpGNhranxhx˙NBaseQ
36 nfv xφhSubGrpGNh
37 ovexd φhSubGrpGNhxhx˙NV
38 eqid 0G=0G
39 38 subg0cl hSubGrpG0Gh
40 39 ne0d hSubGrpGh
41 40 ad2antlr φhSubGrpGNhh
42 36 37 33 41 rnmptn0 φhSubGrpGNhranxhx˙N
43 nfmpt1 _xxhx˙N
44 43 nfrn _xranxhx˙N
45 44 nfel2 xiranxhx˙N
46 36 45 nfan xφhSubGrpGNhiranxhx˙N
47 44 nfel2 xi+Qjranxhx˙N
48 44 47 nfralw xjranxhx˙Ni+Qjranxhx˙N
49 44 nfel2 xinvgQiranxhx˙N
50 48 49 nfan xjranxhx˙Ni+Qjranxhx˙NinvgQiranxhx˙N
51 sneq x=zx=z
52 51 oveq1d x=zx˙N=z˙N
53 52 cbvmptv xhx˙N=zhz˙N
54 simp-4r φhSubGrpGNhxhi=x˙NhSubGrpG
55 54 ad2antrr φhSubGrpGNhxhi=x˙Nyhj=y˙NhSubGrpG
56 simp-4r φhSubGrpGNhxhi=x˙Nyhj=y˙Nxh
57 simplr φhSubGrpGNhxhi=x˙Nyhj=y˙Nyh
58 eqid +G=+G
59 58 subgcl hSubGrpGxhyhx+Gyh
60 55 56 57 59 syl3anc φhSubGrpGNhxhi=x˙Nyhj=y˙Nx+Gyh
61 sneq z=x+Gyz=x+Gy
62 61 oveq1d z=x+Gyz˙N=x+Gy˙N
63 62 eqeq2d z=x+Gyi+Qj=z˙Ni+Qj=x+Gy˙N
64 63 adantl φhSubGrpGNhxhi=x˙Nyhj=y˙Nz=x+Gyi+Qj=z˙Ni+Qj=x+Gy˙N
65 simpr φhSubGrpGNhxhi=x˙Ni=x˙N
66 23 adantr φhSubGrpGNhxhi=x˙NxG~QGN=x˙N
67 65 66 eqtr4d φhSubGrpGNhxhi=x˙Ni=xG~QGN
68 67 ad2antrr φhSubGrpGNhxhi=x˙Nyhj=y˙Ni=xG~QGN
69 simpr φhSubGrpGNhxhi=x˙Nyhj=y˙Nj=y˙N
70 10 ad4antr φhSubGrpGNhxhi=x˙NNNrmSGrpG
71 70 ad2antrr φhSubGrpGNhxhi=x˙Nyhj=y˙NNNrmSGrpG
72 71 20 syl φhSubGrpGNhxhi=x˙Nyhj=y˙NNSubGrpG
73 55 14 syl φhSubGrpGNhxhi=x˙Nyhj=y˙NhB
74 73 57 sseldd φhSubGrpGNhxhi=x˙Nyhj=y˙NyB
75 1 7 72 74 quslsm φhSubGrpGNhxhi=x˙Nyhj=y˙NyG~QGN=y˙N
76 69 75 eqtr4d φhSubGrpGNhxhi=x˙Nyhj=y˙Nj=yG~QGN
77 68 76 oveq12d φhSubGrpGNhxhi=x˙Nyhj=y˙Ni+Qj=xG~QGN+QyG~QGN
78 16 adantr φhSubGrpGNhxhi=x˙NxB
79 78 ad2antrr φhSubGrpGNhxhi=x˙Nyhj=y˙NxB
80 eqid +Q=+Q
81 6 1 58 80 qusadd NNrmSGrpGxByBxG~QGN+QyG~QGN=x+GyG~QGN
82 71 79 74 81 syl3anc φhSubGrpGNhxhi=x˙Nyhj=y˙NxG~QGN+QyG~QGN=x+GyG~QGN
83 73 60 sseldd φhSubGrpGNhxhi=x˙Nyhj=y˙Nx+GyB
84 1 7 72 83 quslsm φhSubGrpGNhxhi=x˙Nyhj=y˙Nx+GyG~QGN=x+Gy˙N
85 77 82 84 3eqtrd φhSubGrpGNhxhi=x˙Nyhj=y˙Ni+Qj=x+Gy˙N
86 60 64 85 rspcedvd φhSubGrpGNhxhi=x˙Nyhj=y˙Nzhi+Qj=z˙N
87 ovexd φhSubGrpGNhxhi=x˙Nyhj=y˙Ni+QjV
88 53 86 87 elrnmptd φhSubGrpGNhxhi=x˙Nyhj=y˙Ni+Qjranxhx˙N
89 88 adantllr φhSubGrpGNhxhi=x˙Njranxhx˙Nyhj=y˙Ni+Qjranxhx˙N
90 sneq x=yx=y
91 90 oveq1d x=yx˙N=y˙N
92 91 cbvmptv xhx˙N=yhy˙N
93 ovex y˙NV
94 92 93 elrnmpti jranxhx˙Nyhj=y˙N
95 94 biimpi jranxhx˙Nyhj=y˙N
96 95 adantl φhSubGrpGNhxhi=x˙Njranxhx˙Nyhj=y˙N
97 89 96 r19.29a φhSubGrpGNhxhi=x˙Njranxhx˙Ni+Qjranxhx˙N
98 97 ralrimiva φhSubGrpGNhxhi=x˙Njranxhx˙Ni+Qjranxhx˙N
99 eqid invgG=invgG
100 99 subginvcl hSubGrpGxhinvgGxh
101 100 ad5ant24 φhSubGrpGNhxhi=x˙NinvgGxh
102 simpr φhSubGrpGNhxhi=x˙Ny=invgGxy=invgGx
103 102 sneqd φhSubGrpGNhxhi=x˙Ny=invgGxy=invgGx
104 103 oveq1d φhSubGrpGNhxhi=x˙Ny=invgGxy˙N=invgGx˙N
105 15 adantr φhSubGrpGNhxhhB
106 100 ad4ant24 φhSubGrpGNhxhinvgGxh
107 105 106 sseldd φhSubGrpGNhxhinvgGxB
108 1 7 22 107 quslsm φhSubGrpGNhxhinvgGxG~QGN=invgGx˙N
109 108 ad2antrr φhSubGrpGNhxhi=x˙Ny=invgGxinvgGxG~QGN=invgGx˙N
110 104 109 eqtr4d φhSubGrpGNhxhi=x˙Ny=invgGxy˙N=invgGxG~QGN
111 110 eqeq2d φhSubGrpGNhxhi=x˙Ny=invgGxinvgQi=y˙NinvgQi=invgGxG~QGN
112 67 fveq2d φhSubGrpGNhxhi=x˙NinvgQi=invgQxG~QGN
113 eqid invgQ=invgQ
114 6 1 99 113 qusinv NNrmSGrpGxBinvgQxG~QGN=invgGxG~QGN
115 70 78 114 syl2anc φhSubGrpGNhxhi=x˙NinvgQxG~QGN=invgGxG~QGN
116 112 115 eqtrd φhSubGrpGNhxhi=x˙NinvgQi=invgGxG~QGN
117 101 111 116 rspcedvd φhSubGrpGNhxhi=x˙NyhinvgQi=y˙N
118 fvexd φhSubGrpGNhxhi=x˙NinvgQiV
119 92 117 118 elrnmptd φhSubGrpGNhxhi=x˙NinvgQiranxhx˙N
120 98 119 jca φhSubGrpGNhxhi=x˙Njranxhx˙Ni+Qjranxhx˙NinvgQiranxhx˙N
121 120 adantllr φhSubGrpGNhiranxhx˙Nxhi=x˙Njranxhx˙Ni+Qjranxhx˙NinvgQiranxhx˙N
122 ovex x˙NV
123 33 122 elrnmpti iranxhx˙Nxhi=x˙N
124 123 biimpi iranxhx˙Nxhi=x˙N
125 124 adantl φhSubGrpGNhiranxhx˙Nxhi=x˙N
126 46 50 121 125 r19.29af2 φhSubGrpGNhiranxhx˙Njranxhx˙Ni+Qjranxhx˙NinvgQiranxhx˙N
127 126 ralrimiva φhSubGrpGNhiranxhx˙Njranxhx˙Ni+Qjranxhx˙NinvgQiranxhx˙N
128 eqid BaseQ=BaseQ
129 128 80 113 issubg2 QGrpranxhx˙NSubGrpQranxhx˙NBaseQranxhx˙Niranxhx˙Njranxhx˙Ni+Qjranxhx˙NinvgQiranxhx˙N
130 129 biimpar QGrpranxhx˙NBaseQranxhx˙Niranxhx˙Njranxhx˙Ni+Qjranxhx˙NinvgQiranxhx˙Nranxhx˙NSubGrpQ
131 13 35 42 127 130 syl13anc φhSubGrpGNhranxhx˙NSubGrpQ
132 131 3 eleqtrrdi φhSubGrpGNhranxhx˙NT