Metamath Proof Explorer

Theorem rhmqusspan

Description: Ring homomorphism out of a quotient given an ideal spanned by a singleton. (Contributed by metakunt, 7-Jun-2025)

Ref Expression
Hypotheses rhmqusspan.1 ⊢ 0 = ( 0g ‘ 𝐻 )
rhmqusspan.2 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 RingHom 𝐻 ) )
rhmqusspan.3 ⊢ 𝐾 = ( ◡ 𝐹 “ { 0 } )
rhmqusspan.4 ⊢ 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝑁 ) )
rhmqusspan.5 ⊢ 𝐽 = ( 𝑞 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐹 “ 𝑞 ) )
rhmqusspan.6 ⊢ ( 𝜑 → 𝐺 ∈ CRing )
rhmqusspan.7 ⊢ 𝑁 = ( ( RSpan ‘ 𝐺 ) ‘ { 𝑋 } )
rhmqusspan.8 ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐺 ) )
rhmqusspan.9 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = 0 )
Assertion rhmqusspan ( 𝜑 → ( 𝐽 ∈ ( 𝑄 RingHom 𝐻 ) ∧ ∀ 𝑔 ∈ ( Base ‘ 𝐺 ) ( 𝐽 ‘ [ 𝑔 ] ( 𝐺 ~QG 𝑁 ) ) = ( 𝐹 ‘ 𝑔 ) ) )

Proof

Step Hyp Ref Expression
1 rhmqusspan.1 ⊢ 0 = ( 0g ‘ 𝐻 )
2 rhmqusspan.2 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 RingHom 𝐻 ) )
3 rhmqusspan.3 ⊢ 𝐾 = ( ◡ 𝐹 “ { 0 } )
4 rhmqusspan.4 ⊢ 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝑁 ) )
5 rhmqusspan.5 ⊢ 𝐽 = ( 𝑞 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐹 “ 𝑞 ) )
6 rhmqusspan.6 ⊢ ( 𝜑 → 𝐺 ∈ CRing )
7 rhmqusspan.7 ⊢ 𝑁 = ( ( RSpan ‘ 𝐺 ) ‘ { 𝑋 } )
8 rhmqusspan.8 ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐺 ) )
9 rhmqusspan.9 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = 0 )
10 6 crngringd ⊢ ( 𝜑 → 𝐺 ∈ Ring )
11 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
12 eqid ⊢ ( RSpan ‘ 𝐺 ) = ( RSpan ‘ 𝐺 )
13 eqid ⊢ ( ∥r ‘ 𝐺 ) = ( ∥r ‘ 𝐺 )
14 11 12 13 rspsn ⊢ ( ( 𝐺 ∈ Ring ∧ 𝑋 ∈ ( Base ‘ 𝐺 ) ) → ( ( RSpan ‘ 𝐺 ) ‘ { 𝑋 } ) = { 𝑦 ∣ 𝑋 ( ∥r ‘ 𝐺 ) 𝑦 } )
15 10 8 14 syl2anc ⊢ ( 𝜑 → ( ( RSpan ‘ 𝐺 ) ‘ { 𝑋 } ) = { 𝑦 ∣ 𝑋 ( ∥r ‘ 𝐺 ) 𝑦 } )
16 15 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( RSpan ‘ 𝐺 ) ‘ { 𝑋 } ) ↔ 𝑥 ∈ { 𝑦 ∣ 𝑋 ( ∥r ‘ 𝐺 ) 𝑦 } ) )
17 16 biimpd ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( RSpan ‘ 𝐺 ) ‘ { 𝑋 } ) → 𝑥 ∈ { 𝑦 ∣ 𝑋 ( ∥r ‘ 𝐺 ) 𝑦 } ) )
18 17 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( RSpan ‘ 𝐺 ) ‘ { 𝑋 } ) ) → 𝑥 ∈ { 𝑦 ∣ 𝑋 ( ∥r ‘ 𝐺 ) 𝑦 } )
19 vex ⊢ 𝑥 ∈ V
20 19 a1i ⊢ ( 𝜑 → 𝑥 ∈ V )
21 breq2 ⊢ ( 𝑦 = 𝑥 → ( 𝑋 ( ∥r ‘ 𝐺 ) 𝑦 ↔ 𝑋 ( ∥r ‘ 𝐺 ) 𝑥 ) )
22 21 elabg ⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ { 𝑦 ∣ 𝑋 ( ∥r ‘ 𝐺 ) 𝑦 } ↔ 𝑋 ( ∥r ‘ 𝐺 ) 𝑥 ) )
23 22 biimpd ⊢ ( 𝑥 ∈ V → ( 𝑥 ∈ { 𝑦 ∣ 𝑋 ( ∥r ‘ 𝐺 ) 𝑦 } → 𝑋 ( ∥r ‘ 𝐺 ) 𝑥 ) )
24 20 23 syl ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑦 ∣ 𝑋 ( ∥r ‘ 𝐺 ) 𝑦 } → 𝑋 ( ∥r ‘ 𝐺 ) 𝑥 ) )
25 24 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∣ 𝑋 ( ∥r ‘ 𝐺 ) 𝑦 } ) → 𝑋 ( ∥r ‘ 𝐺 ) 𝑥 )
26 eqid ⊢ ( .r ‘ 𝐺 ) = ( .r ‘ 𝐺 )
27 11 13 26 dvdsr ⊢ ( 𝑋 ( ∥r ‘ 𝐺 ) 𝑥 ↔ ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 ) )
28 27 biimpi ⊢ ( 𝑋 ( ∥r ‘ 𝐺 ) 𝑥 → ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 ) )
29 28 adantl ⊢ ( ( 𝜑 ∧ 𝑋 ( ∥r ‘ 𝐺 ) 𝑥 ) → ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 ) )
30 fveq2 ⊢ ( ( 𝑧 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 → ( 𝐹 ‘ ( 𝑧 ( .r ‘ 𝐺 ) 𝑋 ) ) = ( 𝐹 ‘ 𝑥 ) )
31 30 eqcomd ⊢ ( ( 𝑧 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑧 ( .r ‘ 𝐺 ) 𝑋 ) ) )
32 31 adantl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ∧ ( 𝑧 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑧 ( .r ‘ 𝐺 ) 𝑋 ) ) )
33 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) → 𝐹 ∈ ( 𝐺 RingHom 𝐻 ) )
34 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) → 𝑧 ∈ ( Base ‘ 𝐺 ) )
35 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) → 𝑋 ∈ ( Base ‘ 𝐺 ) )
36 eqid ⊢ ( .r ‘ 𝐻 ) = ( .r ‘ 𝐻 )
37 11 26 36 rhmmul ⊢ ( ( 𝐹 ∈ ( 𝐺 RingHom 𝐻 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ∧ 𝑋 ∈ ( Base ‘ 𝐺 ) ) → ( 𝐹 ‘ ( 𝑧 ( .r ‘ 𝐺 ) 𝑋 ) ) = ( ( 𝐹 ‘ 𝑧 ) ( .r ‘ 𝐻 ) ( 𝐹 ‘ 𝑋 ) ) )
38 33 34 35 37 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) → ( 𝐹 ‘ ( 𝑧 ( .r ‘ 𝐺 ) 𝑋 ) ) = ( ( 𝐹 ‘ 𝑧 ) ( .r ‘ 𝐻 ) ( 𝐹 ‘ 𝑋 ) ) )
39 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) → ( 𝐹 ‘ 𝑋 ) = 0 )
40 39 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝐹 ‘ 𝑧 ) ( .r ‘ 𝐻 ) ( 𝐹 ‘ 𝑋 ) ) = ( ( 𝐹 ‘ 𝑧 ) ( .r ‘ 𝐻 ) 0 ) )
41 rhmrcl2 ⊢ ( 𝐹 ∈ ( 𝐺 RingHom 𝐻 ) → 𝐻 ∈ Ring )
42 ringsrg ⊢ ( 𝐻 ∈ Ring → 𝐻 ∈ SRing )
43 33 41 42 3syl ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) → 𝐻 ∈ SRing )
44 eqid ⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
45 11 44 rhmf ⊢ ( 𝐹 ∈ ( 𝐺 RingHom 𝐻 ) → 𝐹 : ( Base ‘ 𝐺 ) ⟶ ( Base ‘ 𝐻 ) )
46 2 45 syl ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝐺 ) ⟶ ( Base ‘ 𝐻 ) )
47 46 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 ) ) → 𝐹 : ( Base ‘ 𝐺 ) ⟶ ( Base ‘ 𝐻 ) )
48 47 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ( Base ‘ 𝐻 ) )
49 44 36 1 srgrz ⊢ ( ( 𝐻 ∈ SRing ∧ ( 𝐹 ‘ 𝑧 ) ∈ ( Base ‘ 𝐻 ) ) → ( ( 𝐹 ‘ 𝑧 ) ( .r ‘ 𝐻 ) 0 ) = 0 )
50 43 48 49 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝐹 ‘ 𝑧 ) ( .r ‘ 𝐻 ) 0 ) = 0 )
51 40 50 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) → ( ( 𝐹 ‘ 𝑧 ) ( .r ‘ 𝐻 ) ( 𝐹 ‘ 𝑋 ) ) = 0 )
52 38 51 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) → ( 𝐹 ‘ ( 𝑧 ( .r ‘ 𝐺 ) 𝑋 ) ) = 0 )
53 52 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ∧ ( 𝑧 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 ) → ( 𝐹 ‘ ( 𝑧 ( .r ‘ 𝐺 ) 𝑋 ) ) = 0 )
54 32 53 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 ) ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ) ∧ ( 𝑧 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 ) → ( 𝐹 ‘ 𝑥 ) = 0 )
55 nfv ⊢ Ⅎ 𝑧 ( 𝑦 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥
56 nfv ⊢ Ⅎ 𝑦 ( 𝑧 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥
57 oveq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 ( .r ‘ 𝐺 ) 𝑋 ) = ( 𝑧 ( .r ‘ 𝐺 ) 𝑋 ) )
58 57 eqeq1d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑦 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 ↔ ( 𝑧 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 ) )
59 55 56 58 cbvrexw ⊢ ( ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 ↔ ∃ 𝑧 ∈ ( Base ‘ 𝐺 ) ( 𝑧 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 )
60 59 biimpi ⊢ ( ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 → ∃ 𝑧 ∈ ( Base ‘ 𝐺 ) ( 𝑧 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 )
61 60 adantl ⊢ ( ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 ) → ∃ 𝑧 ∈ ( Base ‘ 𝐺 ) ( 𝑧 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 )
62 61 adantl ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 ) ) → ∃ 𝑧 ∈ ( Base ‘ 𝐺 ) ( 𝑧 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 )
63 54 62 r19.29a ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 ) ) → ( 𝐹 ‘ 𝑥 ) = 0 )
64 63 ex ⊢ ( 𝜑 → ( ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 ) → ( 𝐹 ‘ 𝑥 ) = 0 ) )
65 64 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ( ∥r ‘ 𝐺 ) 𝑥 ) → ( ( 𝑋 ∈ ( Base ‘ 𝐺 ) ∧ ∃ 𝑦 ∈ ( Base ‘ 𝐺 ) ( 𝑦 ( .r ‘ 𝐺 ) 𝑋 ) = 𝑥 ) → ( 𝐹 ‘ 𝑥 ) = 0 ) )
66 29 65 mpd ⊢ ( ( 𝜑 ∧ 𝑋 ( ∥r ‘ 𝐺 ) 𝑥 ) → ( 𝐹 ‘ 𝑥 ) = 0 )
67 66 ex ⊢ ( 𝜑 → ( 𝑋 ( ∥r ‘ 𝐺 ) 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) )
68 67 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∣ 𝑋 ( ∥r ‘ 𝐺 ) 𝑦 } ) → ( 𝑋 ( ∥r ‘ 𝐺 ) 𝑥 → ( 𝐹 ‘ 𝑥 ) = 0 ) )
69 25 68 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ { 𝑦 ∣ 𝑋 ( ∥r ‘ 𝐺 ) 𝑦 } ) → ( 𝐹 ‘ 𝑥 ) = 0 )
70 69 ex ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑦 ∣ 𝑋 ( ∥r ‘ 𝐺 ) 𝑦 } → ( 𝐹 ‘ 𝑥 ) = 0 ) )
71 70 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( RSpan ‘ 𝐺 ) ‘ { 𝑋 } ) ) → ( 𝑥 ∈ { 𝑦 ∣ 𝑋 ( ∥r ‘ 𝐺 ) 𝑦 } → ( 𝐹 ‘ 𝑥 ) = 0 ) )
72 18 71 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( RSpan ‘ 𝐺 ) ‘ { 𝑋 } ) ) → ( 𝐹 ‘ 𝑥 ) = 0 )
73 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( RSpan ‘ 𝐺 ) ‘ { 𝑋 } ) ) → ( 𝐹 ‘ 𝑥 ) ∈ V )
74 elsng ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ V → ( ( 𝐹 ‘ 𝑥 ) ∈ { 0 } ↔ ( 𝐹 ‘ 𝑥 ) = 0 ) )
75 73 74 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( RSpan ‘ 𝐺 ) ‘ { 𝑋 } ) ) → ( ( 𝐹 ‘ 𝑥 ) ∈ { 0 } ↔ ( 𝐹 ‘ 𝑥 ) = 0 ) )
76 72 75 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( RSpan ‘ 𝐺 ) ‘ { 𝑋 } ) ) → ( 𝐹 ‘ 𝑥 ) ∈ { 0 } )
77 46 ffund ⊢ ( 𝜑 → Fun 𝐹 )
78 77 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( RSpan ‘ 𝐺 ) ‘ { 𝑋 } ) ) → Fun 𝐹 )
79 eqid ⊢ ( LIdeal ‘ 𝐺 ) = ( LIdeal ‘ 𝐺 )
80 79 11 lidl1 ⊢ ( 𝐺 ∈ Ring → ( Base ‘ 𝐺 ) ∈ ( LIdeal ‘ 𝐺 ) )
81 10 80 syl ⊢ ( 𝜑 → ( Base ‘ 𝐺 ) ∈ ( LIdeal ‘ 𝐺 ) )
82 8 snssd ⊢ ( 𝜑 → { 𝑋 } ⊆ ( Base ‘ 𝐺 ) )
83 12 79 rspssp ⊢ ( ( 𝐺 ∈ Ring ∧ ( Base ‘ 𝐺 ) ∈ ( LIdeal ‘ 𝐺 ) ∧ { 𝑋 } ⊆ ( Base ‘ 𝐺 ) ) → ( ( RSpan ‘ 𝐺 ) ‘ { 𝑋 } ) ⊆ ( Base ‘ 𝐺 ) )
84 10 81 82 83 syl3anc ⊢ ( 𝜑 → ( ( RSpan ‘ 𝐺 ) ‘ { 𝑋 } ) ⊆ ( Base ‘ 𝐺 ) )
85 84 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( RSpan ‘ 𝐺 ) ‘ { 𝑋 } ) ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
86 fdm ⊢ ( 𝐹 : ( Base ‘ 𝐺 ) ⟶ ( Base ‘ 𝐻 ) → dom 𝐹 = ( Base ‘ 𝐺 ) )
87 46 86 syl ⊢ ( 𝜑 → dom 𝐹 = ( Base ‘ 𝐺 ) )
88 87 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( RSpan ‘ 𝐺 ) ‘ { 𝑋 } ) ) → dom 𝐹 = ( Base ‘ 𝐺 ) )
89 85 88 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( RSpan ‘ 𝐺 ) ‘ { 𝑋 } ) ) → 𝑥 ∈ dom 𝐹 )
90 fvimacnv ⊢ ( ( Fun 𝐹 ∧ 𝑥 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ { 0 } ↔ 𝑥 ∈ ( ◡ 𝐹 “ { 0 } ) ) )
91 78 89 90 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( RSpan ‘ 𝐺 ) ‘ { 𝑋 } ) ) → ( ( 𝐹 ‘ 𝑥 ) ∈ { 0 } ↔ 𝑥 ∈ ( ◡ 𝐹 “ { 0 } ) ) )
92 76 91 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( RSpan ‘ 𝐺 ) ‘ { 𝑋 } ) ) → 𝑥 ∈ ( ◡ 𝐹 “ { 0 } ) )
93 92 ex ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( RSpan ‘ 𝐺 ) ‘ { 𝑋 } ) → 𝑥 ∈ ( ◡ 𝐹 “ { 0 } ) ) )
94 93 ssrdv ⊢ ( 𝜑 → ( ( RSpan ‘ 𝐺 ) ‘ { 𝑋 } ) ⊆ ( ◡ 𝐹 “ { 0 } ) )
95 3 eqcomi ⊢ ( ◡ 𝐹 “ { 0 } ) = 𝐾
96 94 95 sseqtrdi ⊢ ( 𝜑 → ( ( RSpan ‘ 𝐺 ) ‘ { 𝑋 } ) ⊆ 𝐾 )
97 7 96 eqsstrid ⊢ ( 𝜑 → 𝑁 ⊆ 𝐾 )
98 12 11 79 rspcl ⊢ ( ( 𝐺 ∈ Ring ∧ { 𝑋 } ⊆ ( Base ‘ 𝐺 ) ) → ( ( RSpan ‘ 𝐺 ) ‘ { 𝑋 } ) ∈ ( LIdeal ‘ 𝐺 ) )
99 10 82 98 syl2anc ⊢ ( 𝜑 → ( ( RSpan ‘ 𝐺 ) ‘ { 𝑋 } ) ∈ ( LIdeal ‘ 𝐺 ) )
100 7 99 eqeltrid ⊢ ( 𝜑 → 𝑁 ∈ ( LIdeal ‘ 𝐺 ) )
101 1 2 3 4 5 6 97 100 rhmqusnsg ⊢ ( 𝜑 → 𝐽 ∈ ( 𝑄 RingHom 𝐻 ) )
102 2 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝐺 ) ) → 𝐹 ∈ ( 𝐺 RingHom 𝐻 ) )
103 rhmghm ⊢ ( 𝐹 ∈ ( 𝐺 RingHom 𝐻 ) → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
104 102 103 syl ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝐺 ) ) → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
105 97 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝐺 ) ) → 𝑁 ⊆ 𝐾 )
106 lidlnsg ⊢ ( ( 𝐺 ∈ Ring ∧ 𝑁 ∈ ( LIdeal ‘ 𝐺 ) ) → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
107 10 100 106 syl2anc ⊢ ( 𝜑 → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
108 107 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝐺 ) ) → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
109 simpr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝐺 ) ) → 𝑔 ∈ ( Base ‘ 𝐺 ) )
110 1 104 3 4 5 105 108 109 ghmqusnsglem1 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ 𝐺 ) ) → ( 𝐽 ‘ [ 𝑔 ] ( 𝐺 ~QG 𝑁 ) ) = ( 𝐹 ‘ 𝑔 ) )
111 110 ralrimiva ⊢ ( 𝜑 → ∀ 𝑔 ∈ ( Base ‘ 𝐺 ) ( 𝐽 ‘ [ 𝑔 ] ( 𝐺 ~QG 𝑁 ) ) = ( 𝐹 ‘ 𝑔 ) )
112 101 111 jca ⊢ ( 𝜑 → ( 𝐽 ∈ ( 𝑄 RingHom 𝐻 ) ∧ ∀ 𝑔 ∈ ( Base ‘ 𝐺 ) ( 𝐽 ‘ [ 𝑔 ] ( 𝐺 ~QG 𝑁 ) ) = ( 𝐹 ‘ 𝑔 ) ) )