Metamath Proof Explorer

Theorem rhmquskerlem

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

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

Proof

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