Metamath Proof Explorer

Theorem nsgmgclem

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

Ref Expression
Hypotheses nsgmgclem.b ⊢ B = Base G
nsgmgclem.q ⊢ Q = G / 𝑠 G ~ QG N
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 = Base G
2 nsgmgclem.q ⊢ Q = G / 𝑠 G ~ QG N
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 ⊢ φ → 0 G = 0 G
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 ⊆ Base G
12 sneq ⊢ a = 0 G → a = 0 G
13 12 oveq1d ⊢ a = 0 G → a ⊕ ˙ N = 0 G ⊕ ˙ N
14 13 eleq1d ⊢ a = 0 G → a ⊕ ˙ N ∈ F ↔ 0 G ⊕ ˙ 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 ⊢ 0 G = 0 G
20 1 19 grpidcl ⊢ G ∈ Grp → 0 G ∈ B
21 18 20 syl ⊢ φ → 0 G ∈ B
22 19 3 lsm02 ⊢ N ∈ SubGrp ⁡ G → 0 G ⊕ ˙ N = N
23 16 22 syl ⊢ φ → 0 G ⊕ ˙ N = N
24 2 nsgqus0 ⊢ N ∈ NrmSGrp ⁡ G ∧ F ∈ SubGrp ⁡ Q → N ∈ F
25 4 5 24 syl2anc ⊢ φ → N ∈ F
26 23 25 eqeltrd ⊢ φ → 0 G ⊕ ˙ N ∈ F
27 14 21 26 elrabd ⊢ φ → 0 G ∈ a ∈ B | a ⊕ ˙ N ∈ F
28 sneq ⊢ a = x + G y → a = x + G y
29 28 oveq1d ⊢ a = x + G y → a ⊕ ˙ N = x + G y ⊕ ˙ N
30 29 eleq1d ⊢ a = x + G y → a ⊕ ˙ N ∈ F ↔ x + G y ⊕ ˙ 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 + G y ∈ B
38 31 33 35 37 syl3anc ⊢ φ ∧ x ∈ a ∈ B | a ⊕ ˙ N ∈ F ∧ y ∈ a ∈ B | a ⊕ ˙ N ∈ F → x + G y ∈ 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 + G y G ~ QG N = x + G y ⊕ ˙ 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 → x G ~ QG N + Q y G ~ QG N = x + G y G ~ QG N
44 41 33 35 43 syl3anc ⊢ φ ∧ x ∈ a ∈ B | a ⊕ ˙ N ∈ F ∧ y ∈ a ∈ B | a ⊕ ˙ N ∈ F → x G ~ QG N + Q y G ~ QG N = x + G y G ~ QG N
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 → x G ~ QG N = 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 → x G ~ QG N ∈ F
54 1 3 39 35 quslsm ⊢ φ ∧ x ∈ a ∈ B | a ⊕ ˙ N ∈ F ∧ y ∈ a ∈ B | a ⊕ ˙ N ∈ F → y G ~ QG N = 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 → y G ~ QG N ∈ F
62 42 subgcl ⊢ F ∈ SubGrp ⁡ Q ∧ x G ~ QG N ∈ F ∧ y G ~ QG N ∈ F → x G ~ QG N + Q y G ~ QG N ∈ F
63 45 53 61 62 syl3anc ⊢ φ ∧ x ∈ a ∈ B | a ⊕ ˙ N ∈ F ∧ y ∈ a ∈ B | a ⊕ ˙ N ∈ F → x G ~ QG N + Q y G ~ QG N ∈ F
64 44 63 eqeltrrd ⊢ φ ∧ x ∈ a ∈ B | a ⊕ ˙ N ∈ F ∧ y ∈ a ∈ B | a ⊕ ˙ N ∈ F → x + G y G ~ QG N ∈ F
65 40 64 eqeltrrd ⊢ φ ∧ x ∈ a ∈ B | a ⊕ ˙ N ∈ F ∧ y ∈ a ∈ B | a ⊕ ˙ N ∈ F → x + G y ⊕ ˙ N ∈ F
66 30 38 65 elrabd ⊢ φ ∧ x ∈ a ∈ B | a ⊕ ˙ N ∈ F ∧ y ∈ a ∈ B | a ⊕ ˙ N ∈ F → x + G y ∈ a ∈ B | a ⊕ ˙ N ∈ F
67 66 3impa ⊢ φ ∧ x ∈ a ∈ B | a ⊕ ˙ N ∈ F ∧ y ∈ a ∈ B | a ⊕ ˙ N ∈ F → x + G y ∈ a ∈ B | a ⊕ ˙ N ∈ F
68 sneq ⊢ a = inv g ⁡ G ⁡ x → a = inv g ⁡ G ⁡ x
69 68 oveq1d ⊢ a = inv g ⁡ G ⁡ x → a ⊕ ˙ N = inv g ⁡ G ⁡ x ⊕ ˙ N
70 69 eleq1d ⊢ a = inv g ⁡ G ⁡ x → a ⊕ ˙ N ∈ F ↔ inv g ⁡ G ⁡ x ⊕ ˙ N ∈ F
71 eqid ⊢ inv g ⁡ G = inv g ⁡ G
72 1 71 grpinvcl ⊢ G ∈ Grp ∧ x ∈ B → inv g ⁡ G ⁡ x ∈ B
73 18 72 sylan ⊢ φ ∧ x ∈ B → inv g ⁡ G ⁡ x ∈ B
74 73 adantr ⊢ φ ∧ x ∈ B ∧ x ⊕ ˙ N ∈ F → inv g ⁡ G ⁡ x ∈ B
75 eqid ⊢ inv g ⁡ Q = inv g ⁡ Q
76 2 1 71 75 qusinv ⊢ N ∈ NrmSGrp ⁡ G ∧ x ∈ B → inv g ⁡ Q ⁡ x G ~ QG N = inv g ⁡ G ⁡ x G ~ QG N
77 4 76 sylan ⊢ φ ∧ x ∈ B → inv g ⁡ Q ⁡ x G ~ QG N = inv g ⁡ G ⁡ x G ~ QG N
78 16 adantr ⊢ φ ∧ x ∈ B → N ∈ SubGrp ⁡ G
79 simpr ⊢ φ ∧ x ∈ B → x ∈ B
80 1 3 78 79 quslsm ⊢ φ ∧ x ∈ B → x G ~ QG N = x ⊕ ˙ N
81 80 fveq2d ⊢ φ ∧ x ∈ B → inv g ⁡ Q ⁡ x G ~ QG N = inv g ⁡ Q ⁡ x ⊕ ˙ N
82 1 3 78 73 quslsm ⊢ φ ∧ x ∈ B → inv g ⁡ G ⁡ x G ~ QG N = inv g ⁡ G ⁡ x ⊕ ˙ N
83 77 81 82 3eqtr3d ⊢ φ ∧ x ∈ B → inv g ⁡ Q ⁡ x ⊕ ˙ N = inv g ⁡ G ⁡ x ⊕ ˙ N
84 83 adantr ⊢ φ ∧ x ∈ B ∧ x ⊕ ˙ N ∈ F → inv g ⁡ Q ⁡ x ⊕ ˙ N = inv g ⁡ 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 → inv g ⁡ Q ⁡ x ⊕ ˙ N ∈ F
88 85 86 87 syl2anc ⊢ φ ∧ x ∈ B ∧ x ⊕ ˙ N ∈ F → inv g ⁡ Q ⁡ x ⊕ ˙ N ∈ F
89 84 88 eqeltrrd ⊢ φ ∧ x ∈ B ∧ x ⊕ ˙ N ∈ F → inv g ⁡ G ⁡ x ⊕ ˙ N ∈ F
90 70 74 89 elrabd ⊢ φ ∧ x ∈ B ∧ x ⊕ ˙ N ∈ F → inv g ⁡ G ⁡ x ∈ a ∈ B | a ⊕ ˙ N ∈ F
91 90 anasss ⊢ φ ∧ x ∈ B ∧ x ⊕ ˙ N ∈ F → inv g ⁡ G ⁡ x ∈ a ∈ B | a ⊕ ˙ N ∈ F
92 50 91 sylan2b ⊢ φ ∧ x ∈ a ∈ B | a ⊕ ˙ N ∈ F → inv g ⁡ G ⁡ x ∈ a ∈ B | a ⊕ ˙ N ∈ F
93 6 7 8 11 27 67 92 18 issubgrpd2 ⊢ φ → a ∈ B | a ⊕ ˙ N ∈ F ∈ SubGrp ⁡ G