Step | Hyp | Ref
| Expression |
1 | | ghmmhm 17670 |
. . 3
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹 ∈ (𝑆 MndHom 𝑇)) |
2 | | ghmmhm 17670 |
. . 3
⊢ (𝐺 ∈ (𝑆 GrpHom 𝑇) → 𝐺 ∈ (𝑆 MndHom 𝑇)) |
3 | | mhmeql 17364 |
. . 3
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → dom (𝐹 ∩ 𝐺) ∈ (SubMnd‘𝑆)) |
4 | 1, 2, 3 | syl2an 494 |
. 2
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐺 ∈ (𝑆 GrpHom 𝑇)) → dom (𝐹 ∩ 𝐺) ∈ (SubMnd‘𝑆)) |
5 | | ghmgrp1 17662 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑆 ∈ Grp) |
6 | 5 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐺 ∈ (𝑆 GrpHom 𝑇)) → 𝑆 ∈ Grp) |
7 | 6 | adantr 481 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐺 ∈ (𝑆 GrpHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) → 𝑆 ∈ Grp) |
8 | | simprl 794 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐺 ∈ (𝑆 GrpHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) → 𝑥 ∈ (Base‘𝑆)) |
9 | | eqid 2622 |
. . . . . . . . 9
⊢
(Base‘𝑆) =
(Base‘𝑆) |
10 | | eqid 2622 |
. . . . . . . . 9
⊢
(invg‘𝑆) = (invg‘𝑆) |
11 | 9, 10 | grpinvcl 17467 |
. . . . . . . 8
⊢ ((𝑆 ∈ Grp ∧ 𝑥 ∈ (Base‘𝑆)) →
((invg‘𝑆)‘𝑥) ∈ (Base‘𝑆)) |
12 | 7, 8, 11 | syl2anc 693 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐺 ∈ (𝑆 GrpHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) → ((invg‘𝑆)‘𝑥) ∈ (Base‘𝑆)) |
13 | | simprr 796 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐺 ∈ (𝑆 GrpHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) → (𝐹‘𝑥) = (𝐺‘𝑥)) |
14 | 13 | fveq2d 6195 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐺 ∈ (𝑆 GrpHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) → ((invg‘𝑇)‘(𝐹‘𝑥)) = ((invg‘𝑇)‘(𝐺‘𝑥))) |
15 | | eqid 2622 |
. . . . . . . . . 10
⊢
(invg‘𝑇) = (invg‘𝑇) |
16 | 9, 10, 15 | ghminv 17667 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑥 ∈ (Base‘𝑆)) → (𝐹‘((invg‘𝑆)‘𝑥)) = ((invg‘𝑇)‘(𝐹‘𝑥))) |
17 | 16 | ad2ant2r 783 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐺 ∈ (𝑆 GrpHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) → (𝐹‘((invg‘𝑆)‘𝑥)) = ((invg‘𝑇)‘(𝐹‘𝑥))) |
18 | 9, 10, 15 | ghminv 17667 |
. . . . . . . . 9
⊢ ((𝐺 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑥 ∈ (Base‘𝑆)) → (𝐺‘((invg‘𝑆)‘𝑥)) = ((invg‘𝑇)‘(𝐺‘𝑥))) |
19 | 18 | ad2ant2lr 784 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐺 ∈ (𝑆 GrpHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) → (𝐺‘((invg‘𝑆)‘𝑥)) = ((invg‘𝑇)‘(𝐺‘𝑥))) |
20 | 14, 17, 19 | 3eqtr4d 2666 |
. . . . . . 7
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐺 ∈ (𝑆 GrpHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) → (𝐹‘((invg‘𝑆)‘𝑥)) = (𝐺‘((invg‘𝑆)‘𝑥))) |
21 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑦 = ((invg‘𝑆)‘𝑥) → (𝐹‘𝑦) = (𝐹‘((invg‘𝑆)‘𝑥))) |
22 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑦 = ((invg‘𝑆)‘𝑥) → (𝐺‘𝑦) = (𝐺‘((invg‘𝑆)‘𝑥))) |
23 | 21, 22 | eqeq12d 2637 |
. . . . . . . 8
⊢ (𝑦 = ((invg‘𝑆)‘𝑥) → ((𝐹‘𝑦) = (𝐺‘𝑦) ↔ (𝐹‘((invg‘𝑆)‘𝑥)) = (𝐺‘((invg‘𝑆)‘𝑥)))) |
24 | 23 | elrab 3363 |
. . . . . . 7
⊢
(((invg‘𝑆)‘𝑥) ∈ {𝑦 ∈ (Base‘𝑆) ∣ (𝐹‘𝑦) = (𝐺‘𝑦)} ↔ (((invg‘𝑆)‘𝑥) ∈ (Base‘𝑆) ∧ (𝐹‘((invg‘𝑆)‘𝑥)) = (𝐺‘((invg‘𝑆)‘𝑥)))) |
25 | 12, 20, 24 | sylanbrc 698 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐺 ∈ (𝑆 GrpHom 𝑇)) ∧ (𝑥 ∈ (Base‘𝑆) ∧ (𝐹‘𝑥) = (𝐺‘𝑥))) → ((invg‘𝑆)‘𝑥) ∈ {𝑦 ∈ (Base‘𝑆) ∣ (𝐹‘𝑦) = (𝐺‘𝑦)}) |
26 | 25 | expr 643 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐺 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑥 ∈ (Base‘𝑆)) → ((𝐹‘𝑥) = (𝐺‘𝑥) → ((invg‘𝑆)‘𝑥) ∈ {𝑦 ∈ (Base‘𝑆) ∣ (𝐹‘𝑦) = (𝐺‘𝑦)})) |
27 | 26 | ralrimiva 2966 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐺 ∈ (𝑆 GrpHom 𝑇)) → ∀𝑥 ∈ (Base‘𝑆)((𝐹‘𝑥) = (𝐺‘𝑥) → ((invg‘𝑆)‘𝑥) ∈ {𝑦 ∈ (Base‘𝑆) ∣ (𝐹‘𝑦) = (𝐺‘𝑦)})) |
28 | | fveq2 6191 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥)) |
29 | | fveq2 6191 |
. . . . . 6
⊢ (𝑦 = 𝑥 → (𝐺‘𝑦) = (𝐺‘𝑥)) |
30 | 28, 29 | eqeq12d 2637 |
. . . . 5
⊢ (𝑦 = 𝑥 → ((𝐹‘𝑦) = (𝐺‘𝑦) ↔ (𝐹‘𝑥) = (𝐺‘𝑥))) |
31 | 30 | ralrab 3368 |
. . . 4
⊢
(∀𝑥 ∈
{𝑦 ∈ (Base‘𝑆) ∣ (𝐹‘𝑦) = (𝐺‘𝑦)} ((invg‘𝑆)‘𝑥) ∈ {𝑦 ∈ (Base‘𝑆) ∣ (𝐹‘𝑦) = (𝐺‘𝑦)} ↔ ∀𝑥 ∈ (Base‘𝑆)((𝐹‘𝑥) = (𝐺‘𝑥) → ((invg‘𝑆)‘𝑥) ∈ {𝑦 ∈ (Base‘𝑆) ∣ (𝐹‘𝑦) = (𝐺‘𝑦)})) |
32 | 27, 31 | sylibr 224 |
. . 3
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐺 ∈ (𝑆 GrpHom 𝑇)) → ∀𝑥 ∈ {𝑦 ∈ (Base‘𝑆) ∣ (𝐹‘𝑦) = (𝐺‘𝑦)} ((invg‘𝑆)‘𝑥) ∈ {𝑦 ∈ (Base‘𝑆) ∣ (𝐹‘𝑦) = (𝐺‘𝑦)}) |
33 | | eqid 2622 |
. . . . . . . 8
⊢
(Base‘𝑇) =
(Base‘𝑇) |
34 | 9, 33 | ghmf 17664 |
. . . . . . 7
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
35 | 34 | adantr 481 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐺 ∈ (𝑆 GrpHom 𝑇)) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
36 | | ffn 6045 |
. . . . . 6
⊢ (𝐹:(Base‘𝑆)⟶(Base‘𝑇) → 𝐹 Fn (Base‘𝑆)) |
37 | 35, 36 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐺 ∈ (𝑆 GrpHom 𝑇)) → 𝐹 Fn (Base‘𝑆)) |
38 | 9, 33 | ghmf 17664 |
. . . . . . 7
⊢ (𝐺 ∈ (𝑆 GrpHom 𝑇) → 𝐺:(Base‘𝑆)⟶(Base‘𝑇)) |
39 | 38 | adantl 482 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐺 ∈ (𝑆 GrpHom 𝑇)) → 𝐺:(Base‘𝑆)⟶(Base‘𝑇)) |
40 | | ffn 6045 |
. . . . . 6
⊢ (𝐺:(Base‘𝑆)⟶(Base‘𝑇) → 𝐺 Fn (Base‘𝑆)) |
41 | 39, 40 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐺 ∈ (𝑆 GrpHom 𝑇)) → 𝐺 Fn (Base‘𝑆)) |
42 | | fndmin 6324 |
. . . . 5
⊢ ((𝐹 Fn (Base‘𝑆) ∧ 𝐺 Fn (Base‘𝑆)) → dom (𝐹 ∩ 𝐺) = {𝑦 ∈ (Base‘𝑆) ∣ (𝐹‘𝑦) = (𝐺‘𝑦)}) |
43 | 37, 41, 42 | syl2anc 693 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐺 ∈ (𝑆 GrpHom 𝑇)) → dom (𝐹 ∩ 𝐺) = {𝑦 ∈ (Base‘𝑆) ∣ (𝐹‘𝑦) = (𝐺‘𝑦)}) |
44 | | eleq2 2690 |
. . . . 5
⊢ (dom
(𝐹 ∩ 𝐺) = {𝑦 ∈ (Base‘𝑆) ∣ (𝐹‘𝑦) = (𝐺‘𝑦)} → (((invg‘𝑆)‘𝑥) ∈ dom (𝐹 ∩ 𝐺) ↔ ((invg‘𝑆)‘𝑥) ∈ {𝑦 ∈ (Base‘𝑆) ∣ (𝐹‘𝑦) = (𝐺‘𝑦)})) |
45 | 44 | raleqbi1dv 3146 |
. . . 4
⊢ (dom
(𝐹 ∩ 𝐺) = {𝑦 ∈ (Base‘𝑆) ∣ (𝐹‘𝑦) = (𝐺‘𝑦)} → (∀𝑥 ∈ dom (𝐹 ∩ 𝐺)((invg‘𝑆)‘𝑥) ∈ dom (𝐹 ∩ 𝐺) ↔ ∀𝑥 ∈ {𝑦 ∈ (Base‘𝑆) ∣ (𝐹‘𝑦) = (𝐺‘𝑦)} ((invg‘𝑆)‘𝑥) ∈ {𝑦 ∈ (Base‘𝑆) ∣ (𝐹‘𝑦) = (𝐺‘𝑦)})) |
46 | 43, 45 | syl 17 |
. . 3
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐺 ∈ (𝑆 GrpHom 𝑇)) → (∀𝑥 ∈ dom (𝐹 ∩ 𝐺)((invg‘𝑆)‘𝑥) ∈ dom (𝐹 ∩ 𝐺) ↔ ∀𝑥 ∈ {𝑦 ∈ (Base‘𝑆) ∣ (𝐹‘𝑦) = (𝐺‘𝑦)} ((invg‘𝑆)‘𝑥) ∈ {𝑦 ∈ (Base‘𝑆) ∣ (𝐹‘𝑦) = (𝐺‘𝑦)})) |
47 | 32, 46 | mpbird 247 |
. 2
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐺 ∈ (𝑆 GrpHom 𝑇)) → ∀𝑥 ∈ dom (𝐹 ∩ 𝐺)((invg‘𝑆)‘𝑥) ∈ dom (𝐹 ∩ 𝐺)) |
48 | 10 | issubg3 17612 |
. . 3
⊢ (𝑆 ∈ Grp → (dom (𝐹 ∩ 𝐺) ∈ (SubGrp‘𝑆) ↔ (dom (𝐹 ∩ 𝐺) ∈ (SubMnd‘𝑆) ∧ ∀𝑥 ∈ dom (𝐹 ∩ 𝐺)((invg‘𝑆)‘𝑥) ∈ dom (𝐹 ∩ 𝐺)))) |
49 | 6, 48 | syl 17 |
. 2
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐺 ∈ (𝑆 GrpHom 𝑇)) → (dom (𝐹 ∩ 𝐺) ∈ (SubGrp‘𝑆) ↔ (dom (𝐹 ∩ 𝐺) ∈ (SubMnd‘𝑆) ∧ ∀𝑥 ∈ dom (𝐹 ∩ 𝐺)((invg‘𝑆)‘𝑥) ∈ dom (𝐹 ∩ 𝐺)))) |
50 | 4, 47, 49 | mpbir2and 957 |
1
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐺 ∈ (𝑆 GrpHom 𝑇)) → dom (𝐹 ∩ 𝐺) ∈ (SubGrp‘𝑆)) |