Metamath Proof Explorer

Theorem nsgqusf1olem3

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

Ref Expression
Hypotheses nsgqusf1o.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
nsgqusf1o.s ⊢ 𝑆 = { ℎ ∈ ( SubGrp ‘ 𝐺 ) ∣ 𝑁 ⊆ ℎ }
nsgqusf1o.t ⊢ 𝑇 = ( SubGrp ‘ 𝑄 )
nsgqusf1o.1 ⊢ ≤ = ( le ‘ ( toInc ‘ 𝑆 ) )
nsgqusf1o.2 ⊢ ≲ = ( le ‘ ( toInc ‘ 𝑇 ) )
nsgqusf1o.q ⊢ 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝑁 ) )
nsgqusf1o.p ⊢ ⊕ = ( LSSum ‘ 𝐺 )
nsgqusf1o.e ⊢ 𝐸 = ( ℎ ∈ 𝑆 ↦ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
nsgqusf1o.f ⊢ 𝐹 = ( 𝑓 ∈ 𝑇 ↦ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } )
nsgqusf1o.n ⊢ ( 𝜑 → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
Assertion nsgqusf1olem3 ( 𝜑 → ran 𝐹 = 𝑆 )

Proof

Step Hyp Ref Expression
1 nsgqusf1o.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 nsgqusf1o.s ⊢ 𝑆 = { ℎ ∈ ( SubGrp ‘ 𝐺 ) ∣ 𝑁 ⊆ ℎ }
3 nsgqusf1o.t ⊢ 𝑇 = ( SubGrp ‘ 𝑄 )
4 nsgqusf1o.1 ⊢ ≤ = ( le ‘ ( toInc ‘ 𝑆 ) )
5 nsgqusf1o.2 ⊢ ≲ = ( le ‘ ( toInc ‘ 𝑇 ) )
6 nsgqusf1o.q ⊢ 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝑁 ) )
7 nsgqusf1o.p ⊢ ⊕ = ( LSSum ‘ 𝐺 )
8 nsgqusf1o.e ⊢ 𝐸 = ( ℎ ∈ 𝑆 ↦ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
9 nsgqusf1o.f ⊢ 𝐹 = ( 𝑓 ∈ 𝑇 ↦ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } )
10 nsgqusf1o.n ⊢ ( 𝜑 → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
11 9 elrnmpt ⊢ ( ℎ ∈ V → ( ℎ ∈ ran 𝐹 ↔ ∃ 𝑓 ∈ 𝑇 ℎ = { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ) )
12 11 elv ⊢ ( ℎ ∈ ran 𝐹 ↔ ∃ 𝑓 ∈ 𝑇 ℎ = { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } )
13 2 reqabi ⊢ ( ℎ ∈ 𝑆 ↔ ( ℎ ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ⊆ ℎ ) )
14 1 2 3 4 5 6 7 8 9 10 nsgqusf1olem1 ⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) → ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ∈ 𝑇 )
15 eleq2 ⊢ ( 𝑓 = ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) → ( ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 ↔ ( { 𝑎 } ⊕ 𝑁 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ) )
16 15 rabbidv ⊢ ( 𝑓 = ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) → { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } = { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) } )
17 16 eqeq2d ⊢ ( 𝑓 = ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) → ( ℎ = { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ↔ ℎ = { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) } ) )
18 17 adantl ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑓 = ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ) → ( ℎ = { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ↔ ℎ = { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) } ) )
19 nfv ⊢ Ⅎ 𝑥 ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 )
20 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) )
21 20 nfrn ⊢ Ⅎ 𝑥 ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) )
22 21 nfel2 ⊢ Ⅎ 𝑥 ( { 𝑎 } ⊕ 𝑁 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) )
23 19 22 nfan ⊢ Ⅎ 𝑥 ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( { 𝑎 } ⊕ 𝑁 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
24 nsgsubg ⊢ ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
25 10 24 syl ⊢ ( 𝜑 → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
26 subgrcl ⊢ ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
27 25 26 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
28 27 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 ∈ ℎ ) → 𝐺 ∈ Grp )
29 28 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 ∈ ℎ ) ∧ ( { 𝑎 } ⊕ 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) ) → 𝐺 ∈ Grp )
30 1 subgss ⊢ ( ℎ ∈ ( SubGrp ‘ 𝐺 ) → ℎ ⊆ 𝐵 )
31 30 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) → ℎ ⊆ 𝐵 )
32 31 sselda ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 ∈ ℎ ) → 𝑥 ∈ 𝐵 )
33 32 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 ∈ ℎ ) ∧ ( { 𝑎 } ⊕ 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) ) → 𝑥 ∈ 𝐵 )
34 simplr ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 ∈ ℎ ) → 𝑎 ∈ 𝐵 )
35 34 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 ∈ ℎ ) ∧ ( { 𝑎 } ⊕ 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) ) → 𝑎 ∈ 𝐵 )
36 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
37 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
38 1 36 37 grpasscan1 ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) 𝑎 ) ) = 𝑎 )
39 29 33 35 38 syl3anc ⊢ ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 ∈ ℎ ) ∧ ( { 𝑎 } ⊕ 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) 𝑎 ) ) = 𝑎 )
40 simp-5r ⊢ ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 ∈ ℎ ) ∧ ( { 𝑎 } ⊕ 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) ) → ℎ ∈ ( SubGrp ‘ 𝐺 ) )
41 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 ∈ ℎ ) ∧ ( { 𝑎 } ⊕ 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) ) → 𝑥 ∈ ℎ )
42 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 ∈ ℎ ) ∧ ( { 𝑎 } ⊕ 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) ) → 𝑁 ⊆ ℎ )
43 1 subgss ⊢ ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → 𝑁 ⊆ 𝐵 )
44 25 43 syl ⊢ ( 𝜑 → 𝑁 ⊆ 𝐵 )
45 44 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 ∈ ℎ ) ∧ ( { 𝑎 } ⊕ 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) ) → 𝑁 ⊆ 𝐵 )
46 eqid ⊢ ( 𝐺 ~QG 𝑁 ) = ( 𝐺 ~QG 𝑁 )
47 1 46 eqger ⊢ ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺 ~QG 𝑁 ) Er 𝐵 )
48 25 47 syl ⊢ ( 𝜑 → ( 𝐺 ~QG 𝑁 ) Er 𝐵 )
49 48 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 ∈ ℎ ) → ( 𝐺 ~QG 𝑁 ) Er 𝐵 )
50 49 adantr ⊢ ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 ∈ ℎ ) ∧ ( { 𝑎 } ⊕ 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) ) → ( 𝐺 ~QG 𝑁 ) Er 𝐵 )
51 49 34 erth ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 ∈ ℎ ) → ( 𝑎 ( 𝐺 ~QG 𝑁 ) 𝑥 ↔ [ 𝑎 ] ( 𝐺 ~QG 𝑁 ) = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) )
52 25 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 ∈ ℎ ) → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
53 1 7 52 34 quslsm ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 ∈ ℎ ) → [ 𝑎 ] ( 𝐺 ~QG 𝑁 ) = ( { 𝑎 } ⊕ 𝑁 ) )
54 1 7 52 32 quslsm ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 ∈ ℎ ) → [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) )
55 53 54 eqeq12d ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 ∈ ℎ ) → ( [ 𝑎 ] ( 𝐺 ~QG 𝑁 ) = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ↔ ( { 𝑎 } ⊕ 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) ) )
56 51 55 bitrd ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 ∈ ℎ ) → ( 𝑎 ( 𝐺 ~QG 𝑁 ) 𝑥 ↔ ( { 𝑎 } ⊕ 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) ) )
57 56 biimpar ⊢ ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 ∈ ℎ ) ∧ ( { 𝑎 } ⊕ 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) ) → 𝑎 ( 𝐺 ~QG 𝑁 ) 𝑥 )
58 50 57 ersym ⊢ ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 ∈ ℎ ) ∧ ( { 𝑎 } ⊕ 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) ) → 𝑥 ( 𝐺 ~QG 𝑁 ) 𝑎 )
59 1 37 36 46 eqgval ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ⊆ 𝐵 ) → ( 𝑥 ( 𝐺 ~QG 𝑁 ) 𝑎 ↔ ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) 𝑎 ) ∈ 𝑁 ) ) )
60 59 biimpa ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ⊆ 𝐵 ) ∧ 𝑥 ( 𝐺 ~QG 𝑁 ) 𝑎 ) → ( 𝑥 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) 𝑎 ) ∈ 𝑁 ) )
61 60 simp3d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ⊆ 𝐵 ) ∧ 𝑥 ( 𝐺 ~QG 𝑁 ) 𝑎 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) 𝑎 ) ∈ 𝑁 )
62 29 45 58 61 syl21anc ⊢ ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 ∈ ℎ ) ∧ ( { 𝑎 } ⊕ 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) 𝑎 ) ∈ 𝑁 )
63 42 62 sseldd ⊢ ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 ∈ ℎ ) ∧ ( { 𝑎 } ⊕ 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) 𝑎 ) ∈ ℎ )
64 36 subgcl ⊢ ( ( ℎ ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ℎ ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) 𝑎 ) ∈ ℎ ) → ( 𝑥 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) 𝑎 ) ) ∈ ℎ )
65 40 41 63 64 syl3anc ⊢ ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 ∈ ℎ ) ∧ ( { 𝑎 } ⊕ 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) ( ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ( +g ‘ 𝐺 ) 𝑎 ) ) ∈ ℎ )
66 39 65 eqeltrrd ⊢ ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑥 ∈ ℎ ) ∧ ( { 𝑎 } ⊕ 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) ) → 𝑎 ∈ ℎ )
67 66 adantllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( { 𝑎 } ⊕ 𝑁 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ) ∧ 𝑥 ∈ ℎ ) ∧ ( { 𝑎 } ⊕ 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) ) → 𝑎 ∈ ℎ )
68 eqid ⊢ ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) = ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) )
69 ovex ⊢ ( { 𝑥 } ⊕ 𝑁 ) ∈ V
70 68 69 elrnmpti ⊢ ( ( { 𝑎 } ⊕ 𝑁 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ↔ ∃ 𝑥 ∈ ℎ ( { 𝑎 } ⊕ 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) )
71 70 bilani ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( { 𝑎 } ⊕ 𝑁 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ) → ∃ 𝑥 ∈ ℎ ( { 𝑎 } ⊕ 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) )
72 23 67 71 r19.29af ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ ( { 𝑎 } ⊕ 𝑁 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ) → 𝑎 ∈ ℎ )
73 simpr ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑎 ∈ ℎ ) → 𝑎 ∈ ℎ )
74 ovexd ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑎 ∈ ℎ ) → ( { 𝑎 } ⊕ 𝑁 ) ∈ V )
75 sneq ⊢ ( 𝑥 = 𝑎 → { 𝑥 } = { 𝑎 } )
76 75 oveq1d ⊢ ( 𝑥 = 𝑎 → ( { 𝑥 } ⊕ 𝑁 ) = ( { 𝑎 } ⊕ 𝑁 ) )
77 76 eqcomd ⊢ ( 𝑥 = 𝑎 → ( { 𝑎 } ⊕ 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) )
78 77 adantl ⊢ ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑎 ∈ ℎ ) ∧ 𝑥 = 𝑎 ) → ( { 𝑎 } ⊕ 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) )
79 68 73 74 78 elrnmptdv ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑎 ∈ ℎ ) → ( { 𝑎 } ⊕ 𝑁 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
80 72 79 impbida ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑎 ∈ 𝐵 ) → ( ( { 𝑎 } ⊕ 𝑁 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ↔ 𝑎 ∈ ℎ ) )
81 80 rabbidva ⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) → { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) } = { 𝑎 ∈ 𝐵 ∣ 𝑎 ∈ ℎ } )
82 30 adantl ⊢ ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) → ℎ ⊆ 𝐵 )
83 dfss7 ⊢ ( ℎ ⊆ 𝐵 ↔ { 𝑎 ∈ 𝐵 ∣ 𝑎 ∈ ℎ } = ℎ )
84 82 83 sylib ⊢ ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) → { 𝑎 ∈ 𝐵 ∣ 𝑎 ∈ ℎ } = ℎ )
85 84 adantr ⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) → { 𝑎 ∈ 𝐵 ∣ 𝑎 ∈ ℎ } = ℎ )
86 81 85 eqtr2d ⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) → ℎ = { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) } )
87 14 18 86 rspcedvd ⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) → ∃ 𝑓 ∈ 𝑇 ℎ = { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } )
88 87 anasss ⊢ ( ( 𝜑 ∧ ( ℎ ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ⊆ ℎ ) ) → ∃ 𝑓 ∈ 𝑇 ℎ = { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } )
89 10 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
90 3 eleq2i ⊢ ( 𝑓 ∈ 𝑇 ↔ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) )
91 90 bilani ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) → 𝑓 ∈ ( SubGrp ‘ 𝑄 ) )
92 1 6 7 89 91 nsgmgclem ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) → { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ∈ ( SubGrp ‘ 𝐺 ) )
93 92 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) ∧ ℎ = { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ) → { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ∈ ( SubGrp ‘ 𝐺 ) )
94 eleq1 ⊢ ( ℎ = { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } → ( ℎ ∈ ( SubGrp ‘ 𝐺 ) ↔ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ∈ ( SubGrp ‘ 𝐺 ) ) )
95 94 adantl ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) ∧ ℎ = { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ) → ( ℎ ∈ ( SubGrp ‘ 𝐺 ) ↔ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ∈ ( SubGrp ‘ 𝐺 ) ) )
96 93 95 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) ∧ ℎ = { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ) → ℎ ∈ ( SubGrp ‘ 𝐺 ) )
97 44 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) → 𝑁 ⊆ 𝐵 )
98 25 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) ∧ 𝑎 ∈ 𝑁 ) → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
99 simpr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) ∧ 𝑎 ∈ 𝑁 ) → 𝑎 ∈ 𝑁 )
100 7 grplsmid ⊢ ( ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑎 ∈ 𝑁 ) → ( { 𝑎 } ⊕ 𝑁 ) = 𝑁 )
101 98 99 100 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) ∧ 𝑎 ∈ 𝑁 ) → ( { 𝑎 } ⊕ 𝑁 ) = 𝑁 )
102 6 nsgqus0 ⊢ ( ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) → 𝑁 ∈ 𝑓 )
103 89 91 102 syl2anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) → 𝑁 ∈ 𝑓 )
104 103 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) ∧ 𝑎 ∈ 𝑁 ) → 𝑁 ∈ 𝑓 )
105 101 104 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) ∧ 𝑎 ∈ 𝑁 ) → ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 )
106 97 105 ssrabdv ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) → 𝑁 ⊆ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } )
107 106 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) ∧ ℎ = { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ) → 𝑁 ⊆ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } )
108 simpr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) ∧ ℎ = { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ) → ℎ = { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } )
109 107 108 sseqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) ∧ ℎ = { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ) → 𝑁 ⊆ ℎ )
110 96 109 jca ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) ∧ ℎ = { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ) → ( ℎ ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ⊆ ℎ ) )
111 110 r19.29an ⊢ ( ( 𝜑 ∧ ∃ 𝑓 ∈ 𝑇 ℎ = { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ) → ( ℎ ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ⊆ ℎ ) )
112 88 111 impbida ⊢ ( 𝜑 → ( ( ℎ ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ⊆ ℎ ) ↔ ∃ 𝑓 ∈ 𝑇 ℎ = { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ) )
113 13 112 bitrid ⊢ ( 𝜑 → ( ℎ ∈ 𝑆 ↔ ∃ 𝑓 ∈ 𝑇 ℎ = { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ) )
114 12 113 bitr4id ⊢ ( 𝜑 → ( ℎ ∈ ran 𝐹 ↔ ℎ ∈ 𝑆 ) )
115 114 eqrdv ⊢ ( 𝜑 → ran 𝐹 = 𝑆 )