Metamath Proof Explorer

Theorem nsgmgclem

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

Ref Expression
Hypotheses nsgmgclem.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
nsgmgclem.q ⊢ 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝑁 ) )
nsgmgclem.p ⊢ ⊕ = ( LSSum ‘ 𝐺 )
nsgmgclem.n ⊢ ( 𝜑 → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
nsgmgclem.f ⊢ ( 𝜑 → 𝐹 ∈ ( SubGrp ‘ 𝑄 ) )
Assertion nsgmgclem ( 𝜑 → { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ∈ ( SubGrp ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 nsgmgclem.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 nsgmgclem.q ⊢ 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝑁 ) )
3 nsgmgclem.p ⊢ ⊕ = ( LSSum ‘ 𝐺 )
4 nsgmgclem.n ⊢ ( 𝜑 → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
5 nsgmgclem.f ⊢ ( 𝜑 → 𝐹 ∈ ( SubGrp ‘ 𝑄 ) )
6 eqidd ⊢ ( 𝜑 → ( 𝐺 ↾s { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) = ( 𝐺 ↾s { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) )
7 eqidd ⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 ) )
8 eqidd ⊢ ( 𝜑 → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 ) )
9 ssrab2 ⊢ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ⊆ 𝐵
10 9 a1i ⊢ ( 𝜑 → { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ⊆ 𝐵 )
11 10 1 sseqtrdi ⊢ ( 𝜑 → { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ⊆ ( Base ‘ 𝐺 ) )
12 sneq ⊢ ( 𝑎 = ( 0g ‘ 𝐺 ) → { 𝑎 } = { ( 0g ‘ 𝐺 ) } )
13 12 oveq1d ⊢ ( 𝑎 = ( 0g ‘ 𝐺 ) → ( { 𝑎 } ⊕ 𝑁 ) = ( { ( 0g ‘ 𝐺 ) } ⊕ 𝑁 ) )
14 13 eleq1d ⊢ ( 𝑎 = ( 0g ‘ 𝐺 ) → ( ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 ↔ ( { ( 0g ‘ 𝐺 ) } ⊕ 𝑁 ) ∈ 𝐹 ) )
15 nsgsubg ⊢ ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
16 4 15 syl ⊢ ( 𝜑 → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
17 subgrcl ⊢ ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
18 16 17 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
19 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
20 1 19 grpidcl ⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ 𝐵 )
21 18 20 syl ⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) ∈ 𝐵 )
22 19 3 lsm02 ⊢ ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → ( { ( 0g ‘ 𝐺 ) } ⊕ 𝑁 ) = 𝑁 )
23 16 22 syl ⊢ ( 𝜑 → ( { ( 0g ‘ 𝐺 ) } ⊕ 𝑁 ) = 𝑁 )
24 2 nsgqus0 ⊢ ( ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝐹 ∈ ( SubGrp ‘ 𝑄 ) ) → 𝑁 ∈ 𝐹 )
25 4 5 24 syl2anc ⊢ ( 𝜑 → 𝑁 ∈ 𝐹 )
26 23 25 eqeltrd ⊢ ( 𝜑 → ( { ( 0g ‘ 𝐺 ) } ⊕ 𝑁 ) ∈ 𝐹 )
27 14 21 26 elrabd ⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } )
28 sneq ⊢ ( 𝑎 = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) → { 𝑎 } = { ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) } )
29 28 oveq1d ⊢ ( 𝑎 = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) → ( { 𝑎 } ⊕ 𝑁 ) = ( { ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) } ⊕ 𝑁 ) )
30 29 eleq1d ⊢ ( 𝑎 = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) → ( ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 ↔ ( { ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) } ⊕ 𝑁 ) ∈ 𝐹 ) )
31 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) ∧ 𝑦 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) → 𝐺 ∈ Grp )
32 elrabi ⊢ ( 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } → 𝑥 ∈ 𝐵 )
33 32 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) ∧ 𝑦 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) → 𝑥 ∈ 𝐵 )
34 elrabi ⊢ ( 𝑦 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } → 𝑦 ∈ 𝐵 )
35 34 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) ∧ 𝑦 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) → 𝑦 ∈ 𝐵 )
36 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
37 1 36 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐵 )
38 31 33 35 37 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) ∧ 𝑦 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐵 )
39 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) ∧ 𝑦 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
40 1 3 39 38 quslsm ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) ∧ 𝑦 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) → [ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ] ( 𝐺 ~QG 𝑁 ) = ( { ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) } ⊕ 𝑁 ) )
41 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) ∧ 𝑦 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
42 eqid ⊢ ( +g ‘ 𝑄 ) = ( +g ‘ 𝑄 )
43 2 1 36 42 qusadd ⊢ ( ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ( +g ‘ 𝑄 ) [ 𝑦 ] ( 𝐺 ~QG 𝑁 ) ) = [ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ] ( 𝐺 ~QG 𝑁 ) )
44 41 33 35 43 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) ∧ 𝑦 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) → ( [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ( +g ‘ 𝑄 ) [ 𝑦 ] ( 𝐺 ~QG 𝑁 ) ) = [ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ] ( 𝐺 ~QG 𝑁 ) )
45 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) ∧ 𝑦 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) → 𝐹 ∈ ( SubGrp ‘ 𝑄 ) )
46 1 3 39 33 quslsm ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) ∧ 𝑦 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) → [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) )
47 sneq ⊢ ( 𝑎 = 𝑥 → { 𝑎 } = { 𝑥 } )
48 47 oveq1d ⊢ ( 𝑎 = 𝑥 → ( { 𝑎 } ⊕ 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) )
49 48 eleq1d ⊢ ( 𝑎 = 𝑥 → ( ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 ↔ ( { 𝑥 } ⊕ 𝑁 ) ∈ 𝐹 ) )
50 49 elrab ⊢ ( 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ↔ ( 𝑥 ∈ 𝐵 ∧ ( { 𝑥 } ⊕ 𝑁 ) ∈ 𝐹 ) )
51 50 simprbi ⊢ ( 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } → ( { 𝑥 } ⊕ 𝑁 ) ∈ 𝐹 )
52 51 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) ∧ 𝑦 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) → ( { 𝑥 } ⊕ 𝑁 ) ∈ 𝐹 )
53 46 52 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) ∧ 𝑦 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) → [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ∈ 𝐹 )
54 1 3 39 35 quslsm ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) ∧ 𝑦 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) → [ 𝑦 ] ( 𝐺 ~QG 𝑁 ) = ( { 𝑦 } ⊕ 𝑁 ) )
55 sneq ⊢ ( 𝑎 = 𝑦 → { 𝑎 } = { 𝑦 } )
56 55 oveq1d ⊢ ( 𝑎 = 𝑦 → ( { 𝑎 } ⊕ 𝑁 ) = ( { 𝑦 } ⊕ 𝑁 ) )
57 56 eleq1d ⊢ ( 𝑎 = 𝑦 → ( ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 ↔ ( { 𝑦 } ⊕ 𝑁 ) ∈ 𝐹 ) )
58 57 elrab ⊢ ( 𝑦 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ↔ ( 𝑦 ∈ 𝐵 ∧ ( { 𝑦 } ⊕ 𝑁 ) ∈ 𝐹 ) )
59 58 simprbi ⊢ ( 𝑦 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } → ( { 𝑦 } ⊕ 𝑁 ) ∈ 𝐹 )
60 59 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) ∧ 𝑦 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) → ( { 𝑦 } ⊕ 𝑁 ) ∈ 𝐹 )
61 54 60 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) ∧ 𝑦 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) → [ 𝑦 ] ( 𝐺 ~QG 𝑁 ) ∈ 𝐹 )
62 42 subgcl ⊢ ( ( 𝐹 ∈ ( SubGrp ‘ 𝑄 ) ∧ [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ∈ 𝐹 ∧ [ 𝑦 ] ( 𝐺 ~QG 𝑁 ) ∈ 𝐹 ) → ( [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ( +g ‘ 𝑄 ) [ 𝑦 ] ( 𝐺 ~QG 𝑁 ) ) ∈ 𝐹 )
63 45 53 61 62 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) ∧ 𝑦 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) → ( [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ( +g ‘ 𝑄 ) [ 𝑦 ] ( 𝐺 ~QG 𝑁 ) ) ∈ 𝐹 )
64 44 63 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) ∧ 𝑦 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) → [ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ] ( 𝐺 ~QG 𝑁 ) ∈ 𝐹 )
65 40 64 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) ∧ 𝑦 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) → ( { ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) } ⊕ 𝑁 ) ∈ 𝐹 )
66 30 38 65 elrabd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) ∧ 𝑦 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } )
67 66 3impa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ∧ 𝑦 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } )
68 sneq ⊢ ( 𝑎 = ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) → { 𝑎 } = { ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) } )
69 68 oveq1d ⊢ ( 𝑎 = ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) → ( { 𝑎 } ⊕ 𝑁 ) = ( { ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) } ⊕ 𝑁 ) )
70 69 eleq1d ⊢ ( 𝑎 = ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) → ( ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 ↔ ( { ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) } ⊕ 𝑁 ) ∈ 𝐹 ) )
71 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
72 1 71 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐵 )
73 18 72 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐵 )
74 73 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( { 𝑥 } ⊕ 𝑁 ) ∈ 𝐹 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐵 )
75 eqid ⊢ ( invg ‘ 𝑄 ) = ( invg ‘ 𝑄 )
76 2 1 71 75 qusinv ⊢ ( ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( invg ‘ 𝑄 ) ‘ [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) = [ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ] ( 𝐺 ~QG 𝑁 ) )
77 4 76 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( invg ‘ 𝑄 ) ‘ [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) = [ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ] ( 𝐺 ~QG 𝑁 ) )
78 16 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
79 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
80 1 3 78 79 quslsm ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) )
81 80 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( invg ‘ 𝑄 ) ‘ [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) = ( ( invg ‘ 𝑄 ) ‘ ( { 𝑥 } ⊕ 𝑁 ) ) )
82 1 3 78 73 quslsm ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → [ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ] ( 𝐺 ~QG 𝑁 ) = ( { ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) } ⊕ 𝑁 ) )
83 77 81 82 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( invg ‘ 𝑄 ) ‘ ( { 𝑥 } ⊕ 𝑁 ) ) = ( { ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) } ⊕ 𝑁 ) )
84 83 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( { 𝑥 } ⊕ 𝑁 ) ∈ 𝐹 ) → ( ( invg ‘ 𝑄 ) ‘ ( { 𝑥 } ⊕ 𝑁 ) ) = ( { ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) } ⊕ 𝑁 ) )
85 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( { 𝑥 } ⊕ 𝑁 ) ∈ 𝐹 ) → 𝐹 ∈ ( SubGrp ‘ 𝑄 ) )
86 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( { 𝑥 } ⊕ 𝑁 ) ∈ 𝐹 ) → ( { 𝑥 } ⊕ 𝑁 ) ∈ 𝐹 )
87 75 subginvcl ⊢ ( ( 𝐹 ∈ ( SubGrp ‘ 𝑄 ) ∧ ( { 𝑥 } ⊕ 𝑁 ) ∈ 𝐹 ) → ( ( invg ‘ 𝑄 ) ‘ ( { 𝑥 } ⊕ 𝑁 ) ) ∈ 𝐹 )
88 85 86 87 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( { 𝑥 } ⊕ 𝑁 ) ∈ 𝐹 ) → ( ( invg ‘ 𝑄 ) ‘ ( { 𝑥 } ⊕ 𝑁 ) ) ∈ 𝐹 )
89 84 88 eqeltrrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( { 𝑥 } ⊕ 𝑁 ) ∈ 𝐹 ) → ( { ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) } ⊕ 𝑁 ) ∈ 𝐹 )
90 70 74 89 elrabd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( { 𝑥 } ⊕ 𝑁 ) ∈ 𝐹 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } )
91 90 anasss ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ ( { 𝑥 } ⊕ 𝑁 ) ∈ 𝐹 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } )
92 50 91 sylan2b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } )
93 6 7 8 11 27 67 92 18 issubgrpd2 ⊢ ( 𝜑 → { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝐹 } ∈ ( SubGrp ‘ 𝐺 ) )