Step | Hyp | Ref
| Expression |
1 | | eqid 2728 |
. 2
⊢
(Base‘𝑄) =
(Base‘𝑄) |
2 | | eqid 2728 |
. 2
⊢
(1r‘𝑄) = (1r‘𝑄) |
3 | | eqid 2728 |
. 2
⊢
(1r‘𝐻) = (1r‘𝐻) |
4 | | eqid 2728 |
. 2
⊢
(.r‘𝑄) = (.r‘𝑄) |
5 | | eqid 2728 |
. 2
⊢
(.r‘𝐻) = (.r‘𝐻) |
6 | | rhmqusker.f |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (𝐺 RingHom 𝐻)) |
7 | | rhmrcl1 20414 |
. . . . 5
⊢ (𝐹 ∈ (𝐺 RingHom 𝐻) → 𝐺 ∈ Ring) |
8 | 6, 7 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ Ring) |
9 | | rhmqusker.k |
. . . . . 6
⊢ 𝐾 = (◡𝐹 “ { 0 }) |
10 | | eqid 2728 |
. . . . . . . 8
⊢
(LIdeal‘𝐺) =
(LIdeal‘𝐺) |
11 | | rhmqusker.1 |
. . . . . . . 8
⊢ 0 =
(0g‘𝐻) |
12 | 10, 11 | kerlidl 33134 |
. . . . . . 7
⊢ (𝐹 ∈ (𝐺 RingHom 𝐻) → (◡𝐹 “ { 0 }) ∈
(LIdeal‘𝐺)) |
13 | 6, 12 | syl 17 |
. . . . . 6
⊢ (𝜑 → (◡𝐹 “ { 0 }) ∈
(LIdeal‘𝐺)) |
14 | 9, 13 | eqeltrid 2833 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ (LIdeal‘𝐺)) |
15 | | rhmquskerlem.2 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ CRing) |
16 | 10 | crng2idl 21172 |
. . . . . 6
⊢ (𝐺 ∈ CRing →
(LIdeal‘𝐺) =
(2Ideal‘𝐺)) |
17 | 15, 16 | syl 17 |
. . . . 5
⊢ (𝜑 → (LIdeal‘𝐺) = (2Ideal‘𝐺)) |
18 | 14, 17 | eleqtrd 2831 |
. . . 4
⊢ (𝜑 → 𝐾 ∈ (2Ideal‘𝐺)) |
19 | | rhmqusker.q |
. . . . 5
⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾)) |
20 | | eqid 2728 |
. . . . 5
⊢
(2Ideal‘𝐺) =
(2Ideal‘𝐺) |
21 | | eqid 2728 |
. . . . 5
⊢
(1r‘𝐺) = (1r‘𝐺) |
22 | 19, 20, 21 | qus1 21167 |
. . . 4
⊢ ((𝐺 ∈ Ring ∧ 𝐾 ∈ (2Ideal‘𝐺)) → (𝑄 ∈ Ring ∧
[(1r‘𝐺)](𝐺 ~QG 𝐾) = (1r‘𝑄))) |
23 | 8, 18, 22 | syl2anc 583 |
. . 3
⊢ (𝜑 → (𝑄 ∈ Ring ∧
[(1r‘𝐺)](𝐺 ~QG 𝐾) = (1r‘𝑄))) |
24 | 23 | simpld 494 |
. 2
⊢ (𝜑 → 𝑄 ∈ Ring) |
25 | | rhmrcl2 20415 |
. . 3
⊢ (𝐹 ∈ (𝐺 RingHom 𝐻) → 𝐻 ∈ Ring) |
26 | 6, 25 | syl 17 |
. 2
⊢ (𝜑 → 𝐻 ∈ Ring) |
27 | | rhmghm 20422 |
. . . . 5
⊢ (𝐹 ∈ (𝐺 RingHom 𝐻) → 𝐹 ∈ (𝐺 GrpHom 𝐻)) |
28 | 6, 27 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (𝐺 GrpHom 𝐻)) |
29 | | rhmquskerlem.j |
. . . 4
⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪
(𝐹 “ 𝑞)) |
30 | | eqid 2728 |
. . . . . 6
⊢
(Base‘𝐺) =
(Base‘𝐺) |
31 | 30, 21 | ringidcl 20201 |
. . . . 5
⊢ (𝐺 ∈ Ring →
(1r‘𝐺)
∈ (Base‘𝐺)) |
32 | 8, 31 | syl 17 |
. . . 4
⊢ (𝜑 → (1r‘𝐺) ∈ (Base‘𝐺)) |
33 | 11, 28, 9, 19, 29, 32 | ghmquskerlem1 19233 |
. . 3
⊢ (𝜑 → (𝐽‘[(1r‘𝐺)](𝐺 ~QG 𝐾)) = (𝐹‘(1r‘𝐺))) |
34 | 23 | simprd 495 |
. . . 4
⊢ (𝜑 →
[(1r‘𝐺)](𝐺 ~QG 𝐾) = (1r‘𝑄)) |
35 | 34 | fveq2d 6901 |
. . 3
⊢ (𝜑 → (𝐽‘[(1r‘𝐺)](𝐺 ~QG 𝐾)) = (𝐽‘(1r‘𝑄))) |
36 | 21, 3 | rhm1 20427 |
. . . 4
⊢ (𝐹 ∈ (𝐺 RingHom 𝐻) → (𝐹‘(1r‘𝐺)) = (1r‘𝐻)) |
37 | 6, 36 | syl 17 |
. . 3
⊢ (𝜑 → (𝐹‘(1r‘𝐺)) = (1r‘𝐻)) |
38 | 33, 35, 37 | 3eqtr3d 2776 |
. 2
⊢ (𝜑 → (𝐽‘(1r‘𝑄)) = (1r‘𝐻)) |
39 | 6 | ad6antr 735 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → 𝐹 ∈ (𝐺 RingHom 𝐻)) |
40 | 19 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾))) |
41 | | eqidd 2729 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (Base‘𝐺) = (Base‘𝐺)) |
42 | | ovexd 7455 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐺 ~QG 𝐾) ∈ V) |
43 | 40, 41, 42, 15 | qusbas 17526 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((Base‘𝐺) / (𝐺 ~QG 𝐾)) = (Base‘𝑄)) |
44 | 11 | ghmker 19195 |
. . . . . . . . . . . . . . . 16
⊢ (𝐹 ∈ (𝐺 GrpHom 𝐻) → (◡𝐹 “ { 0 }) ∈
(NrmSGrp‘𝐺)) |
45 | 28, 44 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (◡𝐹 “ { 0 }) ∈
(NrmSGrp‘𝐺)) |
46 | 9, 45 | eqeltrid 2833 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐾 ∈ (NrmSGrp‘𝐺)) |
47 | | nsgsubg 19112 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ (NrmSGrp‘𝐺) → 𝐾 ∈ (SubGrp‘𝐺)) |
48 | | eqid 2728 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ~QG 𝐾) = (𝐺 ~QG 𝐾) |
49 | 30, 48 | eqger 19132 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ (SubGrp‘𝐺) → (𝐺 ~QG 𝐾) Er (Base‘𝐺)) |
50 | 46, 47, 49 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐺 ~QG 𝐾) Er (Base‘𝐺)) |
51 | 50 | qsss 8796 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((Base‘𝐺) / (𝐺 ~QG 𝐾)) ⊆ 𝒫 (Base‘𝐺)) |
52 | 43, 51 | eqsstrrd 4019 |
. . . . . . . . . . 11
⊢ (𝜑 → (Base‘𝑄) ⊆ 𝒫
(Base‘𝐺)) |
53 | 52 | sselda 3980 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) → 𝑟 ∈ 𝒫 (Base‘𝐺)) |
54 | 53 | elpwid 4612 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) → 𝑟 ⊆ (Base‘𝐺)) |
55 | 54 | ad5antr 733 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → 𝑟 ⊆ (Base‘𝐺)) |
56 | | simp-4r 783 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → 𝑥 ∈ 𝑟) |
57 | 55, 56 | sseldd 3981 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → 𝑥 ∈ (Base‘𝐺)) |
58 | 52 | sselda 3980 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ (Base‘𝑄)) → 𝑠 ∈ 𝒫 (Base‘𝐺)) |
59 | 58 | elpwid 4612 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ (Base‘𝑄)) → 𝑠 ⊆ (Base‘𝐺)) |
60 | 59 | adantlr 714 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) → 𝑠 ⊆ (Base‘𝐺)) |
61 | 60 | ad4antr 731 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → 𝑠 ⊆ (Base‘𝐺)) |
62 | | simplr 768 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → 𝑦 ∈ 𝑠) |
63 | 61, 62 | sseldd 3981 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → 𝑦 ∈ (Base‘𝐺)) |
64 | | eqid 2728 |
. . . . . . . 8
⊢
(.r‘𝐺) = (.r‘𝐺) |
65 | 30, 64, 5 | rhmmul 20424 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝐺 RingHom 𝐻) ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝐹‘(𝑥(.r‘𝐺)𝑦)) = ((𝐹‘𝑥)(.r‘𝐻)(𝐹‘𝑦))) |
66 | 39, 57, 63, 65 | syl3anc 1369 |
. . . . . 6
⊢
(((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → (𝐹‘(𝑥(.r‘𝐺)𝑦)) = ((𝐹‘𝑥)(.r‘𝐻)(𝐹‘𝑦))) |
67 | 50 | ad6antr 735 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → (𝐺 ~QG 𝐾) Er (Base‘𝐺)) |
68 | | simp-6r 787 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → 𝑟 ∈ (Base‘𝑄)) |
69 | 43 | ad6antr 735 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → ((Base‘𝐺) / (𝐺 ~QG 𝐾)) = (Base‘𝑄)) |
70 | 68, 69 | eleqtrrd 2832 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → 𝑟 ∈ ((Base‘𝐺) / (𝐺 ~QG 𝐾))) |
71 | | qsel 8814 |
. . . . . . . . . . 11
⊢ (((𝐺 ~QG 𝐾) Er (Base‘𝐺) ∧ 𝑟 ∈ ((Base‘𝐺) / (𝐺 ~QG 𝐾)) ∧ 𝑥 ∈ 𝑟) → 𝑟 = [𝑥](𝐺 ~QG 𝐾)) |
72 | 67, 70, 56, 71 | syl3anc 1369 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → 𝑟 = [𝑥](𝐺 ~QG 𝐾)) |
73 | | simp-5r 785 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → 𝑠 ∈ (Base‘𝑄)) |
74 | 73, 69 | eleqtrrd 2832 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → 𝑠 ∈ ((Base‘𝐺) / (𝐺 ~QG 𝐾))) |
75 | | qsel 8814 |
. . . . . . . . . . 11
⊢ (((𝐺 ~QG 𝐾) Er (Base‘𝐺) ∧ 𝑠 ∈ ((Base‘𝐺) / (𝐺 ~QG 𝐾)) ∧ 𝑦 ∈ 𝑠) → 𝑠 = [𝑦](𝐺 ~QG 𝐾)) |
76 | 67, 74, 62, 75 | syl3anc 1369 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → 𝑠 = [𝑦](𝐺 ~QG 𝐾)) |
77 | 72, 76 | oveq12d 7438 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → (𝑟(.r‘𝑄)𝑠) = ([𝑥](𝐺 ~QG 𝐾)(.r‘𝑄)[𝑦](𝐺 ~QG 𝐾))) |
78 | 15 | ad6antr 735 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → 𝐺 ∈ CRing) |
79 | 14 | ad6antr 735 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → 𝐾 ∈ (LIdeal‘𝐺)) |
80 | 19, 30, 64, 4, 78, 79, 57, 63 | qusmul 33114 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → ([𝑥](𝐺 ~QG 𝐾)(.r‘𝑄)[𝑦](𝐺 ~QG 𝐾)) = [(𝑥(.r‘𝐺)𝑦)](𝐺 ~QG 𝐾)) |
81 | 77, 80 | eqtr2d 2769 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → [(𝑥(.r‘𝐺)𝑦)](𝐺 ~QG 𝐾) = (𝑟(.r‘𝑄)𝑠)) |
82 | 81 | fveq2d 6901 |
. . . . . . 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 20198 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → (𝑥(.r‘𝐺)𝑦) ∈ (Base‘𝐺)) |
86 | 11, 83, 9, 19, 29, 85 | ghmquskerlem1 19233 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → (𝐽‘[(𝑥(.r‘𝐺)𝑦)](𝐺 ~QG 𝐾)) = (𝐹‘(𝑥(.r‘𝐺)𝑦))) |
87 | 82, 86 | eqtr3d 2770 |
. . . . . 6
⊢
(((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → (𝐽‘(𝑟(.r‘𝑄)𝑠)) = (𝐹‘(𝑥(.r‘𝐺)𝑦))) |
88 | | simpllr 775 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → (𝐽‘𝑟) = (𝐹‘𝑥)) |
89 | | simpr 484 |
. . . . . . 7
⊢
(((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → (𝐽‘𝑠) = (𝐹‘𝑦)) |
90 | 88, 89 | oveq12d 7438 |
. . . . . 6
⊢
(((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → ((𝐽‘𝑟)(.r‘𝐻)(𝐽‘𝑠)) = ((𝐹‘𝑥)(.r‘𝐻)(𝐹‘𝑦))) |
91 | 66, 87, 90 | 3eqtr4d 2778 |
. . . . 5
⊢
(((((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) ∧ 𝑦 ∈ 𝑠) ∧ (𝐽‘𝑠) = (𝐹‘𝑦)) → (𝐽‘(𝑟(.r‘𝑄)𝑠)) = ((𝐽‘𝑟)(.r‘𝐻)(𝐽‘𝑠))) |
92 | 28 | ad4antr 731 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) → 𝐹 ∈ (𝐺 GrpHom 𝐻)) |
93 | | simpllr 775 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) → 𝑠 ∈ (Base‘𝑄)) |
94 | 11, 92, 9, 19, 29, 93 | ghmquskerlem2 19235 |
. . . . 5
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) → ∃𝑦 ∈ 𝑠 (𝐽‘𝑠) = (𝐹‘𝑦)) |
95 | 91, 94 | r19.29a 3159 |
. . . 4
⊢
(((((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) ∧ 𝑥 ∈ 𝑟) ∧ (𝐽‘𝑟) = (𝐹‘𝑥)) → (𝐽‘(𝑟(.r‘𝑄)𝑠)) = ((𝐽‘𝑟)(.r‘𝐻)(𝐽‘𝑠))) |
96 | 28 | ad2antrr 725 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) → 𝐹 ∈ (𝐺 GrpHom 𝐻)) |
97 | | simplr 768 |
. . . . 5
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) → 𝑟 ∈ (Base‘𝑄)) |
98 | 11, 96, 9, 19, 29, 97 | ghmquskerlem2 19235 |
. . . 4
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) → ∃𝑥 ∈ 𝑟 (𝐽‘𝑟) = (𝐹‘𝑥)) |
99 | 95, 98 | r19.29a 3159 |
. . 3
⊢ (((𝜑 ∧ 𝑟 ∈ (Base‘𝑄)) ∧ 𝑠 ∈ (Base‘𝑄)) → (𝐽‘(𝑟(.r‘𝑄)𝑠)) = ((𝐽‘𝑟)(.r‘𝐻)(𝐽‘𝑠))) |
100 | 99 | anasss 466 |
. 2
⊢ ((𝜑 ∧ (𝑟 ∈ (Base‘𝑄) ∧ 𝑠 ∈ (Base‘𝑄))) → (𝐽‘(𝑟(.r‘𝑄)𝑠)) = ((𝐽‘𝑟)(.r‘𝐻)(𝐽‘𝑠))) |
101 | 11, 28, 9, 19, 29 | ghmquskerlem3 19236 |
. 2
⊢ (𝜑 → 𝐽 ∈ (𝑄 GrpHom 𝐻)) |
102 | 1, 2, 3, 4, 5, 24,
26, 38, 100, 101 | isrhm2d 20425 |
1
⊢ (𝜑 → 𝐽 ∈ (𝑄 RingHom 𝐻)) |