Step | Hyp | Ref
| Expression |
1 | | rncrhmcl.h |
. . 3
⊢ (𝜑 → 𝐹 ∈ (𝑀 RingHom 𝑁)) |
2 | | rnrhmsubrg 20207 |
. . 3
⊢ (𝐹 ∈ (𝑀 RingHom 𝑁) → ran 𝐹 ∈ (SubRing‘𝑁)) |
3 | | rncrhmcl.c |
. . . 4
⊢ 𝐶 = (𝑁 ↾s ran 𝐹) |
4 | 3 | subrgring 20178 |
. . 3
⊢ (ran
𝐹 ∈
(SubRing‘𝑁) →
𝐶 ∈
Ring) |
5 | 1, 2, 4 | 3syl 18 |
. 2
⊢ (𝜑 → 𝐶 ∈ Ring) |
6 | 3 | ressbasss2 40600 |
. . . . . 6
⊢
(Base‘𝐶)
⊆ ran 𝐹 |
7 | 6 | sseli 3939 |
. . . . 5
⊢ (𝑥 ∈ (Base‘𝐶) → 𝑥 ∈ ran 𝐹) |
8 | 6 | sseli 3939 |
. . . . 5
⊢ (𝑦 ∈ (Base‘𝐶) → 𝑦 ∈ ran 𝐹) |
9 | 7, 8 | anim12i 614 |
. . . 4
⊢ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) |
10 | | eqid 2738 |
. . . . . . . . 9
⊢
(Base‘𝑀) =
(Base‘𝑀) |
11 | | eqid 2738 |
. . . . . . . . 9
⊢
(Base‘𝑁) =
(Base‘𝑁) |
12 | 10, 11 | rhmf 20111 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝑀 RingHom 𝑁) → 𝐹:(Base‘𝑀)⟶(Base‘𝑁)) |
13 | 1, 12 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹:(Base‘𝑀)⟶(Base‘𝑁)) |
14 | 13 | ffnd 6667 |
. . . . . 6
⊢ (𝜑 → 𝐹 Fn (Base‘𝑀)) |
15 | | simpl 484 |
. . . . . 6
⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹) → 𝑥 ∈ ran 𝐹) |
16 | | fvelrnb 6901 |
. . . . . . 7
⊢ (𝐹 Fn (Base‘𝑀) → (𝑥 ∈ ran 𝐹 ↔ ∃𝑎 ∈ (Base‘𝑀)(𝐹‘𝑎) = 𝑥)) |
17 | 16 | biimpa 478 |
. . . . . 6
⊢ ((𝐹 Fn (Base‘𝑀) ∧ 𝑥 ∈ ran 𝐹) → ∃𝑎 ∈ (Base‘𝑀)(𝐹‘𝑎) = 𝑥) |
18 | 14, 15, 17 | syl2an 597 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) → ∃𝑎 ∈ (Base‘𝑀)(𝐹‘𝑎) = 𝑥) |
19 | | simpr 486 |
. . . . . . . 8
⊢ ((𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹) → 𝑦 ∈ ran 𝐹) |
20 | | fvelrnb 6901 |
. . . . . . . . 9
⊢ (𝐹 Fn (Base‘𝑀) → (𝑦 ∈ ran 𝐹 ↔ ∃𝑏 ∈ (Base‘𝑀)(𝐹‘𝑏) = 𝑦)) |
21 | 20 | biimpa 478 |
. . . . . . . 8
⊢ ((𝐹 Fn (Base‘𝑀) ∧ 𝑦 ∈ ran 𝐹) → ∃𝑏 ∈ (Base‘𝑀)(𝐹‘𝑏) = 𝑦) |
22 | 14, 19, 21 | syl2an 597 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) → ∃𝑏 ∈ (Base‘𝑀)(𝐹‘𝑏) = 𝑦) |
23 | 22 | adantr 482 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) ∧ (𝑎 ∈ (Base‘𝑀) ∧ (𝐹‘𝑎) = 𝑥)) → ∃𝑏 ∈ (Base‘𝑀)(𝐹‘𝑏) = 𝑦) |
24 | | rncrhmcl.m |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ CRing) |
25 | 24 | ad3antrrr 729 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) ∧ (𝑎 ∈ (Base‘𝑀) ∧ (𝐹‘𝑎) = 𝑥)) ∧ (𝑏 ∈ (Base‘𝑀) ∧ (𝐹‘𝑏) = 𝑦)) → 𝑀 ∈ CRing) |
26 | | simplrl 776 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) ∧ (𝑎 ∈ (Base‘𝑀) ∧ (𝐹‘𝑎) = 𝑥)) ∧ (𝑏 ∈ (Base‘𝑀) ∧ (𝐹‘𝑏) = 𝑦)) → 𝑎 ∈ (Base‘𝑀)) |
27 | | simprl 770 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) ∧ (𝑎 ∈ (Base‘𝑀) ∧ (𝐹‘𝑎) = 𝑥)) ∧ (𝑏 ∈ (Base‘𝑀) ∧ (𝐹‘𝑏) = 𝑦)) → 𝑏 ∈ (Base‘𝑀)) |
28 | | eqid 2738 |
. . . . . . . . . . 11
⊢
(.r‘𝑀) = (.r‘𝑀) |
29 | 10, 28 | crngcom 19936 |
. . . . . . . . . 10
⊢ ((𝑀 ∈ CRing ∧ 𝑎 ∈ (Base‘𝑀) ∧ 𝑏 ∈ (Base‘𝑀)) → (𝑎(.r‘𝑀)𝑏) = (𝑏(.r‘𝑀)𝑎)) |
30 | 25, 26, 27, 29 | syl3anc 1372 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) ∧ (𝑎 ∈ (Base‘𝑀) ∧ (𝐹‘𝑎) = 𝑥)) ∧ (𝑏 ∈ (Base‘𝑀) ∧ (𝐹‘𝑏) = 𝑦)) → (𝑎(.r‘𝑀)𝑏) = (𝑏(.r‘𝑀)𝑎)) |
31 | 30 | fveq2d 6844 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) ∧ (𝑎 ∈ (Base‘𝑀) ∧ (𝐹‘𝑎) = 𝑥)) ∧ (𝑏 ∈ (Base‘𝑀) ∧ (𝐹‘𝑏) = 𝑦)) → (𝐹‘(𝑎(.r‘𝑀)𝑏)) = (𝐹‘(𝑏(.r‘𝑀)𝑎))) |
32 | 1 | ad3antrrr 729 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) ∧ (𝑎 ∈ (Base‘𝑀) ∧ (𝐹‘𝑎) = 𝑥)) ∧ (𝑏 ∈ (Base‘𝑀) ∧ (𝐹‘𝑏) = 𝑦)) → 𝐹 ∈ (𝑀 RingHom 𝑁)) |
33 | | eqid 2738 |
. . . . . . . . . 10
⊢
(.r‘𝑁) = (.r‘𝑁) |
34 | 10, 28, 33 | rhmmul 20112 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑀 RingHom 𝑁) ∧ 𝑎 ∈ (Base‘𝑀) ∧ 𝑏 ∈ (Base‘𝑀)) → (𝐹‘(𝑎(.r‘𝑀)𝑏)) = ((𝐹‘𝑎)(.r‘𝑁)(𝐹‘𝑏))) |
35 | 32, 26, 27, 34 | syl3anc 1372 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) ∧ (𝑎 ∈ (Base‘𝑀) ∧ (𝐹‘𝑎) = 𝑥)) ∧ (𝑏 ∈ (Base‘𝑀) ∧ (𝐹‘𝑏) = 𝑦)) → (𝐹‘(𝑎(.r‘𝑀)𝑏)) = ((𝐹‘𝑎)(.r‘𝑁)(𝐹‘𝑏))) |
36 | 10, 28, 33 | rhmmul 20112 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑀 RingHom 𝑁) ∧ 𝑏 ∈ (Base‘𝑀) ∧ 𝑎 ∈ (Base‘𝑀)) → (𝐹‘(𝑏(.r‘𝑀)𝑎)) = ((𝐹‘𝑏)(.r‘𝑁)(𝐹‘𝑎))) |
37 | 32, 27, 26, 36 | syl3anc 1372 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) ∧ (𝑎 ∈ (Base‘𝑀) ∧ (𝐹‘𝑎) = 𝑥)) ∧ (𝑏 ∈ (Base‘𝑀) ∧ (𝐹‘𝑏) = 𝑦)) → (𝐹‘(𝑏(.r‘𝑀)𝑎)) = ((𝐹‘𝑏)(.r‘𝑁)(𝐹‘𝑎))) |
38 | 31, 35, 37 | 3eqtr3d 2786 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) ∧ (𝑎 ∈ (Base‘𝑀) ∧ (𝐹‘𝑎) = 𝑥)) ∧ (𝑏 ∈ (Base‘𝑀) ∧ (𝐹‘𝑏) = 𝑦)) → ((𝐹‘𝑎)(.r‘𝑁)(𝐹‘𝑏)) = ((𝐹‘𝑏)(.r‘𝑁)(𝐹‘𝑎))) |
39 | | rnexg 7834 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝑀 RingHom 𝑁) → ran 𝐹 ∈ V) |
40 | 3, 33 | ressmulr 17148 |
. . . . . . . . . 10
⊢ (ran
𝐹 ∈ V →
(.r‘𝑁) =
(.r‘𝐶)) |
41 | 1, 39, 40 | 3syl 18 |
. . . . . . . . 9
⊢ (𝜑 → (.r‘𝑁) = (.r‘𝐶)) |
42 | 41 | ad3antrrr 729 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) ∧ (𝑎 ∈ (Base‘𝑀) ∧ (𝐹‘𝑎) = 𝑥)) ∧ (𝑏 ∈ (Base‘𝑀) ∧ (𝐹‘𝑏) = 𝑦)) → (.r‘𝑁) = (.r‘𝐶)) |
43 | | simplrr 777 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) ∧ (𝑎 ∈ (Base‘𝑀) ∧ (𝐹‘𝑎) = 𝑥)) ∧ (𝑏 ∈ (Base‘𝑀) ∧ (𝐹‘𝑏) = 𝑦)) → (𝐹‘𝑎) = 𝑥) |
44 | | simprr 772 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) ∧ (𝑎 ∈ (Base‘𝑀) ∧ (𝐹‘𝑎) = 𝑥)) ∧ (𝑏 ∈ (Base‘𝑀) ∧ (𝐹‘𝑏) = 𝑦)) → (𝐹‘𝑏) = 𝑦) |
45 | 42, 43, 44 | oveq123d 7373 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) ∧ (𝑎 ∈ (Base‘𝑀) ∧ (𝐹‘𝑎) = 𝑥)) ∧ (𝑏 ∈ (Base‘𝑀) ∧ (𝐹‘𝑏) = 𝑦)) → ((𝐹‘𝑎)(.r‘𝑁)(𝐹‘𝑏)) = (𝑥(.r‘𝐶)𝑦)) |
46 | 42, 44, 43 | oveq123d 7373 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) ∧ (𝑎 ∈ (Base‘𝑀) ∧ (𝐹‘𝑎) = 𝑥)) ∧ (𝑏 ∈ (Base‘𝑀) ∧ (𝐹‘𝑏) = 𝑦)) → ((𝐹‘𝑏)(.r‘𝑁)(𝐹‘𝑎)) = (𝑦(.r‘𝐶)𝑥)) |
47 | 38, 45, 46 | 3eqtr3d 2786 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) ∧ (𝑎 ∈ (Base‘𝑀) ∧ (𝐹‘𝑎) = 𝑥)) ∧ (𝑏 ∈ (Base‘𝑀) ∧ (𝐹‘𝑏) = 𝑦)) → (𝑥(.r‘𝐶)𝑦) = (𝑦(.r‘𝐶)𝑥)) |
48 | 23, 47 | rexlimddv 3157 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) ∧ (𝑎 ∈ (Base‘𝑀) ∧ (𝐹‘𝑎) = 𝑥)) → (𝑥(.r‘𝐶)𝑦) = (𝑦(.r‘𝐶)𝑥)) |
49 | 18, 48 | rexlimddv 3157 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ran 𝐹 ∧ 𝑦 ∈ ran 𝐹)) → (𝑥(.r‘𝐶)𝑦) = (𝑦(.r‘𝐶)𝑥)) |
50 | 9, 49 | sylan2 594 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(.r‘𝐶)𝑦) = (𝑦(.r‘𝐶)𝑥)) |
51 | 50 | ralrimivva 3196 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)(𝑥(.r‘𝐶)𝑦) = (𝑦(.r‘𝐶)𝑥)) |
52 | | eqid 2738 |
. . 3
⊢
(Base‘𝐶) =
(Base‘𝐶) |
53 | | eqid 2738 |
. . 3
⊢
(.r‘𝐶) = (.r‘𝐶) |
54 | 52, 53 | iscrng2 19937 |
. 2
⊢ (𝐶 ∈ CRing ↔ (𝐶 ∈ Ring ∧ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)(𝑥(.r‘𝐶)𝑦) = (𝑦(.r‘𝐶)𝑥))) |
55 | 5, 51, 54 | sylanbrc 584 |
1
⊢ (𝜑 → 𝐶 ∈ CRing) |