Metamath Proof Explorer

Theorem nsgqusf1olem2

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 nsgqusf1olem2 ( 𝜑 → 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 simpr ⊢ ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 = ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ) → 𝑓 = ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
12 2 reqabi ⊢ ( ℎ ∈ 𝑆 ↔ ( ℎ ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ⊆ ℎ ) )
13 1 2 3 4 5 6 7 8 9 10 nsgqusf1olem1 ⊢ ( ( ( 𝜑 ∧ ℎ ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑁 ⊆ ℎ ) → ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ∈ 𝑇 )
14 13 anasss ⊢ ( ( 𝜑 ∧ ( ℎ ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ⊆ ℎ ) ) → ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ∈ 𝑇 )
15 14 3 eleqtrdi ⊢ ( ( 𝜑 ∧ ( ℎ ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑁 ⊆ ℎ ) ) → ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ∈ ( SubGrp ‘ 𝑄 ) )
16 12 15 sylan2b ⊢ ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) → ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ∈ ( SubGrp ‘ 𝑄 ) )
17 16 adantr ⊢ ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 = ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ) → ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ∈ ( SubGrp ‘ 𝑄 ) )
18 11 17 eqeltrd ⊢ ( ( ( 𝜑 ∧ ℎ ∈ 𝑆 ) ∧ 𝑓 = ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ) → 𝑓 ∈ ( SubGrp ‘ 𝑄 ) )
19 18 r19.29an ⊢ ( ( 𝜑 ∧ ∃ ℎ ∈ 𝑆 𝑓 = ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ) → 𝑓 ∈ ( SubGrp ‘ 𝑄 ) )
20 sseq2 ⊢ ( ℎ = { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } → ( 𝑁 ⊆ ℎ ↔ 𝑁 ⊆ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ) )
21 10 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
22 simpr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) → 𝑓 ∈ ( SubGrp ‘ 𝑄 ) )
23 1 6 7 21 22 nsgmgclem ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) → { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ∈ ( SubGrp ‘ 𝐺 ) )
24 3 eleq2i ⊢ ( 𝑓 ∈ 𝑇 ↔ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) )
25 nsgsubg ⊢ ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
26 10 25 syl ⊢ ( 𝜑 → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
27 1 subgss ⊢ ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → 𝑁 ⊆ 𝐵 )
28 26 27 syl ⊢ ( 𝜑 → 𝑁 ⊆ 𝐵 )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) → 𝑁 ⊆ 𝐵 )
30 26 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) ∧ 𝑎 ∈ 𝑁 ) → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
31 7 grplsmid ⊢ ( ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑎 ∈ 𝑁 ) → ( { 𝑎 } ⊕ 𝑁 ) = 𝑁 )
32 30 31 sylancom ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) ∧ 𝑎 ∈ 𝑁 ) → ( { 𝑎 } ⊕ 𝑁 ) = 𝑁 )
33 24 biimpi ⊢ ( 𝑓 ∈ 𝑇 → 𝑓 ∈ ( SubGrp ‘ 𝑄 ) )
34 6 nsgqus0 ⊢ ( ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) → 𝑁 ∈ 𝑓 )
35 10 33 34 syl2an ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) → 𝑁 ∈ 𝑓 )
36 35 adantr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) ∧ 𝑎 ∈ 𝑁 ) → 𝑁 ∈ 𝑓 )
37 32 36 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) ∧ 𝑎 ∈ 𝑁 ) → ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 )
38 29 37 ssrabdv ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑇 ) → 𝑁 ⊆ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } )
39 24 38 sylan2br ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) → 𝑁 ⊆ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } )
40 20 23 39 elrabd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) → { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ∈ { ℎ ∈ ( SubGrp ‘ 𝐺 ) ∣ 𝑁 ⊆ ℎ } )
41 40 2 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) → { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ∈ 𝑆 )
42 mpteq1 ⊢ ( ℎ = { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } → ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) = ( 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
43 42 rneqd ⊢ ( ℎ = { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } → ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) = ran ( 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
44 43 eqeq2d ⊢ ( ℎ = { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } → ( 𝑓 = ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ↔ 𝑓 = ran ( 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ) )
45 44 adantl ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) ∧ ℎ = { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ) → ( 𝑓 = ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ↔ 𝑓 = ran ( 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ) )
46 eqid ⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
47 46 subgss ⊢ ( 𝑓 ∈ ( SubGrp ‘ 𝑄 ) → 𝑓 ⊆ ( Base ‘ 𝑄 ) )
48 47 adantl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) → 𝑓 ⊆ ( Base ‘ 𝑄 ) )
49 48 sselda ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) ∧ 𝑖 ∈ 𝑓 ) → 𝑖 ∈ ( Base ‘ 𝑄 ) )
50 6 a1i ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) ∧ 𝑖 ∈ 𝑓 ) → 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝑁 ) ) )
51 1 a1i ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) ∧ 𝑖 ∈ 𝑓 ) → 𝐵 = ( Base ‘ 𝐺 ) )
52 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) ∧ 𝑖 ∈ 𝑓 ) → ( 𝐺 ~QG 𝑁 ) ∈ V )
53 subgrcl ⊢ ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
54 26 53 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
55 54 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) ∧ 𝑖 ∈ 𝑓 ) → 𝐺 ∈ Grp )
56 50 51 52 55 qusbas ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) ∧ 𝑖 ∈ 𝑓 ) → ( 𝐵 / ( 𝐺 ~QG 𝑁 ) ) = ( Base ‘ 𝑄 ) )
57 49 56 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) ∧ 𝑖 ∈ 𝑓 ) → 𝑖 ∈ ( 𝐵 / ( 𝐺 ~QG 𝑁 ) ) )
58 elqsi ⊢ ( 𝑖 ∈ ( 𝐵 / ( 𝐺 ~QG 𝑁 ) ) → ∃ 𝑥 ∈ 𝐵 𝑖 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) )
59 57 58 syl ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) ∧ 𝑖 ∈ 𝑓 ) → ∃ 𝑥 ∈ 𝐵 𝑖 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) )
60 sneq ⊢ ( 𝑎 = 𝑥 → { 𝑎 } = { 𝑥 } )
61 60 oveq1d ⊢ ( 𝑎 = 𝑥 → ( { 𝑎 } ⊕ 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) )
62 61 eleq1d ⊢ ( 𝑎 = 𝑥 → ( ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 ↔ ( { 𝑥 } ⊕ 𝑁 ) ∈ 𝑓 ) )
63 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) ∧ 𝑖 ∈ 𝑓 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑖 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) → 𝑥 ∈ 𝐵 )
64 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) ∧ 𝑖 ∈ 𝑓 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑖 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) → 𝑖 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) )
65 26 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) ∧ 𝑖 ∈ 𝑓 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑖 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
66 1 7 65 63 quslsm ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) ∧ 𝑖 ∈ 𝑓 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑖 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) → [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) = ( { 𝑥 } ⊕ 𝑁 ) )
67 64 66 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) ∧ 𝑖 ∈ 𝑓 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑖 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) → 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) )
68 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) ∧ 𝑖 ∈ 𝑓 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑖 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) → 𝑖 ∈ 𝑓 )
69 67 68 eqeltrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) ∧ 𝑖 ∈ 𝑓 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑖 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) → ( { 𝑥 } ⊕ 𝑁 ) ∈ 𝑓 )
70 62 63 69 elrabd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) ∧ 𝑖 ∈ 𝑓 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑖 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) → 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } )
71 70 67 jca ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) ∧ 𝑖 ∈ 𝑓 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑖 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) → ( 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) )
72 71 expl ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) ∧ 𝑖 ∈ 𝑓 ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑖 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ) → ( 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ) )
73 72 reximdv2 ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) ∧ 𝑖 ∈ 𝑓 ) → ( ∃ 𝑥 ∈ 𝐵 𝑖 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) → ∃ 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) )
74 59 73 mpd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) ∧ 𝑖 ∈ 𝑓 ) → ∃ 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) )
75 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) → 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } )
76 62 elrab ⊢ ( 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ↔ ( 𝑥 ∈ 𝐵 ∧ ( { 𝑥 } ⊕ 𝑁 ) ∈ 𝑓 ) )
77 75 76 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) → ( 𝑥 ∈ 𝐵 ∧ ( { 𝑥 } ⊕ 𝑁 ) ∈ 𝑓 ) )
78 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( { 𝑥 } ⊕ 𝑁 ) ∈ 𝑓 ) → 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) )
79 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( { 𝑥 } ⊕ 𝑁 ) ∈ 𝑓 ) → ( { 𝑥 } ⊕ 𝑁 ) ∈ 𝑓 )
80 78 79 eqeltrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ 𝑥 ∈ 𝐵 ) ∧ ( { 𝑥 } ⊕ 𝑁 ) ∈ 𝑓 ) → 𝑖 ∈ 𝑓 )
81 80 anasss ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ ( { 𝑥 } ⊕ 𝑁 ) ∈ 𝑓 ) ) → 𝑖 ∈ 𝑓 )
82 81 adantllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ ( { 𝑥 } ⊕ 𝑁 ) ∈ 𝑓 ) ) → 𝑖 ∈ 𝑓 )
83 77 82 mpdan ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) ∧ 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ) ∧ 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) → 𝑖 ∈ 𝑓 )
84 83 r19.29an ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) ∧ ∃ 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) → 𝑖 ∈ 𝑓 )
85 74 84 impbida ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) → ( 𝑖 ∈ 𝑓 ↔ ∃ 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) )
86 eqid ⊢ ( 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ↦ ( { 𝑥 } ⊕ 𝑁 ) ) = ( 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ↦ ( { 𝑥 } ⊕ 𝑁 ) )
87 86 elrnmpt ⊢ ( 𝑖 ∈ V → ( 𝑖 ∈ ran ( 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ↔ ∃ 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) ) )
88 87 elv ⊢ ( 𝑖 ∈ ran ( 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ↔ ∃ 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } 𝑖 = ( { 𝑥 } ⊕ 𝑁 ) )
89 85 88 bitr4di ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) → ( 𝑖 ∈ 𝑓 ↔ 𝑖 ∈ ran ( 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ) )
90 89 eqrdv ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) → 𝑓 = ran ( 𝑥 ∈ { 𝑎 ∈ 𝐵 ∣ ( { 𝑎 } ⊕ 𝑁 ) ∈ 𝑓 } ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
91 41 45 90 rspcedvd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) → ∃ ℎ ∈ 𝑆 𝑓 = ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) )
92 19 91 impbida ⊢ ( 𝜑 → ( ∃ ℎ ∈ 𝑆 𝑓 = ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) ↔ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) ) )
93 92 abbidv ⊢ ( 𝜑 → { 𝑓 ∣ ∃ ℎ ∈ 𝑆 𝑓 = ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) } = { 𝑓 ∣ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) } )
94 8 rnmpt ⊢ ran 𝐸 = { 𝑓 ∣ ∃ ℎ ∈ 𝑆 𝑓 = ran ( 𝑥 ∈ ℎ ↦ ( { 𝑥 } ⊕ 𝑁 ) ) }
95 abid1 ⊢ ( SubGrp ‘ 𝑄 ) = { 𝑓 ∣ 𝑓 ∈ ( SubGrp ‘ 𝑄 ) }
96 93 94 95 3eqtr4g ⊢ ( 𝜑 → ran 𝐸 = ( SubGrp ‘ 𝑄 ) )
97 96 3 eqtr4di ⊢ ( 𝜑 → ran 𝐸 = 𝑇 )