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