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