Step | Hyp | Ref
| Expression |
1 | | mhmrcl2 18069 |
. . . . 5
⊢ (𝐹 ∈ (𝑅 MndHom 𝑆) → 𝑆 ∈ Mnd) |
2 | | mhmrcl1 18068 |
. . . . 5
⊢ (𝐹 ∈ (𝑅 MndHom 𝑆) → 𝑅 ∈ Mnd) |
3 | 1, 2 | jca 515 |
. . . 4
⊢ (𝐹 ∈ (𝑅 MndHom 𝑆) → (𝑆 ∈ Mnd ∧ 𝑅 ∈ Mnd)) |
4 | 3 | adantr 484 |
. . 3
⊢ ((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶) → (𝑆 ∈ Mnd ∧ 𝑅 ∈ Mnd)) |
5 | | f1ocnv 6624 |
. . . . . 6
⊢ (𝐹:𝐵–1-1-onto→𝐶 → ◡𝐹:𝐶–1-1-onto→𝐵) |
6 | 5 | adantl 485 |
. . . . 5
⊢ ((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶) → ◡𝐹:𝐶–1-1-onto→𝐵) |
7 | | f1of 6612 |
. . . . 5
⊢ (◡𝐹:𝐶–1-1-onto→𝐵 → ◡𝐹:𝐶⟶𝐵) |
8 | 6, 7 | syl 17 |
. . . 4
⊢ ((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶) → ◡𝐹:𝐶⟶𝐵) |
9 | | simpll 767 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝐹 ∈ (𝑅 MndHom 𝑆)) |
10 | 8 | adantr 484 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ◡𝐹:𝐶⟶𝐵) |
11 | | simprl 771 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑥 ∈ 𝐶) |
12 | 10, 11 | ffvelrnd 6856 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (◡𝐹‘𝑥) ∈ 𝐵) |
13 | | simprr 773 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑦 ∈ 𝐶) |
14 | 10, 13 | ffvelrnd 6856 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (◡𝐹‘𝑦) ∈ 𝐵) |
15 | | mhmf1o.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑅) |
16 | | eqid 2738 |
. . . . . . . . 9
⊢
(+g‘𝑅) = (+g‘𝑅) |
17 | | eqid 2738 |
. . . . . . . . 9
⊢
(+g‘𝑆) = (+g‘𝑆) |
18 | 15, 16, 17 | mhmlin 18072 |
. . . . . . . 8
⊢ ((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ (◡𝐹‘𝑥) ∈ 𝐵 ∧ (◡𝐹‘𝑦) ∈ 𝐵) → (𝐹‘((◡𝐹‘𝑥)(+g‘𝑅)(◡𝐹‘𝑦))) = ((𝐹‘(◡𝐹‘𝑥))(+g‘𝑆)(𝐹‘(◡𝐹‘𝑦)))) |
19 | 9, 12, 14, 18 | syl3anc 1372 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝐹‘((◡𝐹‘𝑥)(+g‘𝑅)(◡𝐹‘𝑦))) = ((𝐹‘(◡𝐹‘𝑥))(+g‘𝑆)(𝐹‘(◡𝐹‘𝑦)))) |
20 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶) → 𝐹:𝐵–1-1-onto→𝐶) |
21 | 20 | adantr 484 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝐹:𝐵–1-1-onto→𝐶) |
22 | | f1ocnvfv2 7039 |
. . . . . . . . 9
⊢ ((𝐹:𝐵–1-1-onto→𝐶 ∧ 𝑥 ∈ 𝐶) → (𝐹‘(◡𝐹‘𝑥)) = 𝑥) |
23 | 21, 11, 22 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝐹‘(◡𝐹‘𝑥)) = 𝑥) |
24 | | f1ocnvfv2 7039 |
. . . . . . . . 9
⊢ ((𝐹:𝐵–1-1-onto→𝐶 ∧ 𝑦 ∈ 𝐶) → (𝐹‘(◡𝐹‘𝑦)) = 𝑦) |
25 | 21, 13, 24 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝐹‘(◡𝐹‘𝑦)) = 𝑦) |
26 | 23, 25 | oveq12d 7182 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝐹‘(◡𝐹‘𝑥))(+g‘𝑆)(𝐹‘(◡𝐹‘𝑦))) = (𝑥(+g‘𝑆)𝑦)) |
27 | 19, 26 | eqtrd 2773 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝐹‘((◡𝐹‘𝑥)(+g‘𝑅)(◡𝐹‘𝑦))) = (𝑥(+g‘𝑆)𝑦)) |
28 | 2 | adantr 484 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶) → 𝑅 ∈ Mnd) |
29 | 28 | adantr 484 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → 𝑅 ∈ Mnd) |
30 | 15, 16 | mndcl 18028 |
. . . . . . . 8
⊢ ((𝑅 ∈ Mnd ∧ (◡𝐹‘𝑥) ∈ 𝐵 ∧ (◡𝐹‘𝑦) ∈ 𝐵) → ((◡𝐹‘𝑥)(+g‘𝑅)(◡𝐹‘𝑦)) ∈ 𝐵) |
31 | 29, 12, 14, 30 | syl3anc 1372 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((◡𝐹‘𝑥)(+g‘𝑅)(◡𝐹‘𝑦)) ∈ 𝐵) |
32 | | f1ocnvfv 7040 |
. . . . . . 7
⊢ ((𝐹:𝐵–1-1-onto→𝐶 ∧ ((◡𝐹‘𝑥)(+g‘𝑅)(◡𝐹‘𝑦)) ∈ 𝐵) → ((𝐹‘((◡𝐹‘𝑥)(+g‘𝑅)(◡𝐹‘𝑦))) = (𝑥(+g‘𝑆)𝑦) → (◡𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((◡𝐹‘𝑥)(+g‘𝑅)(◡𝐹‘𝑦)))) |
33 | 21, 31, 32 | syl2anc 587 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → ((𝐹‘((◡𝐹‘𝑥)(+g‘𝑅)(◡𝐹‘𝑦))) = (𝑥(+g‘𝑆)𝑦) → (◡𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((◡𝐹‘𝑥)(+g‘𝑅)(◡𝐹‘𝑦)))) |
34 | 27, 33 | mpd 15 |
. . . . 5
⊢ (((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶) ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (◡𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((◡𝐹‘𝑥)(+g‘𝑅)(◡𝐹‘𝑦))) |
35 | 34 | ralrimivva 3103 |
. . . 4
⊢ ((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶) → ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (◡𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((◡𝐹‘𝑥)(+g‘𝑅)(◡𝐹‘𝑦))) |
36 | | eqid 2738 |
. . . . . . . . 9
⊢
(0g‘𝑅) = (0g‘𝑅) |
37 | | eqid 2738 |
. . . . . . . . 9
⊢
(0g‘𝑆) = (0g‘𝑆) |
38 | 36, 37 | mhm0 18073 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝑅 MndHom 𝑆) → (𝐹‘(0g‘𝑅)) = (0g‘𝑆)) |
39 | 38 | adantr 484 |
. . . . . . 7
⊢ ((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶) → (𝐹‘(0g‘𝑅)) = (0g‘𝑆)) |
40 | 39 | eqcomd 2744 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶) →
(0g‘𝑆) =
(𝐹‘(0g‘𝑅))) |
41 | 40 | fveq2d 6672 |
. . . . 5
⊢ ((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶) → (◡𝐹‘(0g‘𝑆)) = (◡𝐹‘(𝐹‘(0g‘𝑅)))) |
42 | 15, 36 | mndidcl 18035 |
. . . . . . . 8
⊢ (𝑅 ∈ Mnd →
(0g‘𝑅)
∈ 𝐵) |
43 | 2, 42 | syl 17 |
. . . . . . 7
⊢ (𝐹 ∈ (𝑅 MndHom 𝑆) → (0g‘𝑅) ∈ 𝐵) |
44 | 43 | adantr 484 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶) →
(0g‘𝑅)
∈ 𝐵) |
45 | | f1ocnvfv1 7038 |
. . . . . 6
⊢ ((𝐹:𝐵–1-1-onto→𝐶 ∧
(0g‘𝑅)
∈ 𝐵) → (◡𝐹‘(𝐹‘(0g‘𝑅))) = (0g‘𝑅)) |
46 | 20, 44, 45 | syl2anc 587 |
. . . . 5
⊢ ((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶) → (◡𝐹‘(𝐹‘(0g‘𝑅))) = (0g‘𝑅)) |
47 | 41, 46 | eqtrd 2773 |
. . . 4
⊢ ((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶) → (◡𝐹‘(0g‘𝑆)) = (0g‘𝑅)) |
48 | 8, 35, 47 | 3jca 1129 |
. . 3
⊢ ((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶) → (◡𝐹:𝐶⟶𝐵 ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (◡𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((◡𝐹‘𝑥)(+g‘𝑅)(◡𝐹‘𝑦)) ∧ (◡𝐹‘(0g‘𝑆)) = (0g‘𝑅))) |
49 | | mhmf1o.c |
. . . 4
⊢ 𝐶 = (Base‘𝑆) |
50 | 49, 15, 17, 16, 37, 36 | ismhm 18067 |
. . 3
⊢ (◡𝐹 ∈ (𝑆 MndHom 𝑅) ↔ ((𝑆 ∈ Mnd ∧ 𝑅 ∈ Mnd) ∧ (◡𝐹:𝐶⟶𝐵 ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (◡𝐹‘(𝑥(+g‘𝑆)𝑦)) = ((◡𝐹‘𝑥)(+g‘𝑅)(◡𝐹‘𝑦)) ∧ (◡𝐹‘(0g‘𝑆)) = (0g‘𝑅)))) |
51 | 4, 48, 50 | sylanbrc 586 |
. 2
⊢ ((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶) → ◡𝐹 ∈ (𝑆 MndHom 𝑅)) |
52 | 15, 49 | mhmf 18070 |
. . . . 5
⊢ (𝐹 ∈ (𝑅 MndHom 𝑆) → 𝐹:𝐵⟶𝐶) |
53 | 52 | adantr 484 |
. . . 4
⊢ ((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ ◡𝐹 ∈ (𝑆 MndHom 𝑅)) → 𝐹:𝐵⟶𝐶) |
54 | 53 | ffnd 6499 |
. . 3
⊢ ((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ ◡𝐹 ∈ (𝑆 MndHom 𝑅)) → 𝐹 Fn 𝐵) |
55 | 49, 15 | mhmf 18070 |
. . . . 5
⊢ (◡𝐹 ∈ (𝑆 MndHom 𝑅) → ◡𝐹:𝐶⟶𝐵) |
56 | 55 | adantl 485 |
. . . 4
⊢ ((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ ◡𝐹 ∈ (𝑆 MndHom 𝑅)) → ◡𝐹:𝐶⟶𝐵) |
57 | 56 | ffnd 6499 |
. . 3
⊢ ((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ ◡𝐹 ∈ (𝑆 MndHom 𝑅)) → ◡𝐹 Fn 𝐶) |
58 | | dff1o4 6620 |
. . 3
⊢ (𝐹:𝐵–1-1-onto→𝐶 ↔ (𝐹 Fn 𝐵 ∧ ◡𝐹 Fn 𝐶)) |
59 | 54, 57, 58 | sylanbrc 586 |
. 2
⊢ ((𝐹 ∈ (𝑅 MndHom 𝑆) ∧ ◡𝐹 ∈ (𝑆 MndHom 𝑅)) → 𝐹:𝐵–1-1-onto→𝐶) |
60 | 51, 59 | impbida 801 |
1
⊢ (𝐹 ∈ (𝑅 MndHom 𝑆) → (𝐹:𝐵–1-1-onto→𝐶 ↔ ◡𝐹 ∈ (𝑆 MndHom 𝑅))) |