This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ghmqusnsglem1

Description: Lemma for ghmqusnsg . (Contributed by Thierry Arnoux, 13-May-2025)

Ref Expression
Hypotheses ghmqusnsg.0 ⊢ 0 = ( 0g ‘ 𝐻 )
ghmqusnsg.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
ghmqusnsg.k ⊢ 𝐾 = ( ◡ 𝐹 “ { 0 } )
ghmqusnsg.q ⊢ 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝑁 ) )
ghmqusnsg.j ⊢ 𝐽 = ( 𝑞 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐹 “ 𝑞 ) )
ghmqusnsg.n ⊢ ( 𝜑 → 𝑁 ⊆ 𝐾 )
ghmqusnsg.1 ⊢ ( 𝜑 → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
ghmqusnsglem1.x ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐺 ) )
Assertion ghmqusnsglem1 ( 𝜑 → ( 𝐽 ‘ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) = ( 𝐹 ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 ghmqusnsg.0 ⊢ 0 = ( 0g ‘ 𝐻 )
2 ghmqusnsg.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
3 ghmqusnsg.k ⊢ 𝐾 = ( ◡ 𝐹 “ { 0 } )
4 ghmqusnsg.q ⊢ 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝑁 ) )
5 ghmqusnsg.j ⊢ 𝐽 = ( 𝑞 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐹 “ 𝑞 ) )
6 ghmqusnsg.n ⊢ ( 𝜑 → 𝑁 ⊆ 𝐾 )
7 ghmqusnsg.1 ⊢ ( 𝜑 → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
8 ghmqusnsglem1.x ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐺 ) )
9 imaeq2 ⊢ ( 𝑞 = [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) → ( 𝐹 “ 𝑞 ) = ( 𝐹 “ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) )
10 9 unieqd ⊢ ( 𝑞 = [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) → ∪ ( 𝐹 “ 𝑞 ) = ∪ ( 𝐹 “ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) )
11 ovex ⊢ ( 𝐺 ~QG 𝑁 ) ∈ V
12 11 ecelqsi ⊢ ( 𝑋 ∈ ( Base ‘ 𝐺 ) → [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ∈ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑁 ) ) )
13 8 12 syl ⊢ ( 𝜑 → [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ∈ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑁 ) ) )
14 4 a1i ⊢ ( 𝜑 → 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝑁 ) ) )
15 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
16 ovexd ⊢ ( 𝜑 → ( 𝐺 ~QG 𝑁 ) ∈ V )
17 ghmgrp1 ⊢ ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) → 𝐺 ∈ Grp )
18 2 17 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
19 14 15 16 18 qusbas ⊢ ( 𝜑 → ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑁 ) ) = ( Base ‘ 𝑄 ) )
20 13 19 eleqtrd ⊢ ( 𝜑 → [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ∈ ( Base ‘ 𝑄 ) )
21 2 imaexd ⊢ ( 𝜑 → ( 𝐹 “ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) ∈ V )
22 21 uniexd ⊢ ( 𝜑 → ∪ ( 𝐹 “ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) ∈ V )
23 5 10 20 22 fvmptd3 ⊢ ( 𝜑 → ( 𝐽 ‘ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) = ∪ ( 𝐹 “ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) )
24 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
25 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
26 24 25 ghmf ⊢ ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) → 𝐹 : ( Base ‘ 𝐺 ) ⟶ ( Base ‘ 𝐻 ) )
27 2 26 syl ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝐺 ) ⟶ ( Base ‘ 𝐻 ) )
28 27 ffnd ⊢ ( 𝜑 → 𝐹 Fn ( Base ‘ 𝐺 ) )
29 nsgsubg ⊢ ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
30 eqid ⊢ ( 𝐺 ~QG 𝑁 ) = ( 𝐺 ~QG 𝑁 )
31 24 30 eqger ⊢ ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺 ~QG 𝑁 ) Er ( Base ‘ 𝐺 ) )
32 7 29 31 3syl ⊢ ( 𝜑 → ( 𝐺 ~QG 𝑁 ) Er ( Base ‘ 𝐺 ) )
33 32 ecss ⊢ ( 𝜑 → [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ⊆ ( Base ‘ 𝐺 ) )
34 28 33 fvelimabd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐹 “ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) ↔ ∃ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ( 𝐹 ‘ 𝑧 ) = 𝑦 ) )
35 simpr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) → ( 𝐹 ‘ 𝑧 ) = 𝑦 )
36 2 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
37 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
38 36 17 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) → 𝐺 ∈ Grp )
39 8 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) → 𝑋 ∈ ( Base ‘ 𝐺 ) )
40 24 37 38 39 grpinvcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) → ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐺 ) )
41 33 sselda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) → 𝑧 ∈ ( Base ‘ 𝐺 ) )
42 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
43 eqid ⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐻 )
44 24 42 43 ghmlin ⊢ ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) → ( 𝐹 ‘ ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑧 ) ) = ( ( 𝐹 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑧 ) ) )
45 36 40 41 44 syl3anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) → ( 𝐹 ‘ ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑧 ) ) = ( ( 𝐹 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑧 ) ) )
46 28 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) → 𝐹 Fn ( Base ‘ 𝐺 ) )
47 6 3 sseqtrdi ⊢ ( 𝜑 → 𝑁 ⊆ ( ◡ 𝐹 “ { 0 } ) )
48 47 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) → 𝑁 ⊆ ( ◡ 𝐹 “ { 0 } ) )
49 24 subgss ⊢ ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → 𝑁 ⊆ ( Base ‘ 𝐺 ) )
50 7 29 49 3syl ⊢ ( 𝜑 → 𝑁 ⊆ ( Base ‘ 𝐺 ) )
51 50 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) → 𝑁 ⊆ ( Base ‘ 𝐺 ) )
52 vex ⊢ 𝑧 ∈ V
53 elecg ⊢ ( ( 𝑧 ∈ V ∧ 𝑋 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ↔ 𝑋 ( 𝐺 ~QG 𝑁 ) 𝑧 ) )
54 52 53 mpan ⊢ ( 𝑋 ∈ ( Base ‘ 𝐺 ) → ( 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ↔ 𝑋 ( 𝐺 ~QG 𝑁 ) 𝑧 ) )
55 54 biimpa ⊢ ( ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) → 𝑋 ( 𝐺 ~QG 𝑁 ) 𝑧 )
56 8 55 sylan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) → 𝑋 ( 𝐺 ~QG 𝑁 ) 𝑧 )
57 24 37 42 30 eqgval ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑁 ⊆ ( Base ‘ 𝐺 ) ) → ( 𝑋 ( 𝐺 ~QG 𝑁 ) 𝑧 ↔ ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑁 ) ) )
58 57 biimpa ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ⊆ ( Base ‘ 𝐺 ) ) ∧ 𝑋 ( 𝐺 ~QG 𝑁 ) 𝑧 ) → ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑁 ) )
59 58 simp3d ⊢ ( ( ( 𝐺 ∈ Grp ∧ 𝑁 ⊆ ( Base ‘ 𝐺 ) ) ∧ 𝑋 ( 𝐺 ~QG 𝑁 ) 𝑧 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑁 )
60 38 51 56 59 syl21anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑁 )
61 48 60 sseldd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ ( ◡ 𝐹 “ { 0 } ) )
62 fniniseg ⊢ ( 𝐹 Fn ( Base ‘ 𝐺 ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ ( ◡ 𝐹 “ { 0 } ) ↔ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ ( Base ‘ 𝐺 ) ∧ ( 𝐹 ‘ ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑧 ) ) = 0 ) ) )
63 62 biimpa ⊢ ( ( 𝐹 Fn ( Base ‘ 𝐺 ) ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ ( ◡ 𝐹 “ { 0 } ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ ( Base ‘ 𝐺 ) ∧ ( 𝐹 ‘ ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑧 ) ) = 0 ) )
64 46 61 63 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑧 ) ∈ ( Base ‘ 𝐺 ) ∧ ( 𝐹 ‘ ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑧 ) ) = 0 ) )
65 64 simprd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) → ( 𝐹 ‘ ( ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ( +g ‘ 𝐺 ) 𝑧 ) ) = 0 )
66 45 65 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) → ( ( 𝐹 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑧 ) ) = 0 )
67 66 oveq2d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) → ( ( 𝐹 ‘ 𝑋 ) ( +g ‘ 𝐻 ) ( ( 𝐹 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑧 ) ) ) = ( ( 𝐹 ‘ 𝑋 ) ( +g ‘ 𝐻 ) 0 ) )
68 eqid ⊢ ( invg ‘ 𝐻 ) = ( invg ‘ 𝐻 )
69 24 37 68 ghminv ⊢ ( ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ∧ 𝑋 ∈ ( Base ‘ 𝐺 ) ) → ( 𝐹 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) = ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ 𝑋 ) ) )
70 36 39 69 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) → ( 𝐹 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) = ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ 𝑋 ) ) )
71 70 oveq1d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) → ( ( 𝐹 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑧 ) ) = ( ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ 𝑋 ) ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑧 ) ) )
72 71 oveq2d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) → ( ( 𝐹 ‘ 𝑋 ) ( +g ‘ 𝐻 ) ( ( 𝐹 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑧 ) ) ) = ( ( 𝐹 ‘ 𝑋 ) ( +g ‘ 𝐻 ) ( ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ 𝑋 ) ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑧 ) ) ) )
73 ghmgrp2 ⊢ ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) → 𝐻 ∈ Grp )
74 36 73 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) → 𝐻 ∈ Grp )
75 36 26 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) → 𝐹 : ( Base ‘ 𝐺 ) ⟶ ( Base ‘ 𝐻 ) )
76 75 39 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) → ( 𝐹 ‘ 𝑋 ) ∈ ( Base ‘ 𝐻 ) )
77 75 41 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ( Base ‘ 𝐻 ) )
78 25 43 68 grpasscan1 ⊢ ( ( 𝐻 ∈ Grp ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( Base ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( Base ‘ 𝐻 ) ) → ( ( 𝐹 ‘ 𝑋 ) ( +g ‘ 𝐻 ) ( ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ 𝑋 ) ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑧 ) ) ) = ( 𝐹 ‘ 𝑧 ) )
79 74 76 77 78 syl3anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) → ( ( 𝐹 ‘ 𝑋 ) ( +g ‘ 𝐻 ) ( ( ( invg ‘ 𝐻 ) ‘ ( 𝐹 ‘ 𝑋 ) ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑧 ) ) ) = ( 𝐹 ‘ 𝑧 ) )
80 72 79 eqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) → ( ( 𝐹 ‘ 𝑋 ) ( +g ‘ 𝐻 ) ( ( 𝐹 ‘ ( ( invg ‘ 𝐺 ) ‘ 𝑋 ) ) ( +g ‘ 𝐻 ) ( 𝐹 ‘ 𝑧 ) ) ) = ( 𝐹 ‘ 𝑧 ) )
81 25 43 1 74 76 grpridd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) → ( ( 𝐹 ‘ 𝑋 ) ( +g ‘ 𝐻 ) 0 ) = ( 𝐹 ‘ 𝑋 ) )
82 67 80 81 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑋 ) )
83 82 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑋 ) )
84 35 83 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑦 ) → 𝑦 = ( 𝐹 ‘ 𝑋 ) )
85 84 r19.29an ⊢ ( ( 𝜑 ∧ ∃ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ( 𝐹 ‘ 𝑧 ) = 𝑦 ) → 𝑦 = ( 𝐹 ‘ 𝑋 ) )
86 fveqeq2 ⊢ ( 𝑧 = 𝑋 → ( ( 𝐹 ‘ 𝑧 ) = 𝑦 ↔ ( 𝐹 ‘ 𝑋 ) = 𝑦 ) )
87 ecref ⊢ ( ( ( 𝐺 ~QG 𝑁 ) Er ( Base ‘ 𝐺 ) ∧ 𝑋 ∈ ( Base ‘ 𝐺 ) ) → 𝑋 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) )
88 32 8 87 syl2anc ⊢ ( 𝜑 → 𝑋 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) )
89 88 adantr ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝐹 ‘ 𝑋 ) ) → 𝑋 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) )
90 simpr ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝐹 ‘ 𝑋 ) ) → 𝑦 = ( 𝐹 ‘ 𝑋 ) )
91 90 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝐹 ‘ 𝑋 ) ) → ( 𝐹 ‘ 𝑋 ) = 𝑦 )
92 86 89 91 rspcedvdw ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝐹 ‘ 𝑋 ) ) → ∃ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ( 𝐹 ‘ 𝑧 ) = 𝑦 )
93 85 92 impbida ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ( 𝐹 ‘ 𝑧 ) = 𝑦 ↔ 𝑦 = ( 𝐹 ‘ 𝑋 ) ) )
94 velsn ⊢ ( 𝑦 ∈ { ( 𝐹 ‘ 𝑋 ) } ↔ 𝑦 = ( 𝐹 ‘ 𝑋 ) )
95 93 94 bitr4di ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ( 𝐹 ‘ 𝑧 ) = 𝑦 ↔ 𝑦 ∈ { ( 𝐹 ‘ 𝑋 ) } ) )
96 34 95 bitrd ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝐹 “ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) ↔ 𝑦 ∈ { ( 𝐹 ‘ 𝑋 ) } ) )
97 96 eqrdv ⊢ ( 𝜑 → ( 𝐹 “ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) = { ( 𝐹 ‘ 𝑋 ) } )
98 97 unieqd ⊢ ( 𝜑 → ∪ ( 𝐹 “ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) = ∪ { ( 𝐹 ‘ 𝑋 ) } )
99 fvex ⊢ ( 𝐹 ‘ 𝑋 ) ∈ V
100 99 unisn ⊢ ∪ { ( 𝐹 ‘ 𝑋 ) } = ( 𝐹 ‘ 𝑋 )
101 98 100 eqtrdi ⊢ ( 𝜑 → ∪ ( 𝐹 “ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) = ( 𝐹 ‘ 𝑋 ) )
102 23 101 eqtrd ⊢ ( 𝜑 → ( 𝐽 ‘ [ 𝑋 ] ( 𝐺 ~QG 𝑁 ) ) = ( 𝐹 ‘ 𝑋 ) )