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