Metamath Proof Explorer

Theorem nsgmgclem

Description: Lemma for nsgmgc . (Contributed by Thierry Arnoux, 27-Jul-2024)

Ref Expression
Hypotheses nsgmgclem.b ⊢B=BaseG
nsgmgclem.q ⊢Q=G/𝑠G~QGN
nsgmgclem.p ⊢⊕˙=LSSum⁡G
nsgmgclem.n ⊢φ→N∈NrmSGrp⁡G
nsgmgclem.f ⊢φ→F∈SubGrp⁡Q
Assertion nsgmgclem ⊢φ→a∈B|a⊕˙N∈F∈SubGrp⁡G

Proof

Step Hyp Ref Expression
1 nsgmgclem.b ⊢B=BaseG
2 nsgmgclem.q ⊢Q=G/𝑠G~QGN
3 nsgmgclem.p ⊢⊕˙=LSSum⁡G
4 nsgmgclem.n ⊢φ→N∈NrmSGrp⁡G
5 nsgmgclem.f ⊢φ→F∈SubGrp⁡Q
6 eqidd ⊢φ→G↾𝑠a∈B|a⊕˙N∈F=G↾𝑠a∈B|a⊕˙N∈F
7 eqidd ⊢φ→0G=0G
8 eqidd ⊢φ→+G=+G
9 ssrab2 ⊢a∈B|a⊕˙N∈F⊆B
10 9 a1i ⊢φ→a∈B|a⊕˙N∈F⊆B
11 10 1 sseqtrdi ⊢φ→a∈B|a⊕˙N∈F⊆BaseG
12 sneq ⊢a=0G→a=0G
13 12 oveq1d ⊢a=0G→a⊕˙N=0G⊕˙N
14 13 eleq1d ⊢a=0G→a⊕˙N∈F↔0G⊕˙N∈F
15 nsgsubg ⊢N∈NrmSGrp⁡G→N∈SubGrp⁡G
16 4 15 syl ⊢φ→N∈SubGrp⁡G
17 subgrcl ⊢N∈SubGrp⁡G→G∈Grp
18 16 17 syl ⊢φ→G∈Grp
19 eqid ⊢0G=0G
20 1 19 grpidcl ⊢G∈Grp→0G∈B
21 18 20 syl ⊢φ→0G∈B
22 19 3 lsm02 ⊢N∈SubGrp⁡G→0G⊕˙N=N
23 16 22 syl ⊢φ→0G⊕˙N=N
24 2 nsgqus0 ⊢N∈NrmSGrp⁡G∧F∈SubGrp⁡Q→N∈F
25 4 5 24 syl2anc ⊢φ→N∈F
26 23 25 eqeltrd ⊢φ→0G⊕˙N∈F
27 14 21 26 elrabd ⊢φ→0G∈a∈B|a⊕˙N∈F
28 sneq ⊢a=x+Gy→a=x+Gy
29 28 oveq1d ⊢a=x+Gy→a⊕˙N=x+Gy⊕˙N
30 29 eleq1d ⊢a=x+Gy→a⊕˙N∈F↔x+Gy⊕˙N∈F
31 18 ad2antrr ⊢φ∧x∈a∈B|a⊕˙N∈F∧y∈a∈B|a⊕˙N∈F→G∈Grp
32 elrabi ⊢x∈a∈B|a⊕˙N∈F→x∈B
33 32 ad2antlr ⊢φ∧x∈a∈B|a⊕˙N∈F∧y∈a∈B|a⊕˙N∈F→x∈B
34 elrabi ⊢y∈a∈B|a⊕˙N∈F→y∈B
35 34 adantl ⊢φ∧x∈a∈B|a⊕˙N∈F∧y∈a∈B|a⊕˙N∈F→y∈B
36 eqid ⊢+G=+G
37 1 36 grpcl ⊢G∈Grp∧x∈B∧y∈B→x+Gy∈B
38 31 33 35 37 syl3anc ⊢φ∧x∈a∈B|a⊕˙N∈F∧y∈a∈B|a⊕˙N∈F→x+Gy∈B
39 16 ad2antrr ⊢φ∧x∈a∈B|a⊕˙N∈F∧y∈a∈B|a⊕˙N∈F→N∈SubGrp⁡G
40 1 3 39 38 quslsm ⊢φ∧x∈a∈B|a⊕˙N∈F∧y∈a∈B|a⊕˙N∈F→x+GyG~QGN=x+Gy⊕˙N
41 4 ad2antrr ⊢φ∧x∈a∈B|a⊕˙N∈F∧y∈a∈B|a⊕˙N∈F→N∈NrmSGrp⁡G
42 eqid ⊢+Q=+Q
43 2 1 36 42 qusadd ⊢N∈NrmSGrp⁡G∧x∈B∧y∈B→xG~QGN+QyG~QGN=x+GyG~QGN
44 41 33 35 43 syl3anc ⊢φ∧x∈a∈B|a⊕˙N∈F∧y∈a∈B|a⊕˙N∈F→xG~QGN+QyG~QGN=x+GyG~QGN
45 5 ad2antrr ⊢φ∧x∈a∈B|a⊕˙N∈F∧y∈a∈B|a⊕˙N∈F→F∈SubGrp⁡Q
46 1 3 39 33 quslsm ⊢φ∧x∈a∈B|a⊕˙N∈F∧y∈a∈B|a⊕˙N∈F→xG~QGN=x⊕˙N
47 sneq ⊢a=x→a=x
48 47 oveq1d ⊢a=x→a⊕˙N=x⊕˙N
49 48 eleq1d ⊢a=x→a⊕˙N∈F↔x⊕˙N∈F
50 49 elrab ⊢x∈a∈B|a⊕˙N∈F↔x∈B∧x⊕˙N∈F
51 50 simprbi ⊢x∈a∈B|a⊕˙N∈F→x⊕˙N∈F
52 51 ad2antlr ⊢φ∧x∈a∈B|a⊕˙N∈F∧y∈a∈B|a⊕˙N∈F→x⊕˙N∈F
53 46 52 eqeltrd ⊢φ∧x∈a∈B|a⊕˙N∈F∧y∈a∈B|a⊕˙N∈F→xG~QGN∈F
54 1 3 39 35 quslsm ⊢φ∧x∈a∈B|a⊕˙N∈F∧y∈a∈B|a⊕˙N∈F→yG~QGN=y⊕˙N
55 sneq ⊢a=y→a=y
56 55 oveq1d ⊢a=y→a⊕˙N=y⊕˙N
57 56 eleq1d ⊢a=y→a⊕˙N∈F↔y⊕˙N∈F
58 57 elrab ⊢y∈a∈B|a⊕˙N∈F↔y∈B∧y⊕˙N∈F
59 58 simprbi ⊢y∈a∈B|a⊕˙N∈F→y⊕˙N∈F
60 59 adantl ⊢φ∧x∈a∈B|a⊕˙N∈F∧y∈a∈B|a⊕˙N∈F→y⊕˙N∈F
61 54 60 eqeltrd ⊢φ∧x∈a∈B|a⊕˙N∈F∧y∈a∈B|a⊕˙N∈F→yG~QGN∈F
62 42 subgcl ⊢F∈SubGrp⁡Q∧xG~QGN∈F∧yG~QGN∈F→xG~QGN+QyG~QGN∈F
63 45 53 61 62 syl3anc ⊢φ∧x∈a∈B|a⊕˙N∈F∧y∈a∈B|a⊕˙N∈F→xG~QGN+QyG~QGN∈F
64 44 63 eqeltrrd ⊢φ∧x∈a∈B|a⊕˙N∈F∧y∈a∈B|a⊕˙N∈F→x+GyG~QGN∈F
65 40 64 eqeltrrd ⊢φ∧x∈a∈B|a⊕˙N∈F∧y∈a∈B|a⊕˙N∈F→x+Gy⊕˙N∈F
66 30 38 65 elrabd ⊢φ∧x∈a∈B|a⊕˙N∈F∧y∈a∈B|a⊕˙N∈F→x+Gy∈a∈B|a⊕˙N∈F
67 66 3impa ⊢φ∧x∈a∈B|a⊕˙N∈F∧y∈a∈B|a⊕˙N∈F→x+Gy∈a∈B|a⊕˙N∈F
68 sneq ⊢a=invg⁡G⁡x→a=invg⁡G⁡x
69 68 oveq1d ⊢a=invg⁡G⁡x→a⊕˙N=invg⁡G⁡x⊕˙N
70 69 eleq1d ⊢a=invg⁡G⁡x→a⊕˙N∈F↔invg⁡G⁡x⊕˙N∈F
71 eqid ⊢invg⁡G=invg⁡G
72 1 71 grpinvcl ⊢G∈Grp∧x∈B→invg⁡G⁡x∈B
73 18 72 sylan ⊢φ∧x∈B→invg⁡G⁡x∈B
74 73 adantr ⊢φ∧x∈B∧x⊕˙N∈F→invg⁡G⁡x∈B
75 eqid ⊢invg⁡Q=invg⁡Q
76 2 1 71 75 qusinv ⊢N∈NrmSGrp⁡G∧x∈B→invg⁡Q⁡xG~QGN=invg⁡G⁡xG~QGN
77 4 76 sylan ⊢φ∧x∈B→invg⁡Q⁡xG~QGN=invg⁡G⁡xG~QGN
78 16 adantr ⊢φ∧x∈B→N∈SubGrp⁡G
79 simpr ⊢φ∧x∈B→x∈B
80 1 3 78 79 quslsm ⊢φ∧x∈B→xG~QGN=x⊕˙N
81 80 fveq2d ⊢φ∧x∈B→invg⁡Q⁡xG~QGN=invg⁡Q⁡x⊕˙N
82 1 3 78 73 quslsm ⊢φ∧x∈B→invg⁡G⁡xG~QGN=invg⁡G⁡x⊕˙N
83 77 81 82 3eqtr3d ⊢φ∧x∈B→invg⁡Q⁡x⊕˙N=invg⁡G⁡x⊕˙N
84 83 adantr ⊢φ∧x∈B∧x⊕˙N∈F→invg⁡Q⁡x⊕˙N=invg⁡G⁡x⊕˙N
85 5 ad2antrr ⊢φ∧x∈B∧x⊕˙N∈F→F∈SubGrp⁡Q
86 simpr ⊢φ∧x∈B∧x⊕˙N∈F→x⊕˙N∈F
87 75 subginvcl ⊢F∈SubGrp⁡Q∧x⊕˙N∈F→invg⁡Q⁡x⊕˙N∈F
88 85 86 87 syl2anc ⊢φ∧x∈B∧x⊕˙N∈F→invg⁡Q⁡x⊕˙N∈F
89 84 88 eqeltrrd ⊢φ∧x∈B∧x⊕˙N∈F→invg⁡G⁡x⊕˙N∈F
90 70 74 89 elrabd ⊢φ∧x∈B∧x⊕˙N∈F→invg⁡G⁡x∈a∈B|a⊕˙N∈F
91 90 anasss ⊢φ∧x∈B∧x⊕˙N∈F→invg⁡G⁡x∈a∈B|a⊕˙N∈F
92 50 91 sylan2b ⊢φ∧x∈a∈B|a⊕˙N∈F→invg⁡G⁡x∈a∈B|a⊕˙N∈F
93 6 7 8 11 27 67 92 18 issubgrpd2 ⊢φ→a∈B|a⊕˙N∈F∈SubGrp⁡G