Step | Hyp | Ref
| Expression |
1 | | f1ocnv 6361 |
. . . . . . . 8
⊢ (𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆) → ^{◡}𝐹:ran (1^{st} ‘𝑆)–1-1-onto→ran
(1^{st} ‘𝑅)) |
2 | | f1of 6349 |
. . . . . . . 8
⊢ (^{◡}𝐹:ran (1^{st} ‘𝑆)–1-1-onto→ran
(1^{st} ‘𝑅)
→ ^{◡}𝐹:ran (1^{st} ‘𝑆)⟶ran (1^{st}
‘𝑅)) |
3 | 1, 2 | syl 17 |
. . . . . . 7
⊢ (𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆) → ^{◡}𝐹:ran (1^{st} ‘𝑆)⟶ran (1^{st}
‘𝑅)) |
4 | 3 | ad2antll 711 |
. . . . . 6
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆)))
→ ^{◡}𝐹:ran (1^{st} ‘𝑆)⟶ran (1^{st}
‘𝑅)) |
5 | | eqid 2806 |
. . . . . . . . . 10
⊢
(2^{nd} ‘𝑅) = (2^{nd} ‘𝑅) |
6 | | eqid 2806 |
. . . . . . . . . 10
⊢
(GId‘(2^{nd} ‘𝑅)) = (GId‘(2^{nd} ‘𝑅)) |
7 | | eqid 2806 |
. . . . . . . . . 10
⊢
(2^{nd} ‘𝑆) = (2^{nd} ‘𝑆) |
8 | | eqid 2806 |
. . . . . . . . . 10
⊢
(GId‘(2^{nd} ‘𝑆)) = (GId‘(2^{nd} ‘𝑆)) |
9 | 5, 6, 7, 8 | rngohom1 34073 |
. . . . . . . . 9
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹‘(GId‘(2^{nd}
‘𝑅))) =
(GId‘(2^{nd} ‘𝑆))) |
10 | 9 | 3expa 1140 |
. . . . . . . 8
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹‘(GId‘(2^{nd}
‘𝑅))) =
(GId‘(2^{nd} ‘𝑆))) |
11 | 10 | adantrr 699 |
. . . . . . 7
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆)))
→ (𝐹‘(GId‘(2^{nd}
‘𝑅))) =
(GId‘(2^{nd} ‘𝑆))) |
12 | | eqid 2806 |
. . . . . . . . . . 11
⊢ ran
(1^{st} ‘𝑅) =
ran (1^{st} ‘𝑅) |
13 | 12, 5, 6 | rngo1cl 34044 |
. . . . . . . . . 10
⊢ (𝑅 ∈ RingOps →
(GId‘(2^{nd} ‘𝑅)) ∈ ran (1^{st} ‘𝑅)) |
14 | | f1ocnvfv 6754 |
. . . . . . . . . 10
⊢ ((𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆) ∧ (GId‘(2^{nd}
‘𝑅)) ∈ ran
(1^{st} ‘𝑅))
→ ((𝐹‘(GId‘(2^{nd}
‘𝑅))) =
(GId‘(2^{nd} ‘𝑆)) → (^{◡}𝐹‘(GId‘(2^{nd}
‘𝑆))) =
(GId‘(2^{nd} ‘𝑅)))) |
15 | 13, 14 | sylan2 582 |
. . . . . . . . 9
⊢ ((𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆) ∧ 𝑅 ∈ RingOps) → ((𝐹‘(GId‘(2^{nd}
‘𝑅))) =
(GId‘(2^{nd} ‘𝑆)) → (^{◡}𝐹‘(GId‘(2^{nd}
‘𝑆))) =
(GId‘(2^{nd} ‘𝑅)))) |
16 | 15 | ancoms 448 |
. . . . . . . 8
⊢ ((𝑅 ∈ RingOps ∧ 𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆)) → ((𝐹‘(GId‘(2^{nd}
‘𝑅))) =
(GId‘(2^{nd} ‘𝑆)) → (^{◡}𝐹‘(GId‘(2^{nd}
‘𝑆))) =
(GId‘(2^{nd} ‘𝑅)))) |
17 | 16 | ad2ant2rl 746 |
. . . . . . 7
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆)))
→ ((𝐹‘(GId‘(2^{nd}
‘𝑅))) =
(GId‘(2^{nd} ‘𝑆)) → (^{◡}𝐹‘(GId‘(2^{nd}
‘𝑆))) =
(GId‘(2^{nd} ‘𝑅)))) |
18 | 11, 17 | mpd 15 |
. . . . . 6
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆)))
→ (^{◡}𝐹‘(GId‘(2^{nd}
‘𝑆))) =
(GId‘(2^{nd} ‘𝑅))) |
19 | | f1ocnvfv2 6753 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆) ∧ 𝑥 ∈ ran (1^{st} ‘𝑆)) → (𝐹‘(^{◡}𝐹‘𝑥)) = 𝑥) |
20 | | f1ocnvfv2 6753 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆) ∧ 𝑦 ∈ ran (1^{st} ‘𝑆)) → (𝐹‘(^{◡}𝐹‘𝑦)) = 𝑦) |
21 | 19, 20 | anim12da 33813 |
. . . . . . . . . . . . 13
⊢ ((𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆) ∧ (𝑥 ∈ ran (1^{st} ‘𝑆) ∧ 𝑦 ∈ ran (1^{st} ‘𝑆))) → ((𝐹‘(^{◡}𝐹‘𝑥)) = 𝑥 ∧ (𝐹‘(^{◡}𝐹‘𝑦)) = 𝑦)) |
22 | | oveq12 6879 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘(^{◡}𝐹‘𝑥)) = 𝑥 ∧ (𝐹‘(^{◡}𝐹‘𝑦)) = 𝑦) → ((𝐹‘(^{◡}𝐹‘𝑥))(1^{st} ‘𝑆)(𝐹‘(^{◡}𝐹‘𝑦))) = (𝑥(1^{st} ‘𝑆)𝑦)) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆) ∧ (𝑥 ∈ ran (1^{st} ‘𝑆) ∧ 𝑦 ∈ ran (1^{st} ‘𝑆))) → ((𝐹‘(^{◡}𝐹‘𝑥))(1^{st} ‘𝑆)(𝐹‘(^{◡}𝐹‘𝑦))) = (𝑥(1^{st} ‘𝑆)𝑦)) |
24 | 23 | adantll 696 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆))
∧ (𝑥 ∈ ran
(1^{st} ‘𝑆)
∧ 𝑦 ∈ ran
(1^{st} ‘𝑆)))
→ ((𝐹‘(^{◡}𝐹‘𝑥))(1^{st} ‘𝑆)(𝐹‘(^{◡}𝐹‘𝑦))) = (𝑥(1^{st} ‘𝑆)𝑦)) |
25 | 24 | adantll 696 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆)))
∧ (𝑥 ∈ ran
(1^{st} ‘𝑆)
∧ 𝑦 ∈ ran
(1^{st} ‘𝑆)))
→ ((𝐹‘(^{◡}𝐹‘𝑥))(1^{st} ‘𝑆)(𝐹‘(^{◡}𝐹‘𝑦))) = (𝑥(1^{st} ‘𝑆)𝑦)) |
26 | | f1ocnvdm 6760 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆) ∧ 𝑥 ∈ ran (1^{st} ‘𝑆)) → (^{◡}𝐹‘𝑥) ∈ ran (1^{st} ‘𝑅)) |
27 | | f1ocnvdm 6760 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆) ∧ 𝑦 ∈ ran (1^{st} ‘𝑆)) → (^{◡}𝐹‘𝑦) ∈ ran (1^{st} ‘𝑅)) |
28 | 26, 27 | anim12da 33813 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆) ∧ (𝑥 ∈ ran (1^{st} ‘𝑆) ∧ 𝑦 ∈ ran (1^{st} ‘𝑆))) → ((^{◡}𝐹‘𝑥) ∈ ran (1^{st} ‘𝑅) ∧ (^{◡}𝐹‘𝑦) ∈ ran (1^{st} ‘𝑅))) |
29 | | eqid 2806 |
. . . . . . . . . . . . . . . 16
⊢
(1^{st} ‘𝑅) = (1^{st} ‘𝑅) |
30 | | eqid 2806 |
. . . . . . . . . . . . . . . 16
⊢
(1^{st} ‘𝑆) = (1^{st} ‘𝑆) |
31 | 29, 12, 30 | rngohomadd 34074 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ ((^{◡}𝐹‘𝑥) ∈ ran (1^{st} ‘𝑅) ∧ (^{◡}𝐹‘𝑦) ∈ ran (1^{st} ‘𝑅))) → (𝐹‘((^{◡}𝐹‘𝑥)(1^{st} ‘𝑅)(^{◡}𝐹‘𝑦))) = ((𝐹‘(^{◡}𝐹‘𝑥))(1^{st} ‘𝑆)(𝐹‘(^{◡}𝐹‘𝑦)))) |
32 | 28, 31 | sylan2 582 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆)
∧ (𝑥 ∈ ran
(1^{st} ‘𝑆)
∧ 𝑦 ∈ ran
(1^{st} ‘𝑆)))) → (𝐹‘((^{◡}𝐹‘𝑥)(1^{st} ‘𝑅)(^{◡}𝐹‘𝑦))) = ((𝐹‘(^{◡}𝐹‘𝑥))(1^{st} ‘𝑆)(𝐹‘(^{◡}𝐹‘𝑦)))) |
33 | 32 | exp32 409 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆)
→ ((𝑥 ∈ ran
(1^{st} ‘𝑆)
∧ 𝑦 ∈ ran
(1^{st} ‘𝑆))
→ (𝐹‘((^{◡}𝐹‘𝑥)(1^{st} ‘𝑅)(^{◡}𝐹‘𝑦))) = ((𝐹‘(^{◡}𝐹‘𝑥))(1^{st} ‘𝑆)(𝐹‘(^{◡}𝐹‘𝑦)))))) |
34 | 33 | 3expa 1140 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆)
→ ((𝑥 ∈ ran
(1^{st} ‘𝑆)
∧ 𝑦 ∈ ran
(1^{st} ‘𝑆))
→ (𝐹‘((^{◡}𝐹‘𝑥)(1^{st} ‘𝑅)(^{◡}𝐹‘𝑦))) = ((𝐹‘(^{◡}𝐹‘𝑥))(1^{st} ‘𝑆)(𝐹‘(^{◡}𝐹‘𝑦)))))) |
35 | 34 | impr 444 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆)))
→ ((𝑥 ∈ ran
(1^{st} ‘𝑆)
∧ 𝑦 ∈ ran
(1^{st} ‘𝑆))
→ (𝐹‘((^{◡}𝐹‘𝑥)(1^{st} ‘𝑅)(^{◡}𝐹‘𝑦))) = ((𝐹‘(^{◡}𝐹‘𝑥))(1^{st} ‘𝑆)(𝐹‘(^{◡}𝐹‘𝑦))))) |
36 | 35 | imp 395 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆)))
∧ (𝑥 ∈ ran
(1^{st} ‘𝑆)
∧ 𝑦 ∈ ran
(1^{st} ‘𝑆)))
→ (𝐹‘((^{◡}𝐹‘𝑥)(1^{st} ‘𝑅)(^{◡}𝐹‘𝑦))) = ((𝐹‘(^{◡}𝐹‘𝑥))(1^{st} ‘𝑆)(𝐹‘(^{◡}𝐹‘𝑦)))) |
37 | | eqid 2806 |
. . . . . . . . . . . . . . . 16
⊢ ran
(1^{st} ‘𝑆) =
ran (1^{st} ‘𝑆) |
38 | 30, 37 | rngogcl 34017 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ∈ RingOps ∧ 𝑥 ∈ ran (1^{st}
‘𝑆) ∧ 𝑦 ∈ ran (1^{st}
‘𝑆)) → (𝑥(1^{st} ‘𝑆)𝑦) ∈ ran (1^{st} ‘𝑆)) |
39 | 38 | 3expb 1142 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ RingOps ∧ (𝑥 ∈ ran (1^{st}
‘𝑆) ∧ 𝑦 ∈ ran (1^{st}
‘𝑆))) → (𝑥(1^{st} ‘𝑆)𝑦) ∈ ran (1^{st} ‘𝑆)) |
40 | | f1ocnvfv2 6753 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆) ∧ (𝑥(1^{st} ‘𝑆)𝑦) ∈ ran (1^{st} ‘𝑆)) → (𝐹‘(^{◡}𝐹‘(𝑥(1^{st} ‘𝑆)𝑦))) = (𝑥(1^{st} ‘𝑆)𝑦)) |
41 | 40 | ancoms 448 |
. . . . . . . . . . . . . 14
⊢ (((𝑥(1^{st} ‘𝑆)𝑦) ∈ ran (1^{st} ‘𝑆) ∧ 𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆))
→ (𝐹‘(^{◡}𝐹‘(𝑥(1^{st} ‘𝑆)𝑦))) = (𝑥(1^{st} ‘𝑆)𝑦)) |
42 | 39, 41 | sylan 571 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ RingOps ∧ (𝑥 ∈ ran (1^{st}
‘𝑆) ∧ 𝑦 ∈ ran (1^{st}
‘𝑆))) ∧ 𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆)) → (𝐹‘(^{◡}𝐹‘(𝑥(1^{st} ‘𝑆)𝑦))) = (𝑥(1^{st} ‘𝑆)𝑦)) |
43 | 42 | an32s 634 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ RingOps ∧ 𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆)) ∧ (𝑥 ∈ ran (1^{st} ‘𝑆) ∧ 𝑦 ∈ ran (1^{st} ‘𝑆))) → (𝐹‘(^{◡}𝐹‘(𝑥(1^{st} ‘𝑆)𝑦))) = (𝑥(1^{st} ‘𝑆)𝑦)) |
44 | 43 | adantlll 700 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆)) ∧ (𝑥 ∈ ran (1^{st} ‘𝑆) ∧ 𝑦 ∈ ran (1^{st} ‘𝑆))) → (𝐹‘(^{◡}𝐹‘(𝑥(1^{st} ‘𝑆)𝑦))) = (𝑥(1^{st} ‘𝑆)𝑦)) |
45 | 44 | adantlrl 702 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆)))
∧ (𝑥 ∈ ran
(1^{st} ‘𝑆)
∧ 𝑦 ∈ ran
(1^{st} ‘𝑆)))
→ (𝐹‘(^{◡}𝐹‘(𝑥(1^{st} ‘𝑆)𝑦))) = (𝑥(1^{st} ‘𝑆)𝑦)) |
46 | 25, 36, 45 | 3eqtr4rd 2851 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆)))
∧ (𝑥 ∈ ran
(1^{st} ‘𝑆)
∧ 𝑦 ∈ ran
(1^{st} ‘𝑆)))
→ (𝐹‘(^{◡}𝐹‘(𝑥(1^{st} ‘𝑆)𝑦))) = (𝐹‘((^{◡}𝐹‘𝑥)(1^{st} ‘𝑅)(^{◡}𝐹‘𝑦)))) |
47 | | f1of1 6348 |
. . . . . . . . . . . 12
⊢ (𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆) → 𝐹:ran (1^{st} ‘𝑅)–1-1→ran (1^{st} ‘𝑆)) |
48 | 47 | ad2antlr 709 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆)) ∧ (𝑥 ∈ ran (1^{st} ‘𝑆) ∧ 𝑦 ∈ ran (1^{st} ‘𝑆))) → 𝐹:ran (1^{st} ‘𝑅)–1-1→ran (1^{st} ‘𝑆)) |
49 | | f1ocnvdm 6760 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆) ∧ (𝑥(1^{st} ‘𝑆)𝑦) ∈ ran (1^{st} ‘𝑆)) → (^{◡}𝐹‘(𝑥(1^{st} ‘𝑆)𝑦)) ∈ ran (1^{st} ‘𝑅)) |
50 | 49 | ancoms 448 |
. . . . . . . . . . . . . 14
⊢ (((𝑥(1^{st} ‘𝑆)𝑦) ∈ ran (1^{st} ‘𝑆) ∧ 𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆))
→ (^{◡}𝐹‘(𝑥(1^{st} ‘𝑆)𝑦)) ∈ ran (1^{st} ‘𝑅)) |
51 | 39, 50 | sylan 571 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ RingOps ∧ (𝑥 ∈ ran (1^{st}
‘𝑆) ∧ 𝑦 ∈ ran (1^{st}
‘𝑆))) ∧ 𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆)) → (^{◡}𝐹‘(𝑥(1^{st} ‘𝑆)𝑦)) ∈ ran (1^{st} ‘𝑅)) |
52 | 51 | an32s 634 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ RingOps ∧ 𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆)) ∧ (𝑥 ∈ ran (1^{st} ‘𝑆) ∧ 𝑦 ∈ ran (1^{st} ‘𝑆))) → (^{◡}𝐹‘(𝑥(1^{st} ‘𝑆)𝑦)) ∈ ran (1^{st} ‘𝑅)) |
53 | 52 | adantlll 700 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆)) ∧ (𝑥 ∈ ran (1^{st} ‘𝑆) ∧ 𝑦 ∈ ran (1^{st} ‘𝑆))) → (^{◡}𝐹‘(𝑥(1^{st} ‘𝑆)𝑦)) ∈ ran (1^{st} ‘𝑅)) |
54 | 29, 12 | rngogcl 34017 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ RingOps ∧ (^{◡}𝐹‘𝑥) ∈ ran (1^{st} ‘𝑅) ∧ (^{◡}𝐹‘𝑦) ∈ ran (1^{st} ‘𝑅)) → ((^{◡}𝐹‘𝑥)(1^{st} ‘𝑅)(^{◡}𝐹‘𝑦)) ∈ ran (1^{st} ‘𝑅)) |
55 | 54 | 3expb 1142 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ RingOps ∧ ((^{◡}𝐹‘𝑥) ∈ ran (1^{st} ‘𝑅) ∧ (^{◡}𝐹‘𝑦) ∈ ran (1^{st} ‘𝑅))) → ((^{◡}𝐹‘𝑥)(1^{st} ‘𝑅)(^{◡}𝐹‘𝑦)) ∈ ran (1^{st} ‘𝑅)) |
56 | 28, 55 | sylan2 582 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ RingOps ∧ (𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆) ∧ (𝑥 ∈ ran (1^{st} ‘𝑆) ∧ 𝑦 ∈ ran (1^{st} ‘𝑆)))) → ((^{◡}𝐹‘𝑥)(1^{st} ‘𝑅)(^{◡}𝐹‘𝑦)) ∈ ran (1^{st} ‘𝑅)) |
57 | 56 | anassrs 455 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ RingOps ∧ 𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆)) ∧ (𝑥 ∈ ran (1^{st} ‘𝑆) ∧ 𝑦 ∈ ran (1^{st} ‘𝑆))) → ((^{◡}𝐹‘𝑥)(1^{st} ‘𝑅)(^{◡}𝐹‘𝑦)) ∈ ran (1^{st} ‘𝑅)) |
58 | 57 | adantllr 701 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆)) ∧ (𝑥 ∈ ran (1^{st} ‘𝑆) ∧ 𝑦 ∈ ran (1^{st} ‘𝑆))) → ((^{◡}𝐹‘𝑥)(1^{st} ‘𝑅)(^{◡}𝐹‘𝑦)) ∈ ran (1^{st} ‘𝑅)) |
59 | | f1fveq 6739 |
. . . . . . . . . . 11
⊢ ((𝐹:ran (1^{st}
‘𝑅)–1-1→ran (1^{st} ‘𝑆) ∧ ((^{◡}𝐹‘(𝑥(1^{st} ‘𝑆)𝑦)) ∈ ran (1^{st} ‘𝑅) ∧ ((^{◡}𝐹‘𝑥)(1^{st} ‘𝑅)(^{◡}𝐹‘𝑦)) ∈ ran (1^{st} ‘𝑅))) → ((𝐹‘(^{◡}𝐹‘(𝑥(1^{st} ‘𝑆)𝑦))) = (𝐹‘((^{◡}𝐹‘𝑥)(1^{st} ‘𝑅)(^{◡}𝐹‘𝑦))) ↔ (^{◡}𝐹‘(𝑥(1^{st} ‘𝑆)𝑦)) = ((^{◡}𝐹‘𝑥)(1^{st} ‘𝑅)(^{◡}𝐹‘𝑦)))) |
60 | 48, 53, 58, 59 | syl12anc 856 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆)) ∧ (𝑥 ∈ ran (1^{st} ‘𝑆) ∧ 𝑦 ∈ ran (1^{st} ‘𝑆))) → ((𝐹‘(^{◡}𝐹‘(𝑥(1^{st} ‘𝑆)𝑦))) = (𝐹‘((^{◡}𝐹‘𝑥)(1^{st} ‘𝑅)(^{◡}𝐹‘𝑦))) ↔ (^{◡}𝐹‘(𝑥(1^{st} ‘𝑆)𝑦)) = ((^{◡}𝐹‘𝑥)(1^{st} ‘𝑅)(^{◡}𝐹‘𝑦)))) |
61 | 60 | adantlrl 702 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆)))
∧ (𝑥 ∈ ran
(1^{st} ‘𝑆)
∧ 𝑦 ∈ ran
(1^{st} ‘𝑆)))
→ ((𝐹‘(^{◡}𝐹‘(𝑥(1^{st} ‘𝑆)𝑦))) = (𝐹‘((^{◡}𝐹‘𝑥)(1^{st} ‘𝑅)(^{◡}𝐹‘𝑦))) ↔ (^{◡}𝐹‘(𝑥(1^{st} ‘𝑆)𝑦)) = ((^{◡}𝐹‘𝑥)(1^{st} ‘𝑅)(^{◡}𝐹‘𝑦)))) |
62 | 46, 61 | mpbid 223 |
. . . . . . . 8
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆)))
∧ (𝑥 ∈ ran
(1^{st} ‘𝑆)
∧ 𝑦 ∈ ran
(1^{st} ‘𝑆)))
→ (^{◡}𝐹‘(𝑥(1^{st} ‘𝑆)𝑦)) = ((^{◡}𝐹‘𝑥)(1^{st} ‘𝑅)(^{◡}𝐹‘𝑦))) |
63 | | oveq12 6879 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘(^{◡}𝐹‘𝑥)) = 𝑥 ∧ (𝐹‘(^{◡}𝐹‘𝑦)) = 𝑦) → ((𝐹‘(^{◡}𝐹‘𝑥))(2^{nd} ‘𝑆)(𝐹‘(^{◡}𝐹‘𝑦))) = (𝑥(2^{nd} ‘𝑆)𝑦)) |
64 | 21, 63 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆) ∧ (𝑥 ∈ ran (1^{st} ‘𝑆) ∧ 𝑦 ∈ ran (1^{st} ‘𝑆))) → ((𝐹‘(^{◡}𝐹‘𝑥))(2^{nd} ‘𝑆)(𝐹‘(^{◡}𝐹‘𝑦))) = (𝑥(2^{nd} ‘𝑆)𝑦)) |
65 | 64 | adantll 696 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆))
∧ (𝑥 ∈ ran
(1^{st} ‘𝑆)
∧ 𝑦 ∈ ran
(1^{st} ‘𝑆)))
→ ((𝐹‘(^{◡}𝐹‘𝑥))(2^{nd} ‘𝑆)(𝐹‘(^{◡}𝐹‘𝑦))) = (𝑥(2^{nd} ‘𝑆)𝑦)) |
66 | 65 | adantll 696 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆)))
∧ (𝑥 ∈ ran
(1^{st} ‘𝑆)
∧ 𝑦 ∈ ran
(1^{st} ‘𝑆)))
→ ((𝐹‘(^{◡}𝐹‘𝑥))(2^{nd} ‘𝑆)(𝐹‘(^{◡}𝐹‘𝑦))) = (𝑥(2^{nd} ‘𝑆)𝑦)) |
67 | 29, 12, 5, 7 | rngohommul 34075 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ ((^{◡}𝐹‘𝑥) ∈ ran (1^{st} ‘𝑅) ∧ (^{◡}𝐹‘𝑦) ∈ ran (1^{st} ‘𝑅))) → (𝐹‘((^{◡}𝐹‘𝑥)(2^{nd} ‘𝑅)(^{◡}𝐹‘𝑦))) = ((𝐹‘(^{◡}𝐹‘𝑥))(2^{nd} ‘𝑆)(𝐹‘(^{◡}𝐹‘𝑦)))) |
68 | 28, 67 | sylan2 582 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) ∧ (𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆)
∧ (𝑥 ∈ ran
(1^{st} ‘𝑆)
∧ 𝑦 ∈ ran
(1^{st} ‘𝑆)))) → (𝐹‘((^{◡}𝐹‘𝑥)(2^{nd} ‘𝑅)(^{◡}𝐹‘𝑦))) = ((𝐹‘(^{◡}𝐹‘𝑥))(2^{nd} ‘𝑆)(𝐹‘(^{◡}𝐹‘𝑦)))) |
69 | 68 | exp32 409 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆)
→ ((𝑥 ∈ ran
(1^{st} ‘𝑆)
∧ 𝑦 ∈ ran
(1^{st} ‘𝑆))
→ (𝐹‘((^{◡}𝐹‘𝑥)(2^{nd} ‘𝑅)(^{◡}𝐹‘𝑦))) = ((𝐹‘(^{◡}𝐹‘𝑥))(2^{nd} ‘𝑆)(𝐹‘(^{◡}𝐹‘𝑦)))))) |
70 | 69 | 3expa 1140 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆)
→ ((𝑥 ∈ ran
(1^{st} ‘𝑆)
∧ 𝑦 ∈ ran
(1^{st} ‘𝑆))
→ (𝐹‘((^{◡}𝐹‘𝑥)(2^{nd} ‘𝑅)(^{◡}𝐹‘𝑦))) = ((𝐹‘(^{◡}𝐹‘𝑥))(2^{nd} ‘𝑆)(𝐹‘(^{◡}𝐹‘𝑦)))))) |
71 | 70 | impr 444 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆)))
→ ((𝑥 ∈ ran
(1^{st} ‘𝑆)
∧ 𝑦 ∈ ran
(1^{st} ‘𝑆))
→ (𝐹‘((^{◡}𝐹‘𝑥)(2^{nd} ‘𝑅)(^{◡}𝐹‘𝑦))) = ((𝐹‘(^{◡}𝐹‘𝑥))(2^{nd} ‘𝑆)(𝐹‘(^{◡}𝐹‘𝑦))))) |
72 | 71 | imp 395 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆)))
∧ (𝑥 ∈ ran
(1^{st} ‘𝑆)
∧ 𝑦 ∈ ran
(1^{st} ‘𝑆)))
→ (𝐹‘((^{◡}𝐹‘𝑥)(2^{nd} ‘𝑅)(^{◡}𝐹‘𝑦))) = ((𝐹‘(^{◡}𝐹‘𝑥))(2^{nd} ‘𝑆)(𝐹‘(^{◡}𝐹‘𝑦)))) |
73 | 30, 7, 37 | rngocl 34006 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 ∈ RingOps ∧ 𝑥 ∈ ran (1^{st}
‘𝑆) ∧ 𝑦 ∈ ran (1^{st}
‘𝑆)) → (𝑥(2^{nd} ‘𝑆)𝑦) ∈ ran (1^{st} ‘𝑆)) |
74 | 73 | 3expb 1142 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ RingOps ∧ (𝑥 ∈ ran (1^{st}
‘𝑆) ∧ 𝑦 ∈ ran (1^{st}
‘𝑆))) → (𝑥(2^{nd} ‘𝑆)𝑦) ∈ ran (1^{st} ‘𝑆)) |
75 | | f1ocnvfv2 6753 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆) ∧ (𝑥(2^{nd} ‘𝑆)𝑦) ∈ ran (1^{st} ‘𝑆)) → (𝐹‘(^{◡}𝐹‘(𝑥(2^{nd} ‘𝑆)𝑦))) = (𝑥(2^{nd} ‘𝑆)𝑦)) |
76 | 75 | ancoms 448 |
. . . . . . . . . . . . . 14
⊢ (((𝑥(2^{nd} ‘𝑆)𝑦) ∈ ran (1^{st} ‘𝑆) ∧ 𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆))
→ (𝐹‘(^{◡}𝐹‘(𝑥(2^{nd} ‘𝑆)𝑦))) = (𝑥(2^{nd} ‘𝑆)𝑦)) |
77 | 74, 76 | sylan 571 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ RingOps ∧ (𝑥 ∈ ran (1^{st}
‘𝑆) ∧ 𝑦 ∈ ran (1^{st}
‘𝑆))) ∧ 𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆)) → (𝐹‘(^{◡}𝐹‘(𝑥(2^{nd} ‘𝑆)𝑦))) = (𝑥(2^{nd} ‘𝑆)𝑦)) |
78 | 77 | an32s 634 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ RingOps ∧ 𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆)) ∧ (𝑥 ∈ ran (1^{st} ‘𝑆) ∧ 𝑦 ∈ ran (1^{st} ‘𝑆))) → (𝐹‘(^{◡}𝐹‘(𝑥(2^{nd} ‘𝑆)𝑦))) = (𝑥(2^{nd} ‘𝑆)𝑦)) |
79 | 78 | adantlll 700 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆)) ∧ (𝑥 ∈ ran (1^{st} ‘𝑆) ∧ 𝑦 ∈ ran (1^{st} ‘𝑆))) → (𝐹‘(^{◡}𝐹‘(𝑥(2^{nd} ‘𝑆)𝑦))) = (𝑥(2^{nd} ‘𝑆)𝑦)) |
80 | 79 | adantlrl 702 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆)))
∧ (𝑥 ∈ ran
(1^{st} ‘𝑆)
∧ 𝑦 ∈ ran
(1^{st} ‘𝑆)))
→ (𝐹‘(^{◡}𝐹‘(𝑥(2^{nd} ‘𝑆)𝑦))) = (𝑥(2^{nd} ‘𝑆)𝑦)) |
81 | 66, 72, 80 | 3eqtr4rd 2851 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆)))
∧ (𝑥 ∈ ran
(1^{st} ‘𝑆)
∧ 𝑦 ∈ ran
(1^{st} ‘𝑆)))
→ (𝐹‘(^{◡}𝐹‘(𝑥(2^{nd} ‘𝑆)𝑦))) = (𝐹‘((^{◡}𝐹‘𝑥)(2^{nd} ‘𝑅)(^{◡}𝐹‘𝑦)))) |
82 | | f1ocnvdm 6760 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆) ∧ (𝑥(2^{nd} ‘𝑆)𝑦) ∈ ran (1^{st} ‘𝑆)) → (^{◡}𝐹‘(𝑥(2^{nd} ‘𝑆)𝑦)) ∈ ran (1^{st} ‘𝑅)) |
83 | 82 | ancoms 448 |
. . . . . . . . . . . . . 14
⊢ (((𝑥(2^{nd} ‘𝑆)𝑦) ∈ ran (1^{st} ‘𝑆) ∧ 𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆))
→ (^{◡}𝐹‘(𝑥(2^{nd} ‘𝑆)𝑦)) ∈ ran (1^{st} ‘𝑅)) |
84 | 74, 83 | sylan 571 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ RingOps ∧ (𝑥 ∈ ran (1^{st}
‘𝑆) ∧ 𝑦 ∈ ran (1^{st}
‘𝑆))) ∧ 𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆)) → (^{◡}𝐹‘(𝑥(2^{nd} ‘𝑆)𝑦)) ∈ ran (1^{st} ‘𝑅)) |
85 | 84 | an32s 634 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ RingOps ∧ 𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆)) ∧ (𝑥 ∈ ran (1^{st} ‘𝑆) ∧ 𝑦 ∈ ran (1^{st} ‘𝑆))) → (^{◡}𝐹‘(𝑥(2^{nd} ‘𝑆)𝑦)) ∈ ran (1^{st} ‘𝑅)) |
86 | 85 | adantlll 700 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆)) ∧ (𝑥 ∈ ran (1^{st} ‘𝑆) ∧ 𝑦 ∈ ran (1^{st} ‘𝑆))) → (^{◡}𝐹‘(𝑥(2^{nd} ‘𝑆)𝑦)) ∈ ran (1^{st} ‘𝑅)) |
87 | 29, 5, 12 | rngocl 34006 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 ∈ RingOps ∧ (^{◡}𝐹‘𝑥) ∈ ran (1^{st} ‘𝑅) ∧ (^{◡}𝐹‘𝑦) ∈ ran (1^{st} ‘𝑅)) → ((^{◡}𝐹‘𝑥)(2^{nd} ‘𝑅)(^{◡}𝐹‘𝑦)) ∈ ran (1^{st} ‘𝑅)) |
88 | 87 | 3expb 1142 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 ∈ RingOps ∧ ((^{◡}𝐹‘𝑥) ∈ ran (1^{st} ‘𝑅) ∧ (^{◡}𝐹‘𝑦) ∈ ran (1^{st} ‘𝑅))) → ((^{◡}𝐹‘𝑥)(2^{nd} ‘𝑅)(^{◡}𝐹‘𝑦)) ∈ ran (1^{st} ‘𝑅)) |
89 | 28, 88 | sylan2 582 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ RingOps ∧ (𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆) ∧ (𝑥 ∈ ran (1^{st} ‘𝑆) ∧ 𝑦 ∈ ran (1^{st} ‘𝑆)))) → ((^{◡}𝐹‘𝑥)(2^{nd} ‘𝑅)(^{◡}𝐹‘𝑦)) ∈ ran (1^{st} ‘𝑅)) |
90 | 89 | anassrs 455 |
. . . . . . . . . . . 12
⊢ (((𝑅 ∈ RingOps ∧ 𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆)) ∧ (𝑥 ∈ ran (1^{st} ‘𝑆) ∧ 𝑦 ∈ ran (1^{st} ‘𝑆))) → ((^{◡}𝐹‘𝑥)(2^{nd} ‘𝑅)(^{◡}𝐹‘𝑦)) ∈ ran (1^{st} ‘𝑅)) |
91 | 90 | adantllr 701 |
. . . . . . . . . . 11
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆)) ∧ (𝑥 ∈ ran (1^{st} ‘𝑆) ∧ 𝑦 ∈ ran (1^{st} ‘𝑆))) → ((^{◡}𝐹‘𝑥)(2^{nd} ‘𝑅)(^{◡}𝐹‘𝑦)) ∈ ran (1^{st} ‘𝑅)) |
92 | | f1fveq 6739 |
. . . . . . . . . . 11
⊢ ((𝐹:ran (1^{st}
‘𝑅)–1-1→ran (1^{st} ‘𝑆) ∧ ((^{◡}𝐹‘(𝑥(2^{nd} ‘𝑆)𝑦)) ∈ ran (1^{st} ‘𝑅) ∧ ((^{◡}𝐹‘𝑥)(2^{nd} ‘𝑅)(^{◡}𝐹‘𝑦)) ∈ ran (1^{st} ‘𝑅))) → ((𝐹‘(^{◡}𝐹‘(𝑥(2^{nd} ‘𝑆)𝑦))) = (𝐹‘((^{◡}𝐹‘𝑥)(2^{nd} ‘𝑅)(^{◡}𝐹‘𝑦))) ↔ (^{◡}𝐹‘(𝑥(2^{nd} ‘𝑆)𝑦)) = ((^{◡}𝐹‘𝑥)(2^{nd} ‘𝑅)(^{◡}𝐹‘𝑦)))) |
93 | 48, 86, 91, 92 | syl12anc 856 |
. . . . . . . . . 10
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ 𝐹:ran (1^{st}
‘𝑅)–1-1-onto→ran (1^{st} ‘𝑆)) ∧ (𝑥 ∈ ran (1^{st} ‘𝑆) ∧ 𝑦 ∈ ran (1^{st} ‘𝑆))) → ((𝐹‘(^{◡}𝐹‘(𝑥(2^{nd} ‘𝑆)𝑦))) = (𝐹‘((^{◡}𝐹‘𝑥)(2^{nd} ‘𝑅)(^{◡}𝐹‘𝑦))) ↔ (^{◡}𝐹‘(𝑥(2^{nd} ‘𝑆)𝑦)) = ((^{◡}𝐹‘𝑥)(2^{nd} ‘𝑅)(^{◡}𝐹‘𝑦)))) |
94 | 93 | adantlrl 702 |
. . . . . . . . 9
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆)))
∧ (𝑥 ∈ ran
(1^{st} ‘𝑆)
∧ 𝑦 ∈ ran
(1^{st} ‘𝑆)))
→ ((𝐹‘(^{◡}𝐹‘(𝑥(2^{nd} ‘𝑆)𝑦))) = (𝐹‘((^{◡}𝐹‘𝑥)(2^{nd} ‘𝑅)(^{◡}𝐹‘𝑦))) ↔ (^{◡}𝐹‘(𝑥(2^{nd} ‘𝑆)𝑦)) = ((^{◡}𝐹‘𝑥)(2^{nd} ‘𝑅)(^{◡}𝐹‘𝑦)))) |
95 | 81, 94 | mpbid 223 |
. . . . . . . 8
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆)))
∧ (𝑥 ∈ ran
(1^{st} ‘𝑆)
∧ 𝑦 ∈ ran
(1^{st} ‘𝑆)))
→ (^{◡}𝐹‘(𝑥(2^{nd} ‘𝑆)𝑦)) = ((^{◡}𝐹‘𝑥)(2^{nd} ‘𝑅)(^{◡}𝐹‘𝑦))) |
96 | 62, 95 | jca 503 |
. . . . . . 7
⊢ ((((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆)))
∧ (𝑥 ∈ ran
(1^{st} ‘𝑆)
∧ 𝑦 ∈ ran
(1^{st} ‘𝑆)))
→ ((^{◡}𝐹‘(𝑥(1^{st} ‘𝑆)𝑦)) = ((^{◡}𝐹‘𝑥)(1^{st} ‘𝑅)(^{◡}𝐹‘𝑦)) ∧ (^{◡}𝐹‘(𝑥(2^{nd} ‘𝑆)𝑦)) = ((^{◡}𝐹‘𝑥)(2^{nd} ‘𝑅)(^{◡}𝐹‘𝑦)))) |
97 | 96 | ralrimivva 3159 |
. . . . . 6
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆)))
→ ∀𝑥 ∈ ran
(1^{st} ‘𝑆)∀𝑦 ∈ ran (1^{st} ‘𝑆)((^{◡}𝐹‘(𝑥(1^{st} ‘𝑆)𝑦)) = ((^{◡}𝐹‘𝑥)(1^{st} ‘𝑅)(^{◡}𝐹‘𝑦)) ∧ (^{◡}𝐹‘(𝑥(2^{nd} ‘𝑆)𝑦)) = ((^{◡}𝐹‘𝑥)(2^{nd} ‘𝑅)(^{◡}𝐹‘𝑦)))) |
98 | 30, 7, 37, 8, 29, 5, 12, 6 | isrngohom 34070 |
. . . . . . . 8
⊢ ((𝑆 ∈ RingOps ∧ 𝑅 ∈ RingOps) → (^{◡}𝐹 ∈ (𝑆 RngHom 𝑅) ↔ (^{◡}𝐹:ran (1^{st} ‘𝑆)⟶ran (1^{st}
‘𝑅) ∧ (^{◡}𝐹‘(GId‘(2^{nd}
‘𝑆))) =
(GId‘(2^{nd} ‘𝑅)) ∧ ∀𝑥 ∈ ran (1^{st} ‘𝑆)∀𝑦 ∈ ran (1^{st} ‘𝑆)((^{◡}𝐹‘(𝑥(1^{st} ‘𝑆)𝑦)) = ((^{◡}𝐹‘𝑥)(1^{st} ‘𝑅)(^{◡}𝐹‘𝑦)) ∧ (^{◡}𝐹‘(𝑥(2^{nd} ‘𝑆)𝑦)) = ((^{◡}𝐹‘𝑥)(2^{nd} ‘𝑅)(^{◡}𝐹‘𝑦)))))) |
99 | 98 | ancoms 448 |
. . . . . . 7
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (^{◡}𝐹 ∈ (𝑆 RngHom 𝑅) ↔ (^{◡}𝐹:ran (1^{st} ‘𝑆)⟶ran (1^{st}
‘𝑅) ∧ (^{◡}𝐹‘(GId‘(2^{nd}
‘𝑆))) =
(GId‘(2^{nd} ‘𝑅)) ∧ ∀𝑥 ∈ ran (1^{st} ‘𝑆)∀𝑦 ∈ ran (1^{st} ‘𝑆)((^{◡}𝐹‘(𝑥(1^{st} ‘𝑆)𝑦)) = ((^{◡}𝐹‘𝑥)(1^{st} ‘𝑅)(^{◡}𝐹‘𝑦)) ∧ (^{◡}𝐹‘(𝑥(2^{nd} ‘𝑆)𝑦)) = ((^{◡}𝐹‘𝑥)(2^{nd} ‘𝑅)(^{◡}𝐹‘𝑦)))))) |
100 | 99 | adantr 468 |
. . . . . 6
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆)))
→ (^{◡}𝐹 ∈ (𝑆 RngHom 𝑅) ↔ (^{◡}𝐹:ran (1^{st} ‘𝑆)⟶ran (1^{st}
‘𝑅) ∧ (^{◡}𝐹‘(GId‘(2^{nd}
‘𝑆))) =
(GId‘(2^{nd} ‘𝑅)) ∧ ∀𝑥 ∈ ran (1^{st} ‘𝑆)∀𝑦 ∈ ran (1^{st} ‘𝑆)((^{◡}𝐹‘(𝑥(1^{st} ‘𝑆)𝑦)) = ((^{◡}𝐹‘𝑥)(1^{st} ‘𝑅)(^{◡}𝐹‘𝑦)) ∧ (^{◡}𝐹‘(𝑥(2^{nd} ‘𝑆)𝑦)) = ((^{◡}𝐹‘𝑥)(2^{nd} ‘𝑅)(^{◡}𝐹‘𝑦)))))) |
101 | 4, 18, 97, 100 | mpbir3and 1435 |
. . . . 5
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆)))
→ ^{◡}𝐹 ∈ (𝑆 RngHom 𝑅)) |
102 | 1 | ad2antll 711 |
. . . . 5
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆)))
→ ^{◡}𝐹:ran (1^{st} ‘𝑆)–1-1-onto→ran
(1^{st} ‘𝑅)) |
103 | 101, 102 | jca 503 |
. . . 4
⊢ (((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) ∧ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆)))
→ (^{◡}𝐹 ∈ (𝑆 RngHom 𝑅) ∧ ^{◡}𝐹:ran (1^{st} ‘𝑆)–1-1-onto→ran
(1^{st} ‘𝑅))) |
104 | 103 | ex 399 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → ((𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆))
→ (^{◡}𝐹 ∈ (𝑆 RngHom 𝑅) ∧ ^{◡}𝐹:ran (1^{st} ‘𝑆)–1-1-onto→ran
(1^{st} ‘𝑅)))) |
105 | 29, 12, 30, 37 | isrngoiso 34083 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (𝐹 ∈ (𝑅 RngIso 𝑆) ↔ (𝐹 ∈ (𝑅 RngHom 𝑆) ∧ 𝐹:ran (1^{st} ‘𝑅)–1-1-onto→ran
(1^{st} ‘𝑆)))) |
106 | 30, 37, 29, 12 | isrngoiso 34083 |
. . . 4
⊢ ((𝑆 ∈ RingOps ∧ 𝑅 ∈ RingOps) → (^{◡}𝐹 ∈ (𝑆 RngIso 𝑅) ↔ (^{◡}𝐹 ∈ (𝑆 RngHom 𝑅) ∧ ^{◡}𝐹:ran (1^{st} ‘𝑆)–1-1-onto→ran
(1^{st} ‘𝑅)))) |
107 | 106 | ancoms 448 |
. . 3
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (^{◡}𝐹 ∈ (𝑆 RngIso 𝑅) ↔ (^{◡}𝐹 ∈ (𝑆 RngHom 𝑅) ∧ ^{◡}𝐹:ran (1^{st} ‘𝑆)–1-1-onto→ran
(1^{st} ‘𝑅)))) |
108 | 104, 105,
107 | 3imtr4d 285 |
. 2
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps) → (𝐹 ∈ (𝑅 RngIso 𝑆) → ^{◡}𝐹 ∈ (𝑆 RngIso 𝑅))) |
109 | 108 | 3impia 1138 |
1
⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngIso 𝑆)) → ^{◡}𝐹 ∈ (𝑆 RngIso 𝑅)) |