Step |
Hyp |
Ref |
Expression |
1 |
|
resmgmhm.u |
⊢ 𝑈 = ( 𝑆 ↾s 𝑋 ) |
2 |
|
mgmhmrcl |
⊢ ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) → ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm ) ) |
3 |
2
|
simprd |
⊢ ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) → 𝑇 ∈ Mgm ) |
4 |
1
|
submgmmgm |
⊢ ( 𝑋 ∈ ( SubMgm ‘ 𝑆 ) → 𝑈 ∈ Mgm ) |
5 |
3 4
|
anim12ci |
⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( 𝑈 ∈ Mgm ∧ 𝑇 ∈ Mgm ) ) |
6 |
|
eqid |
⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 ) |
7 |
|
eqid |
⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 ) |
8 |
6 7
|
mgmhmf |
⊢ ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) ) |
9 |
6
|
submgmss |
⊢ ( 𝑋 ∈ ( SubMgm ‘ 𝑆 ) → 𝑋 ⊆ ( Base ‘ 𝑆 ) ) |
10 |
|
fssres |
⊢ ( ( 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) ∧ 𝑋 ⊆ ( Base ‘ 𝑆 ) ) → ( 𝐹 ↾ 𝑋 ) : 𝑋 ⟶ ( Base ‘ 𝑇 ) ) |
11 |
8 9 10
|
syl2an |
⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( 𝐹 ↾ 𝑋 ) : 𝑋 ⟶ ( Base ‘ 𝑇 ) ) |
12 |
9
|
adantl |
⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → 𝑋 ⊆ ( Base ‘ 𝑆 ) ) |
13 |
1 6
|
ressbas2 |
⊢ ( 𝑋 ⊆ ( Base ‘ 𝑆 ) → 𝑋 = ( Base ‘ 𝑈 ) ) |
14 |
12 13
|
syl |
⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → 𝑋 = ( Base ‘ 𝑈 ) ) |
15 |
14
|
feq2d |
⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( ( 𝐹 ↾ 𝑋 ) : 𝑋 ⟶ ( Base ‘ 𝑇 ) ↔ ( 𝐹 ↾ 𝑋 ) : ( Base ‘ 𝑈 ) ⟶ ( Base ‘ 𝑇 ) ) ) |
16 |
11 15
|
mpbid |
⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( 𝐹 ↾ 𝑋 ) : ( Base ‘ 𝑈 ) ⟶ ( Base ‘ 𝑇 ) ) |
17 |
|
simpll |
⊢ ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ) |
18 |
9
|
ad2antlr |
⊢ ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑋 ⊆ ( Base ‘ 𝑆 ) ) |
19 |
|
simprl |
⊢ ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑥 ∈ 𝑋 ) |
20 |
18 19
|
sseldd |
⊢ ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑥 ∈ ( Base ‘ 𝑆 ) ) |
21 |
|
simprr |
⊢ ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑦 ∈ 𝑋 ) |
22 |
18 21
|
sseldd |
⊢ ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑦 ∈ ( Base ‘ 𝑆 ) ) |
23 |
|
eqid |
⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 ) |
24 |
|
eqid |
⊢ ( +g ‘ 𝑇 ) = ( +g ‘ 𝑇 ) |
25 |
6 23 24
|
mgmhmlin |
⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) ) |
26 |
17 20 22 25
|
syl3anc |
⊢ ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) ) |
27 |
23
|
submgmcl |
⊢ ( ( 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ 𝑋 ) |
28 |
27
|
3expb |
⊢ ( ( 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ 𝑋 ) |
29 |
28
|
adantll |
⊢ ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ 𝑋 ) |
30 |
|
fvres |
⊢ ( ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ 𝑋 → ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) ) |
31 |
29 30
|
syl |
⊢ ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) ) |
32 |
|
fvres |
⊢ ( 𝑥 ∈ 𝑋 → ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) |
33 |
|
fvres |
⊢ ( 𝑦 ∈ 𝑋 → ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) ) |
34 |
32 33
|
oveqan12d |
⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) ) |
35 |
34
|
adantl |
⊢ ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) ) |
36 |
26 31 35
|
3eqtr4d |
⊢ ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) ) |
37 |
36
|
ralrimivva |
⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) ) |
38 |
1 23
|
ressplusg |
⊢ ( 𝑋 ∈ ( SubMgm ‘ 𝑆 ) → ( +g ‘ 𝑆 ) = ( +g ‘ 𝑈 ) ) |
39 |
38
|
adantl |
⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( +g ‘ 𝑆 ) = ( +g ‘ 𝑈 ) ) |
40 |
39
|
oveqd |
⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) ) |
41 |
40
|
fveqeq2d |
⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) ↔ ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) ) ) |
42 |
14 41
|
raleqbidv |
⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝑈 ) ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) ) ) |
43 |
14 42
|
raleqbidv |
⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑈 ) ∀ 𝑦 ∈ ( Base ‘ 𝑈 ) ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) ) ) |
44 |
37 43
|
mpbid |
⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝑈 ) ∀ 𝑦 ∈ ( Base ‘ 𝑈 ) ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) ) |
45 |
16 44
|
jca |
⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( ( 𝐹 ↾ 𝑋 ) : ( Base ‘ 𝑈 ) ⟶ ( Base ‘ 𝑇 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑈 ) ∀ 𝑦 ∈ ( Base ‘ 𝑈 ) ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) ) ) |
46 |
|
eqid |
⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 ) |
47 |
|
eqid |
⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 ) |
48 |
46 7 47 24
|
ismgmhm |
⊢ ( ( 𝐹 ↾ 𝑋 ) ∈ ( 𝑈 MgmHom 𝑇 ) ↔ ( ( 𝑈 ∈ Mgm ∧ 𝑇 ∈ Mgm ) ∧ ( ( 𝐹 ↾ 𝑋 ) : ( Base ‘ 𝑈 ) ⟶ ( Base ‘ 𝑇 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑈 ) ∀ 𝑦 ∈ ( Base ‘ 𝑈 ) ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) ) ) ) |
49 |
5 45 48
|
sylanbrc |
⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑋 ∈ ( SubMgm ‘ 𝑆 ) ) → ( 𝐹 ↾ 𝑋 ) ∈ ( 𝑈 MgmHom 𝑇 ) ) |