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

Metamath Proof Explorer

Theorem rhmqusnsg

Description: The mapping J induced by a ring homomorphism F from a subring N of the quotient group Q over F 's kernel K is a ring homomorphism. (Contributed by Thierry Arnoux, 13-May-2025)

Ref Expression
Hypotheses rhmqusnsg.0 ⊢ 0 = ( 0g ‘ 𝐻 )
rhmqusnsg.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 RingHom 𝐻 ) )
rhmqusnsg.k ⊢ 𝐾 = ( ◡ 𝐹 “ { 0 } )
rhmqusnsg.q ⊢ 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝑁 ) )
rhmqusnsg.j ⊢ 𝐽 = ( 𝑞 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐹 “ 𝑞 ) )
rhmqusnsg.g ⊢ ( 𝜑 → 𝐺 ∈ CRing )
rhmqusnsg.n ⊢ ( 𝜑 → 𝑁 ⊆ 𝐾 )
rhmqusnsg.1 ⊢ ( 𝜑 → 𝑁 ∈ ( LIdeal ‘ 𝐺 ) )
Assertion rhmqusnsg ( 𝜑 → 𝐽 ∈ ( 𝑄 RingHom 𝐻 ) )

Proof

Step Hyp Ref Expression
1 rhmqusnsg.0 ⊢ 0 = ( 0g ‘ 𝐻 )
2 rhmqusnsg.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 RingHom 𝐻 ) )
3 rhmqusnsg.k ⊢ 𝐾 = ( ◡ 𝐹 “ { 0 } )
4 rhmqusnsg.q ⊢ 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝑁 ) )
5 rhmqusnsg.j ⊢ 𝐽 = ( 𝑞 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐹 “ 𝑞 ) )
6 rhmqusnsg.g ⊢ ( 𝜑 → 𝐺 ∈ CRing )
7 rhmqusnsg.n ⊢ ( 𝜑 → 𝑁 ⊆ 𝐾 )
8 rhmqusnsg.1 ⊢ ( 𝜑 → 𝑁 ∈ ( LIdeal ‘ 𝐺 ) )
9 eqid ⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
10 eqid ⊢ ( 1r ‘ 𝑄 ) = ( 1r ‘ 𝑄 )
11 eqid ⊢ ( 1r ‘ 𝐻 ) = ( 1r ‘ 𝐻 )
12 eqid ⊢ ( .r ‘ 𝑄 ) = ( .r ‘ 𝑄 )
13 eqid ⊢ ( .r ‘ 𝐻 ) = ( .r ‘ 𝐻 )
14 6 crngringd ⊢ ( 𝜑 → 𝐺 ∈ Ring )
15 eqid ⊢ ( LIdeal ‘ 𝐺 ) = ( LIdeal ‘ 𝐺 )
16 15 crng2idl ⊢ ( 𝐺 ∈ CRing → ( LIdeal ‘ 𝐺 ) = ( 2Ideal ‘ 𝐺 ) )
17 6 16 syl ⊢ ( 𝜑 → ( LIdeal ‘ 𝐺 ) = ( 2Ideal ‘ 𝐺 ) )
18 8 17 eleqtrd ⊢ ( 𝜑 → 𝑁 ∈ ( 2Ideal ‘ 𝐺 ) )
19 eqid ⊢ ( 2Ideal ‘ 𝐺 ) = ( 2Ideal ‘ 𝐺 )
20 eqid ⊢ ( 1r ‘ 𝐺 ) = ( 1r ‘ 𝐺 )
21 4 19 20 qus1 ⊢ ( ( 𝐺 ∈ Ring ∧ 𝑁 ∈ ( 2Ideal ‘ 𝐺 ) ) → ( 𝑄 ∈ Ring ∧ [ ( 1r ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑁 ) = ( 1r ‘ 𝑄 ) ) )
22 14 18 21 syl2anc ⊢ ( 𝜑 → ( 𝑄 ∈ Ring ∧ [ ( 1r ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑁 ) = ( 1r ‘ 𝑄 ) ) )
23 22 simpld ⊢ ( 𝜑 → 𝑄 ∈ Ring )
24 rhmrcl2 ⊢ ( 𝐹 ∈ ( 𝐺 RingHom 𝐻 ) → 𝐻 ∈ Ring )
25 2 24 syl ⊢ ( 𝜑 → 𝐻 ∈ Ring )
26 rhmghm ⊢ ( 𝐹 ∈ ( 𝐺 RingHom 𝐻 ) → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
27 2 26 syl ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
28 lidlnsg ⊢ ( ( 𝐺 ∈ Ring ∧ 𝑁 ∈ ( LIdeal ‘ 𝐺 ) ) → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
29 14 8 28 syl2anc ⊢ ( 𝜑 → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
30 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
31 30 20 ringidcl ⊢ ( 𝐺 ∈ Ring → ( 1r ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) )
32 14 31 syl ⊢ ( 𝜑 → ( 1r ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) )
33 1 27 3 4 5 7 29 32 ghmqusnsglem1 ⊢ ( 𝜑 → ( 𝐽 ‘ [ ( 1r ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑁 ) ) = ( 𝐹 ‘ ( 1r ‘ 𝐺 ) ) )
34 22 simprd ⊢ ( 𝜑 → [ ( 1r ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑁 ) = ( 1r ‘ 𝑄 ) )
35 34 fveq2d ⊢ ( 𝜑 → ( 𝐽 ‘ [ ( 1r ‘ 𝐺 ) ] ( 𝐺 ~QG 𝑁 ) ) = ( 𝐽 ‘ ( 1r ‘ 𝑄 ) ) )
36 20 11 rhm1 ⊢ ( 𝐹 ∈ ( 𝐺 RingHom 𝐻 ) → ( 𝐹 ‘ ( 1r ‘ 𝐺 ) ) = ( 1r ‘ 𝐻 ) )
37 2 36 syl ⊢ ( 𝜑 → ( 𝐹 ‘ ( 1r ‘ 𝐺 ) ) = ( 1r ‘ 𝐻 ) )
38 33 35 37 3eqtr3d ⊢ ( 𝜑 → ( 𝐽 ‘ ( 1r ‘ 𝑄 ) ) = ( 1r ‘ 𝐻 ) )
39 2 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝐹 ∈ ( 𝐺 RingHom 𝐻 ) )
40 4 a1i ⊢ ( 𝜑 → 𝑄 = ( 𝐺 /s ( 𝐺 ~QG 𝑁 ) ) )
41 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) )
42 ovexd ⊢ ( 𝜑 → ( 𝐺 ~QG 𝑁 ) ∈ V )
43 40 41 42 6 qusbas ⊢ ( 𝜑 → ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑁 ) ) = ( Base ‘ 𝑄 ) )
44 nsgsubg ⊢ ( 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) → 𝑁 ∈ ( SubGrp ‘ 𝐺 ) )
45 eqid ⊢ ( 𝐺 ~QG 𝑁 ) = ( 𝐺 ~QG 𝑁 )
46 30 45 eqger ⊢ ( 𝑁 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐺 ~QG 𝑁 ) Er ( Base ‘ 𝐺 ) )
47 29 44 46 3syl ⊢ ( 𝜑 → ( 𝐺 ~QG 𝑁 ) Er ( Base ‘ 𝐺 ) )
48 47 qsss ⊢ ( 𝜑 → ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑁 ) ) ⊆ 𝒫 ( Base ‘ 𝐺 ) )
49 43 48 eqsstrrd ⊢ ( 𝜑 → ( Base ‘ 𝑄 ) ⊆ 𝒫 ( Base ‘ 𝐺 ) )
50 49 sselda ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) → 𝑟 ∈ 𝒫 ( Base ‘ 𝐺 ) )
51 50 elpwid ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) → 𝑟 ⊆ ( Base ‘ 𝐺 ) )
52 51 ad5antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑟 ⊆ ( Base ‘ 𝐺 ) )
53 simp-4r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑥 ∈ 𝑟 )
54 52 53 sseldd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
55 49 sselda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) → 𝑠 ∈ 𝒫 ( Base ‘ 𝐺 ) )
56 55 elpwid ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) → 𝑠 ⊆ ( Base ‘ 𝐺 ) )
57 56 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) → 𝑠 ⊆ ( Base ‘ 𝐺 ) )
58 57 ad4antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑠 ⊆ ( Base ‘ 𝐺 ) )
59 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑦 ∈ 𝑠 )
60 58 59 sseldd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑦 ∈ ( Base ‘ 𝐺 ) )
61 eqid ⊢ ( .r ‘ 𝐺 ) = ( .r ‘ 𝐺 )
62 30 61 13 rhmmul ⊢ ( ( 𝐹 ∈ ( 𝐺 RingHom 𝐻 ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ∧ 𝑦 ∈ ( Base ‘ 𝐺 ) ) → ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝐺 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝐻 ) ( 𝐹 ‘ 𝑦 ) ) )
63 39 54 60 62 syl3anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝐺 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝐻 ) ( 𝐹 ‘ 𝑦 ) ) )
64 47 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝐺 ~QG 𝑁 ) Er ( Base ‘ 𝐺 ) )
65 simp-6r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑟 ∈ ( Base ‘ 𝑄 ) )
66 43 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑁 ) ) = ( Base ‘ 𝑄 ) )
67 65 66 eleqtrrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑟 ∈ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑁 ) ) )
68 qsel ⊢ ( ( ( 𝐺 ~QG 𝑁 ) Er ( Base ‘ 𝐺 ) ∧ 𝑟 ∈ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑁 ) ) ∧ 𝑥 ∈ 𝑟 ) → 𝑟 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) )
69 64 67 53 68 syl3anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑟 = [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) )
70 simp-5r ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑠 ∈ ( Base ‘ 𝑄 ) )
71 70 66 eleqtrrd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑠 ∈ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑁 ) ) )
72 qsel ⊢ ( ( ( 𝐺 ~QG 𝑁 ) Er ( Base ‘ 𝐺 ) ∧ 𝑠 ∈ ( ( Base ‘ 𝐺 ) / ( 𝐺 ~QG 𝑁 ) ) ∧ 𝑦 ∈ 𝑠 ) → 𝑠 = [ 𝑦 ] ( 𝐺 ~QG 𝑁 ) )
73 64 71 59 72 syl3anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑠 = [ 𝑦 ] ( 𝐺 ~QG 𝑁 ) )
74 69 73 oveq12d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝑟 ( .r ‘ 𝑄 ) 𝑠 ) = ( [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ( .r ‘ 𝑄 ) [ 𝑦 ] ( 𝐺 ~QG 𝑁 ) ) )
75 6 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝐺 ∈ CRing )
76 8 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑁 ∈ ( LIdeal ‘ 𝐺 ) )
77 4 30 61 12 75 76 54 60 qusmulcrng ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → ( [ 𝑥 ] ( 𝐺 ~QG 𝑁 ) ( .r ‘ 𝑄 ) [ 𝑦 ] ( 𝐺 ~QG 𝑁 ) ) = [ ( 𝑥 ( .r ‘ 𝐺 ) 𝑦 ) ] ( 𝐺 ~QG 𝑁 ) )
78 74 77 eqtr2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → [ ( 𝑥 ( .r ‘ 𝐺 ) 𝑦 ) ] ( 𝐺 ~QG 𝑁 ) = ( 𝑟 ( .r ‘ 𝑄 ) 𝑠 ) )
79 78 fveq2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝐽 ‘ [ ( 𝑥 ( .r ‘ 𝐺 ) 𝑦 ) ] ( 𝐺 ~QG 𝑁 ) ) = ( 𝐽 ‘ ( 𝑟 ( .r ‘ 𝑄 ) 𝑠 ) ) )
80 39 26 syl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
81 7 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑁 ⊆ 𝐾 )
82 29 ad6antr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
83 rhmrcl1 ⊢ ( 𝐹 ∈ ( 𝐺 RingHom 𝐻 ) → 𝐺 ∈ Ring )
84 39 83 syl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝐺 ∈ Ring )
85 30 61 84 54 60 ringcld ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝑥 ( .r ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
86 1 80 3 4 5 81 82 85 ghmqusnsglem1 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝐽 ‘ [ ( 𝑥 ( .r ‘ 𝐺 ) 𝑦 ) ] ( 𝐺 ~QG 𝑁 ) ) = ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝐺 ) 𝑦 ) ) )
87 79 86 eqtr3d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝐽 ‘ ( 𝑟 ( .r ‘ 𝑄 ) 𝑠 ) ) = ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝐺 ) 𝑦 ) ) )
88 simpllr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) )
89 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) )
90 88 89 oveq12d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → ( ( 𝐽 ‘ 𝑟 ) ( .r ‘ 𝐻 ) ( 𝐽 ‘ 𝑠 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝐻 ) ( 𝐹 ‘ 𝑦 ) ) )
91 63 87 90 3eqtr4d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑦 ∈ 𝑠 ) ∧ ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝐽 ‘ ( 𝑟 ( .r ‘ 𝑄 ) 𝑠 ) ) = ( ( 𝐽 ‘ 𝑟 ) ( .r ‘ 𝐻 ) ( 𝐽 ‘ 𝑠 ) ) )
92 27 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
93 7 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → 𝑁 ⊆ 𝐾 )
94 29 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
95 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → 𝑠 ∈ ( Base ‘ 𝑄 ) )
96 1 92 3 4 5 93 94 95 ghmqusnsglem2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → ∃ 𝑦 ∈ 𝑠 ( 𝐽 ‘ 𝑠 ) = ( 𝐹 ‘ 𝑦 ) )
97 91 96 r19.29a ⊢ ( ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑥 ∈ 𝑟 ) ∧ ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) ) → ( 𝐽 ‘ ( 𝑟 ( .r ‘ 𝑄 ) 𝑠 ) ) = ( ( 𝐽 ‘ 𝑟 ) ( .r ‘ 𝐻 ) ( 𝐽 ‘ 𝑠 ) ) )
98 27 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
99 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) → 𝑁 ⊆ 𝐾 )
100 29 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) → 𝑁 ∈ ( NrmSGrp ‘ 𝐺 ) )
101 simplr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) → 𝑟 ∈ ( Base ‘ 𝑄 ) )
102 1 98 3 4 5 99 100 101 ghmqusnsglem2 ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) → ∃ 𝑥 ∈ 𝑟 ( 𝐽 ‘ 𝑟 ) = ( 𝐹 ‘ 𝑥 ) )
103 97 102 r19.29a ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( Base ‘ 𝑄 ) ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) → ( 𝐽 ‘ ( 𝑟 ( .r ‘ 𝑄 ) 𝑠 ) ) = ( ( 𝐽 ‘ 𝑟 ) ( .r ‘ 𝐻 ) ( 𝐽 ‘ 𝑠 ) ) )
104 103 anasss ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ( Base ‘ 𝑄 ) ∧ 𝑠 ∈ ( Base ‘ 𝑄 ) ) ) → ( 𝐽 ‘ ( 𝑟 ( .r ‘ 𝑄 ) 𝑠 ) ) = ( ( 𝐽 ‘ 𝑟 ) ( .r ‘ 𝐻 ) ( 𝐽 ‘ 𝑠 ) ) )
105 1 27 3 4 5 7 29 ghmqusnsg ⊢ ( 𝜑 → 𝐽 ∈ ( 𝑄 GrpHom 𝐻 ) )
106 9 10 11 12 13 23 25 38 104 105 isrhm2d ⊢ ( 𝜑 → 𝐽 ∈ ( 𝑄 RingHom 𝐻 ) )