Metamath Proof Explorer

Theorem nsgqusf1olem1

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 nsgqusf1olem1 ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) → 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 6 qusgrp ⊢ ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑄 ∈ Grp )
12 10 11 syl ⊢ ( 𝜑 → 𝑄 ∈ Grp )
13 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) → 𝑄 ∈ Grp )
14 1 subgss ⊢ ( ℎ ∈ ( SubGrp ‘ 𝐺 ) → ℎ ⊆ 𝐵 )
15 14 ad2antlr ⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) → ℎ ⊆ 𝐵 )
16 15 sselda ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) → 𝑥 ∈ 𝐵 )
17 ovex ⊢ ( 𝐺 ~QG 𝑁 ) ∈ V
18 17 ecelqsi ⊢ ( 𝑥 ∈ 𝐵 → [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ∈ ( 𝐵 / ( 𝐺 ~QG 𝑁 ) ) )
19 16 18 syl ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) → [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ∈ ( 𝐵 / ( 𝐺 ~QG 𝑁 ) ) )
20 nsgsubg ⊢ ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
21 10 20 syl ⊢ ( 𝜑 → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
22 21 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
23 1 7 22 16 quslsm ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) → [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) )
24 6 a1i ⊢ ( 𝜑 → 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝑁 ) ) )
25 1 a1i ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
26 ovexd ⊢ ( 𝜑 → ( 𝐺 ~QG 𝑁 ) ∈ V )
27 subgrcl ⊢ ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
28 21 27 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
29 24 25 26 28 qusbas ⊢ ( 𝜑 → ( 𝐵 / ( 𝐺 ~QG 𝑁 ) ) = ( Base ‘ 𝑄 ) )
30 29 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) → ( 𝐵 / ( 𝐺 ~QG 𝑁 ) ) = ( Base ‘ 𝑄 ) )
31 19 23 30 3eltr3d ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) → ( { 𝑥 } ⊕ 𝑁 ) ∈ ( Base ‘ 𝑄 ) )
32 31 ralrimiva ⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) → ∀ 𝑥 ∈ ℎ ( { 𝑥 } ⊕ 𝑁 ) ∈ ( Base ‘ 𝑄 ) )
33 eqid ⊢ ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) = ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) )
34 33 rnmptss ⊢ ( ∀ 𝑥 ∈ ℎ ( { 𝑥 } ⊕ 𝑁 ) ∈ ( Base ‘ 𝑄 ) → ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ⊆ ( Base ‘ 𝑄 ) )
35 32 34 syl ⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) → ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ⊆ ( Base ‘ 𝑄 ) )
36 nfv ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ )
37 ovexd ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) → ( { 𝑥 } ⊕ 𝑁 ) ∈ V )
38 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
39 38 subg0cl ⊢ ( ℎ ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) ∈ ℎ )
40 39 ne0d ⊢ ( ℎ ∈ ( SubGrp ‘ 𝐺 ) → ℎ ≠ ∅ )
41 40 ad2antlr ⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) → ℎ ≠ ∅ )
42 36 37 33 41 rnmptn0 ⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) → ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ≠ ∅ )
43 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) )
44 43 nfrn ⊢ Ⅎ 𝑥 ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) )
45 44 nfel2 ⊢ Ⅎ 𝑥 𝑖 ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) )
46 36 45 nfan ⊢ Ⅎ 𝑥 ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑖 ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
47 44 nfel2 ⊢ Ⅎ 𝑥 ( 𝑖 ( +g ‘ 𝑄 ) 𝑗 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) )
48 44 47 nfralw ⊢ Ⅎ 𝑥 ∀ 𝑗 ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ( 𝑖 ( +g ‘ 𝑄 ) 𝑗 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) )
49 44 nfel2 ⊢ Ⅎ 𝑥 ( ( invg ‘ 𝑄 ) ‘ 𝑖 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) )
50 48 49 nfan ⊢ Ⅎ 𝑥 ( ∀ 𝑗 ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ( 𝑖 ( +g ‘ 𝑄 ) 𝑗 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ∧ ( ( invg ‘ 𝑄 ) ‘ 𝑖 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
51 sneq ⊢ ( 𝑥 = 𝑧 → { 𝑥 } = { 𝑧 } )
52 51 oveq1d ⊢ ( 𝑥 = 𝑧 → ( { 𝑥 } ⊕ 𝑁 ) = ( { 𝑧 } ⊕ 𝑁 ) )
53 52 cbvmptv ⊢ ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) = ( 𝑧 ∈ ℎ ↦ ( { 𝑧 } ⊕ 𝑁 ) )
54 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) → ℎ ∈ ( SubGrp ‘ 𝐺 ) )
55 54 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑦 ∈ ℎ ) ∧ 𝑗 = ( { 𝑦 } ⊕ 𝑁 ) ) → ℎ ∈ ( SubGrp ‘ 𝐺 ) )
56 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑦 ∈ ℎ ) ∧ 𝑗 = ( { 𝑦 } ⊕ 𝑁 ) ) → 𝑥 ∈ ℎ )
57 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑦 ∈ ℎ ) ∧ 𝑗 = ( { 𝑦 } ⊕ 𝑁 ) ) → 𝑦 ∈ ℎ )
58 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
59 58 subgcl ⊢ ( ( ℎ ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ℎ ∧ 𝑦 ∈ ℎ ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ℎ )
60 55 56 57 59 syl3anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑦 ∈ ℎ ) ∧ 𝑗 = ( { 𝑦 } ⊕ 𝑁 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ℎ )
61 sneq ⊢ ( 𝑧 = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) → { 𝑧 } = { ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) } )
62 61 oveq1d ⊢ ( 𝑧 = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) → ( { 𝑧 } ⊕ 𝑁 ) = ( { ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) } ⊕ 𝑁 ) )
63 62 eqeq2d ⊢ ( 𝑧 = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) → ( ( 𝑖 ( +g ‘ 𝑄 ) 𝑗 ) = ( { 𝑧 } ⊕ 𝑁 ) ↔ ( 𝑖 ( +g ‘ 𝑄 ) 𝑗 ) = ( { ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) } ⊕ 𝑁 ) ) )
64 63 adantl ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑦 ∈ ℎ ) ∧ 𝑗 = ( { 𝑦 } ⊕ 𝑁 ) ) ∧ 𝑧 = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ) → ( ( 𝑖 ( +g ‘ 𝑄 ) 𝑗 ) = ( { 𝑧 } ⊕ 𝑁 ) ↔ ( 𝑖 ( +g ‘ 𝑄 ) 𝑗 ) = ( { ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) } ⊕ 𝑁 ) ) )
65 simpr ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) → 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) )
66 23 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) → [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) )
67 65 66 eqtr4d ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) → 𝑖 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) )
68 67 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑦 ∈ ℎ ) ∧ 𝑗 = ( { 𝑦 } ⊕ 𝑁 ) ) → 𝑖 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) )
69 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑦 ∈ ℎ ) ∧ 𝑗 = ( { 𝑦 } ⊕ 𝑁 ) ) → 𝑗 = ( { 𝑦 } ⊕ 𝑁 ) )
70 10 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
71 70 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑦 ∈ ℎ ) ∧ 𝑗 = ( { 𝑦 } ⊕ 𝑁 ) ) → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
72 71 20 syl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑦 ∈ ℎ ) ∧ 𝑗 = ( { 𝑦 } ⊕ 𝑁 ) ) → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
73 55 14 syl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑦 ∈ ℎ ) ∧ 𝑗 = ( { 𝑦 } ⊕ 𝑁 ) ) → ℎ ⊆ 𝐵 )
74 73 57 sseldd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑦 ∈ ℎ ) ∧ 𝑗 = ( { 𝑦 } ⊕ 𝑁 ) ) → 𝑦 ∈ 𝐵 )
75 1 7 72 74 quslsm ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑦 ∈ ℎ ) ∧ 𝑗 = ( { 𝑦 } ⊕ 𝑁 ) ) → [ 𝑦 ] ( 𝐺 ~QG 𝑁 ) = ( { 𝑦 } ⊕ 𝑁 ) )
76 69 75 eqtr4d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑦 ∈ ℎ ) ∧ 𝑗 = ( { 𝑦 } ⊕ 𝑁 ) ) → 𝑗 = [ 𝑦 ] ( 𝐺 ~QG 𝑁 ) )
77 68 76 oveq12d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑦 ∈ ℎ ) ∧ 𝑗 = ( { 𝑦 } ⊕ 𝑁 ) ) → ( 𝑖 ( +g ‘ 𝑄 ) 𝑗 ) = ( [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ( +g ‘ 𝑄 ) [ 𝑦 ] ( 𝐺 ~QG 𝑁 ) ) )
78 16 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) → 𝑥 ∈ 𝐵 )
79 78 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑦 ∈ ℎ ) ∧ 𝑗 = ( { 𝑦 } ⊕ 𝑁 ) ) → 𝑥 ∈ 𝐵 )
80 eqid ⊢ ( +g ‘ 𝑄 ) = ( +g ‘ 𝑄 )
81 6 1 58 80 qusadd ⊢ ( ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ( +g ‘ 𝑄 ) [ 𝑦 ] ( 𝐺 ~QG 𝑁 ) ) = [ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ] ( 𝐺 ~QG 𝑁 ) )
82 71 79 74 81 syl3anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑦 ∈ ℎ ) ∧ 𝑗 = ( { 𝑦 } ⊕ 𝑁 ) ) → ( [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ( +g ‘ 𝑄 ) [ 𝑦 ] ( 𝐺 ~QG 𝑁 ) ) = [ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ] ( 𝐺 ~QG 𝑁 ) )
83 73 60 sseldd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑦 ∈ ℎ ) ∧ 𝑗 = ( { 𝑦 } ⊕ 𝑁 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝐵 )
84 1 7 72 83 quslsm ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑦 ∈ ℎ ) ∧ 𝑗 = ( { 𝑦 } ⊕ 𝑁 ) ) → [ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ] ( 𝐺 ~QG 𝑁 ) = ( { ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) } ⊕ 𝑁 ) )
85 77 82 84 3eqtrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑦 ∈ ℎ ) ∧ 𝑗 = ( { 𝑦 } ⊕ 𝑁 ) ) → ( 𝑖 ( +g ‘ 𝑄 ) 𝑗 ) = ( { ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) } ⊕ 𝑁 ) )
86 60 64 85 rspcedvd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑦 ∈ ℎ ) ∧ 𝑗 = ( { 𝑦 } ⊕ 𝑁 ) ) → ∃ 𝑧 ∈ ℎ ( 𝑖 ( +g ‘ 𝑄 ) 𝑗 ) = ( { 𝑧 } ⊕ 𝑁 ) )
87 ovexd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑦 ∈ ℎ ) ∧ 𝑗 = ( { 𝑦 } ⊕ 𝑁 ) ) → ( 𝑖 ( +g ‘ 𝑄 ) 𝑗 ) ∈ V )
88 53 86 87 elrnmptd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑦 ∈ ℎ ) ∧ 𝑗 = ( { 𝑦 } ⊕ 𝑁 ) ) → ( 𝑖 ( +g ‘ 𝑄 ) 𝑗 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
89 88 adantllr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑗 ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ) ∧ 𝑦 ∈ ℎ ) ∧ 𝑗 = ( { 𝑦 } ⊕ 𝑁 ) ) → ( 𝑖 ( +g ‘ 𝑄 ) 𝑗 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
90 sneq ⊢ ( 𝑥 = 𝑦 → { 𝑥 } = { 𝑦 } )
91 90 oveq1d ⊢ ( 𝑥 = 𝑦 → ( { 𝑥 } ⊕ 𝑁 ) = ( { 𝑦 } ⊕ 𝑁 ) )
92 91 cbvmptv ⊢ ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) = ( 𝑦 ∈ ℎ ↦ ( { 𝑦 } ⊕ 𝑁 ) )
93 ovex ⊢ ( { 𝑦 } ⊕ 𝑁 ) ∈ V
94 92 93 elrnmpti ⊢ ( 𝑗 ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ↔ ∃ 𝑦 ∈ ℎ 𝑗 = ( { 𝑦 } ⊕ 𝑁 ) )
95 94 bilani ⊢ ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑗 ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ) → ∃ 𝑦 ∈ ℎ 𝑗 = ( { 𝑦 } ⊕ 𝑁 ) )
96 89 95 r19.29a ⊢ ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑗 ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ) → ( 𝑖 ( +g ‘ 𝑄 ) 𝑗 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
97 96 ralrimiva ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) → ∀ 𝑗 ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ( 𝑖 ( +g ‘ 𝑄 ) 𝑗 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
98 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
99 98 subginvcl ⊢ ( ( ℎ ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑥 ∈ ℎ ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℎ )
100 99 ad5ant24 ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℎ )
101 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑦 = ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) → 𝑦 = ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) )
102 101 sneqd ⊢ ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑦 = ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) → { 𝑦 } = { ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) } )
103 102 oveq1d ⊢ ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑦 = ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) → ( { 𝑦 } ⊕ 𝑁 ) = ( { ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) } ⊕ 𝑁 ) )
104 15 adantr ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) → ℎ ⊆ 𝐵 )
105 99 ad4ant24 ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ ℎ )
106 104 105 sseldd ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) → ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ∈ 𝐵 )
107 1 7 22 106 quslsm ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) → [ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ] ( 𝐺 ~QG 𝑁 ) = ( { ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) } ⊕ 𝑁 ) )
108 107 ad2antrr ⊢ ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑦 = ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) → [ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ] ( 𝐺 ~QG 𝑁 ) = ( { ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) } ⊕ 𝑁 ) )
109 103 108 eqtr4d ⊢ ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑦 = ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) → ( { 𝑦 } ⊕ 𝑁 ) = [ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ] ( 𝐺 ~QG 𝑁 ) )
110 109 eqeq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑦 = ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ) → ( ( ( invg ‘ 𝑄 ) ‘ 𝑖 ) = ( { 𝑦 } ⊕ 𝑁 ) ↔ ( ( invg ‘ 𝑄 ) ‘ 𝑖 ) = [ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ] ( 𝐺 ~QG 𝑁 ) ) )
111 67 fveq2d ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) → ( ( invg ‘ 𝑄 ) ‘ 𝑖 ) = ( ( invg ‘ 𝑄 ) ‘ [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) )
112 eqid ⊢ ( invg ‘ 𝑄 ) = ( invg ‘ 𝑄 )
113 6 1 98 112 qusinv ⊢ ( ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( invg ‘ 𝑄 ) ‘ [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) = [ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ] ( 𝐺 ~QG 𝑁 ) )
114 70 78 113 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) → ( ( invg ‘ 𝑄 ) ‘ [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) = [ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ] ( 𝐺 ~QG 𝑁 ) )
115 111 114 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) → ( ( invg ‘ 𝑄 ) ‘ 𝑖 ) = [ ( ( invg ‘ 𝐺 ) ‘ 𝑥 ) ] ( 𝐺 ~QG 𝑁 ) )
116 100 110 115 rspcedvd ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) → ∃ 𝑦 ∈ ℎ ( ( invg ‘ 𝑄 ) ‘ 𝑖 ) = ( { 𝑦 } ⊕ 𝑁 ) )
117 fvexd ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) → ( ( invg ‘ 𝑄 ) ‘ 𝑖 ) ∈ V )
118 92 116 117 elrnmptd ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) → ( ( invg ‘ 𝑄 ) ‘ 𝑖 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
119 97 118 jca ⊢ ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) → ( ∀ 𝑗 ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ( 𝑖 ( +g ‘ 𝑄 ) 𝑗 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ∧ ( ( invg ‘ 𝑄 ) ‘ 𝑖 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ) )
120 119 adantllr ⊢ ( ( ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑖 ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ) ∧ 𝑥 ∈ ℎ ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) → ( ∀ 𝑗 ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ( 𝑖 ( +g ‘ 𝑄 ) 𝑗 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ∧ ( ( invg ‘ 𝑄 ) ‘ 𝑖 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ) )
121 ovex ⊢ ( { 𝑥 } ⊕ 𝑁 ) ∈ V
122 33 121 elrnmpti ⊢ ( 𝑖 ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ↔ ∃ 𝑥 ∈ ℎ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) )
123 122 bilani ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑖 ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ) → ∃ 𝑥 ∈ ℎ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) )
124 46 50 120 123 r19.29af2 ⊢ ( ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) ∧ 𝑖 ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ) → ( ∀ 𝑗 ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ( 𝑖 ( +g ‘ 𝑄 ) 𝑗 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ∧ ( ( invg ‘ 𝑄 ) ‘ 𝑖 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ) )
125 124 ralrimiva ⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) → ∀ 𝑖 ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ( ∀ 𝑗 ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ( 𝑖 ( +g ‘ 𝑄 ) 𝑗 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ∧ ( ( invg ‘ 𝑄 ) ‘ 𝑖 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ) )
126 eqid ⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
127 126 80 112 issubg2 ⊢ ( 𝑄 ∈ Grp → ( ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ∈ ( SubGrp ‘ 𝑄 ) ↔ ( ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ⊆ ( Base ‘ 𝑄 ) ∧ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ≠ ∅ ∧ ∀ 𝑖 ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ( ∀ 𝑗 ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ( 𝑖 ( +g ‘ 𝑄 ) 𝑗 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ∧ ( ( invg ‘ 𝑄 ) ‘ 𝑖 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ) ) ) )
128 127 biimpar ⊢ ( ( 𝑄 ∈ Grp ∧ ( ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ⊆ ( Base ‘ 𝑄 ) ∧ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ≠ ∅ ∧ ∀ 𝑖 ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ( ∀ 𝑗 ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ( 𝑖 ( +g ‘ 𝑄 ) 𝑗 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ∧ ( ( invg ‘ 𝑄 ) ‘ 𝑖 ) ∈ ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ) ) ) → ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ∈ ( SubGrp ‘ 𝑄 ) )
129 13 35 42 125 128 syl13anc ⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) → ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ∈ ( SubGrp ‘ 𝑄 ) )
130 129 3 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) → ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ∈ 𝑇 )