Step | Hyp | Ref
| Expression |
1 | | lmghm 19031 |
. . 3
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) |
2 | | lmghm 19031 |
. . 3
⊢ (𝐺 ∈ (𝑆 LMHom 𝑇) → 𝐺 ∈ (𝑆 GrpHom 𝑇)) |
3 | | ghmeql 17683 |
. . 3
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐺 ∈ (𝑆 GrpHom 𝑇)) → dom (𝐹 ∩ 𝐺) ∈ (SubGrp‘𝑆)) |
4 | 1, 2, 3 | syl2an 494 |
. 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐺 ∈ (𝑆 LMHom 𝑇)) → dom (𝐹 ∩ 𝐺) ∈ (SubGrp‘𝑆)) |
5 | | lmhmlmod1 19033 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑆 ∈ LMod) |
6 | 5 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐺 ∈ (𝑆 LMHom 𝑇)) → 𝑆 ∈ LMod) |
7 | 6 | ad2antrr 762 |
. . . . . . . 8
⊢ ((((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐺 ∈ (𝑆 LMHom 𝑇)) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑆))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → 𝑆 ∈ LMod) |
8 | | simplr 792 |
. . . . . . . 8
⊢ ((((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐺 ∈ (𝑆 LMHom 𝑇)) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑆))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → 𝑥 ∈ (Base‘(Scalar‘𝑆))) |
9 | | simprl 794 |
. . . . . . . 8
⊢ ((((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐺 ∈ (𝑆 LMHom 𝑇)) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑆))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → 𝑦 ∈ (Base‘𝑆)) |
10 | | eqid 2622 |
. . . . . . . . 9
⊢
(Base‘𝑆) =
(Base‘𝑆) |
11 | | eqid 2622 |
. . . . . . . . 9
⊢
(Scalar‘𝑆) =
(Scalar‘𝑆) |
12 | | eqid 2622 |
. . . . . . . . 9
⊢ (
·𝑠 ‘𝑆) = ( ·𝑠
‘𝑆) |
13 | | eqid 2622 |
. . . . . . . . 9
⊢
(Base‘(Scalar‘𝑆)) = (Base‘(Scalar‘𝑆)) |
14 | 10, 11, 12, 13 | lmodvscl 18880 |
. . . . . . . 8
⊢ ((𝑆 ∈ LMod ∧ 𝑥 ∈
(Base‘(Scalar‘𝑆)) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝑥( ·𝑠
‘𝑆)𝑦) ∈ (Base‘𝑆)) |
15 | 7, 8, 9, 14 | syl3anc 1326 |
. . . . . . 7
⊢ ((((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐺 ∈ (𝑆 LMHom 𝑇)) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑆))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → (𝑥( ·𝑠
‘𝑆)𝑦) ∈ (Base‘𝑆)) |
16 | | oveq2 6658 |
. . . . . . . . 9
⊢ ((𝐹‘𝑦) = (𝐺‘𝑦) → (𝑥( ·𝑠
‘𝑇)(𝐹‘𝑦)) = (𝑥( ·𝑠
‘𝑇)(𝐺‘𝑦))) |
17 | 16 | ad2antll 765 |
. . . . . . . 8
⊢ ((((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐺 ∈ (𝑆 LMHom 𝑇)) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑆))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → (𝑥( ·𝑠
‘𝑇)(𝐹‘𝑦)) = (𝑥( ·𝑠
‘𝑇)(𝐺‘𝑦))) |
18 | | simplll 798 |
. . . . . . . . 9
⊢ ((((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐺 ∈ (𝑆 LMHom 𝑇)) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑆))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → 𝐹 ∈ (𝑆 LMHom 𝑇)) |
19 | | eqid 2622 |
. . . . . . . . . 10
⊢ (
·𝑠 ‘𝑇) = ( ·𝑠
‘𝑇) |
20 | 11, 13, 10, 12, 19 | lmhmlin 19035 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝐹‘(𝑥( ·𝑠
‘𝑆)𝑦)) = (𝑥( ·𝑠
‘𝑇)(𝐹‘𝑦))) |
21 | 18, 8, 9, 20 | syl3anc 1326 |
. . . . . . . 8
⊢ ((((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐺 ∈ (𝑆 LMHom 𝑇)) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑆))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → (𝐹‘(𝑥( ·𝑠
‘𝑆)𝑦)) = (𝑥( ·𝑠
‘𝑇)(𝐹‘𝑦))) |
22 | | simpllr 799 |
. . . . . . . . 9
⊢ ((((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐺 ∈ (𝑆 LMHom 𝑇)) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑆))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → 𝐺 ∈ (𝑆 LMHom 𝑇)) |
23 | 11, 13, 10, 12, 19 | lmhmlin 19035 |
. . . . . . . . 9
⊢ ((𝐺 ∈ (𝑆 LMHom 𝑇) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑆)) ∧ 𝑦 ∈ (Base‘𝑆)) → (𝐺‘(𝑥( ·𝑠
‘𝑆)𝑦)) = (𝑥( ·𝑠
‘𝑇)(𝐺‘𝑦))) |
24 | 22, 8, 9, 23 | syl3anc 1326 |
. . . . . . . 8
⊢ ((((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐺 ∈ (𝑆 LMHom 𝑇)) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑆))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → (𝐺‘(𝑥( ·𝑠
‘𝑆)𝑦)) = (𝑥( ·𝑠
‘𝑇)(𝐺‘𝑦))) |
25 | 17, 21, 24 | 3eqtr4d 2666 |
. . . . . . 7
⊢ ((((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐺 ∈ (𝑆 LMHom 𝑇)) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑆))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → (𝐹‘(𝑥( ·𝑠
‘𝑆)𝑦)) = (𝐺‘(𝑥( ·𝑠
‘𝑆)𝑦))) |
26 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑧 = (𝑥( ·𝑠
‘𝑆)𝑦) → (𝐹‘𝑧) = (𝐹‘(𝑥( ·𝑠
‘𝑆)𝑦))) |
27 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑧 = (𝑥( ·𝑠
‘𝑆)𝑦) → (𝐺‘𝑧) = (𝐺‘(𝑥( ·𝑠
‘𝑆)𝑦))) |
28 | 26, 27 | eqeq12d 2637 |
. . . . . . . 8
⊢ (𝑧 = (𝑥( ·𝑠
‘𝑆)𝑦) → ((𝐹‘𝑧) = (𝐺‘𝑧) ↔ (𝐹‘(𝑥( ·𝑠
‘𝑆)𝑦)) = (𝐺‘(𝑥( ·𝑠
‘𝑆)𝑦)))) |
29 | 28 | elrab 3363 |
. . . . . . 7
⊢ ((𝑥(
·𝑠 ‘𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)} ↔ ((𝑥( ·𝑠
‘𝑆)𝑦) ∈ (Base‘𝑆) ∧ (𝐹‘(𝑥( ·𝑠
‘𝑆)𝑦)) = (𝐺‘(𝑥( ·𝑠
‘𝑆)𝑦)))) |
30 | 15, 25, 29 | sylanbrc 698 |
. . . . . 6
⊢ ((((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐺 ∈ (𝑆 LMHom 𝑇)) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑆))) ∧ (𝑦 ∈ (Base‘𝑆) ∧ (𝐹‘𝑦) = (𝐺‘𝑦))) → (𝑥( ·𝑠
‘𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)}) |
31 | 30 | expr 643 |
. . . . 5
⊢ ((((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐺 ∈ (𝑆 LMHom 𝑇)) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑆))) ∧ 𝑦 ∈ (Base‘𝑆)) → ((𝐹‘𝑦) = (𝐺‘𝑦) → (𝑥( ·𝑠
‘𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)})) |
32 | 31 | ralrimiva 2966 |
. . . 4
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐺 ∈ (𝑆 LMHom 𝑇)) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑆))) → ∀𝑦 ∈ (Base‘𝑆)((𝐹‘𝑦) = (𝐺‘𝑦) → (𝑥( ·𝑠
‘𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)})) |
33 | | eqid 2622 |
. . . . . . . . 9
⊢
(Base‘𝑇) =
(Base‘𝑇) |
34 | 10, 33 | lmhmf 19034 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹:(Base‘𝑆)⟶(Base‘𝑇)) |
35 | | ffn 6045 |
. . . . . . . 8
⊢ (𝐹:(Base‘𝑆)⟶(Base‘𝑇) → 𝐹 Fn (Base‘𝑆)) |
36 | 34, 35 | syl 17 |
. . . . . . 7
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹 Fn (Base‘𝑆)) |
37 | 10, 33 | lmhmf 19034 |
. . . . . . . 8
⊢ (𝐺 ∈ (𝑆 LMHom 𝑇) → 𝐺:(Base‘𝑆)⟶(Base‘𝑇)) |
38 | | ffn 6045 |
. . . . . . . 8
⊢ (𝐺:(Base‘𝑆)⟶(Base‘𝑇) → 𝐺 Fn (Base‘𝑆)) |
39 | 37, 38 | syl 17 |
. . . . . . 7
⊢ (𝐺 ∈ (𝑆 LMHom 𝑇) → 𝐺 Fn (Base‘𝑆)) |
40 | | fndmin 6324 |
. . . . . . 7
⊢ ((𝐹 Fn (Base‘𝑆) ∧ 𝐺 Fn (Base‘𝑆)) → dom (𝐹 ∩ 𝐺) = {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)}) |
41 | 36, 39, 40 | syl2an 494 |
. . . . . 6
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐺 ∈ (𝑆 LMHom 𝑇)) → dom (𝐹 ∩ 𝐺) = {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)}) |
42 | 41 | adantr 481 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐺 ∈ (𝑆 LMHom 𝑇)) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑆))) → dom (𝐹 ∩ 𝐺) = {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)}) |
43 | | eleq2 2690 |
. . . . . . 7
⊢ (dom
(𝐹 ∩ 𝐺) = {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)} → ((𝑥( ·𝑠
‘𝑆)𝑦) ∈ dom (𝐹 ∩ 𝐺) ↔ (𝑥( ·𝑠
‘𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)})) |
44 | 43 | raleqbi1dv 3146 |
. . . . . 6
⊢ (dom
(𝐹 ∩ 𝐺) = {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)} → (∀𝑦 ∈ dom (𝐹 ∩ 𝐺)(𝑥( ·𝑠
‘𝑆)𝑦) ∈ dom (𝐹 ∩ 𝐺) ↔ ∀𝑦 ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)} (𝑥( ·𝑠
‘𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)})) |
45 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑧 = 𝑦 → (𝐹‘𝑧) = (𝐹‘𝑦)) |
46 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑧 = 𝑦 → (𝐺‘𝑧) = (𝐺‘𝑦)) |
47 | 45, 46 | eqeq12d 2637 |
. . . . . . 7
⊢ (𝑧 = 𝑦 → ((𝐹‘𝑧) = (𝐺‘𝑧) ↔ (𝐹‘𝑦) = (𝐺‘𝑦))) |
48 | 47 | ralrab 3368 |
. . . . . 6
⊢
(∀𝑦 ∈
{𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)} (𝑥( ·𝑠
‘𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)} ↔ ∀𝑦 ∈ (Base‘𝑆)((𝐹‘𝑦) = (𝐺‘𝑦) → (𝑥( ·𝑠
‘𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)})) |
49 | 44, 48 | syl6bb 276 |
. . . . 5
⊢ (dom
(𝐹 ∩ 𝐺) = {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)} → (∀𝑦 ∈ dom (𝐹 ∩ 𝐺)(𝑥( ·𝑠
‘𝑆)𝑦) ∈ dom (𝐹 ∩ 𝐺) ↔ ∀𝑦 ∈ (Base‘𝑆)((𝐹‘𝑦) = (𝐺‘𝑦) → (𝑥( ·𝑠
‘𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)}))) |
50 | 42, 49 | syl 17 |
. . . 4
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐺 ∈ (𝑆 LMHom 𝑇)) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑆))) → (∀𝑦 ∈ dom (𝐹 ∩ 𝐺)(𝑥( ·𝑠
‘𝑆)𝑦) ∈ dom (𝐹 ∩ 𝐺) ↔ ∀𝑦 ∈ (Base‘𝑆)((𝐹‘𝑦) = (𝐺‘𝑦) → (𝑥( ·𝑠
‘𝑆)𝑦) ∈ {𝑧 ∈ (Base‘𝑆) ∣ (𝐹‘𝑧) = (𝐺‘𝑧)}))) |
51 | 32, 50 | mpbird 247 |
. . 3
⊢ (((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐺 ∈ (𝑆 LMHom 𝑇)) ∧ 𝑥 ∈ (Base‘(Scalar‘𝑆))) → ∀𝑦 ∈ dom (𝐹 ∩ 𝐺)(𝑥( ·𝑠
‘𝑆)𝑦) ∈ dom (𝐹 ∩ 𝐺)) |
52 | 51 | ralrimiva 2966 |
. 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐺 ∈ (𝑆 LMHom 𝑇)) → ∀𝑥 ∈ (Base‘(Scalar‘𝑆))∀𝑦 ∈ dom (𝐹 ∩ 𝐺)(𝑥( ·𝑠
‘𝑆)𝑦) ∈ dom (𝐹 ∩ 𝐺)) |
53 | | lmhmeql.u |
. . . 4
⊢ 𝑈 = (LSubSp‘𝑆) |
54 | 11, 13, 10, 12, 53 | islss4 18962 |
. . 3
⊢ (𝑆 ∈ LMod → (dom (𝐹 ∩ 𝐺) ∈ 𝑈 ↔ (dom (𝐹 ∩ 𝐺) ∈ (SubGrp‘𝑆) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑆))∀𝑦 ∈ dom (𝐹 ∩ 𝐺)(𝑥( ·𝑠
‘𝑆)𝑦) ∈ dom (𝐹 ∩ 𝐺)))) |
55 | 6, 54 | syl 17 |
. 2
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐺 ∈ (𝑆 LMHom 𝑇)) → (dom (𝐹 ∩ 𝐺) ∈ 𝑈 ↔ (dom (𝐹 ∩ 𝐺) ∈ (SubGrp‘𝑆) ∧ ∀𝑥 ∈ (Base‘(Scalar‘𝑆))∀𝑦 ∈ dom (𝐹 ∩ 𝐺)(𝑥( ·𝑠
‘𝑆)𝑦) ∈ dom (𝐹 ∩ 𝐺)))) |
56 | 4, 52, 55 | mpbir2and 957 |
1
⊢ ((𝐹 ∈ (𝑆 LMHom 𝑇) ∧ 𝐺 ∈ (𝑆 LMHom 𝑇)) → dom (𝐹 ∩ 𝐺) ∈ 𝑈) |