Metamath Proof Explorer

Theorem ghmquskerlem1

Description: Lemma for ghmqusker . (Contributed by Thierry Arnoux, 14-Feb-2025)

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

Proof

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