Step |
Hyp |
Ref |
Expression |
1 |
|
gasubg.1 |
⊢ 𝐻 = ( 𝐺 ↾s 𝑆 ) |
2 |
|
gaset |
⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → 𝑌 ∈ V ) |
3 |
1
|
subggrp |
⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐻 ∈ Grp ) |
4 |
2 3
|
anim12ci |
⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝐻 ∈ Grp ∧ 𝑌 ∈ V ) ) |
5 |
|
eqid |
⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 ) |
6 |
5
|
gaf |
⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) → ⊕ : ( ( Base ‘ 𝐺 ) × 𝑌 ) ⟶ 𝑌 ) |
7 |
6
|
adantr |
⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ⊕ : ( ( Base ‘ 𝐺 ) × 𝑌 ) ⟶ 𝑌 ) |
8 |
|
simpr |
⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) |
9 |
5
|
subgss |
⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) ) |
10 |
8 9
|
syl |
⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) ) |
11 |
|
xpss1 |
⊢ ( 𝑆 ⊆ ( Base ‘ 𝐺 ) → ( 𝑆 × 𝑌 ) ⊆ ( ( Base ‘ 𝐺 ) × 𝑌 ) ) |
12 |
10 11
|
syl |
⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑆 × 𝑌 ) ⊆ ( ( Base ‘ 𝐺 ) × 𝑌 ) ) |
13 |
7 12
|
fssresd |
⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) : ( 𝑆 × 𝑌 ) ⟶ 𝑌 ) |
14 |
1
|
subgbas |
⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 = ( Base ‘ 𝐻 ) ) |
15 |
8 14
|
syl |
⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → 𝑆 = ( Base ‘ 𝐻 ) ) |
16 |
15
|
xpeq1d |
⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( 𝑆 × 𝑌 ) = ( ( Base ‘ 𝐻 ) × 𝑌 ) ) |
17 |
16
|
feq2d |
⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) : ( 𝑆 × 𝑌 ) ⟶ 𝑌 ↔ ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) : ( ( Base ‘ 𝐻 ) × 𝑌 ) ⟶ 𝑌 ) ) |
18 |
13 17
|
mpbid |
⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) : ( ( Base ‘ 𝐻 ) × 𝑌 ) ⟶ 𝑌 ) |
19 |
8
|
adantr |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) → 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) |
20 |
|
eqid |
⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 ) |
21 |
20
|
subg0cl |
⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) ∈ 𝑆 ) |
22 |
19 21
|
syl |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) → ( 0g ‘ 𝐺 ) ∈ 𝑆 ) |
23 |
|
simpr |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) → 𝑥 ∈ 𝑌 ) |
24 |
|
ovres |
⊢ ( ( ( 0g ‘ 𝐺 ) ∈ 𝑆 ∧ 𝑥 ∈ 𝑌 ) → ( ( 0g ‘ 𝐺 ) ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = ( ( 0g ‘ 𝐺 ) ⊕ 𝑥 ) ) |
25 |
22 23 24
|
syl2anc |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) → ( ( 0g ‘ 𝐺 ) ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = ( ( 0g ‘ 𝐺 ) ⊕ 𝑥 ) ) |
26 |
1 20
|
subg0 |
⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐻 ) ) |
27 |
19 26
|
syl |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) → ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐻 ) ) |
28 |
27
|
oveq1d |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) → ( ( 0g ‘ 𝐺 ) ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = ( ( 0g ‘ 𝐻 ) ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) ) |
29 |
20
|
gagrpid |
⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑥 ∈ 𝑌 ) → ( ( 0g ‘ 𝐺 ) ⊕ 𝑥 ) = 𝑥 ) |
30 |
29
|
adantlr |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) → ( ( 0g ‘ 𝐺 ) ⊕ 𝑥 ) = 𝑥 ) |
31 |
25 28 30
|
3eqtr3d |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) → ( ( 0g ‘ 𝐻 ) ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = 𝑥 ) |
32 |
|
eqimss2 |
⊢ ( 𝑆 = ( Base ‘ 𝐻 ) → ( Base ‘ 𝐻 ) ⊆ 𝑆 ) |
33 |
15 32
|
syl |
⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( Base ‘ 𝐻 ) ⊆ 𝑆 ) |
34 |
33
|
adantr |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) → ( Base ‘ 𝐻 ) ⊆ 𝑆 ) |
35 |
34
|
sselda |
⊢ ( ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑦 ∈ ( Base ‘ 𝐻 ) ) → 𝑦 ∈ 𝑆 ) |
36 |
34
|
sselda |
⊢ ( ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ 𝑧 ∈ ( Base ‘ 𝐻 ) ) → 𝑧 ∈ 𝑆 ) |
37 |
35 36
|
anim12dan |
⊢ ( ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐻 ) ∧ 𝑧 ∈ ( Base ‘ 𝐻 ) ) ) → ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) |
38 |
|
simprl |
⊢ ( ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑦 ∈ 𝑆 ) |
39 |
7
|
ad2antrr |
⊢ ( ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ⊕ : ( ( Base ‘ 𝐺 ) × 𝑌 ) ⟶ 𝑌 ) |
40 |
9
|
ad3antlr |
⊢ ( ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑆 ⊆ ( Base ‘ 𝐺 ) ) |
41 |
|
simprr |
⊢ ( ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑧 ∈ 𝑆 ) |
42 |
40 41
|
sseldd |
⊢ ( ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑧 ∈ ( Base ‘ 𝐺 ) ) |
43 |
23
|
adantr |
⊢ ( ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑥 ∈ 𝑌 ) |
44 |
39 42 43
|
fovrnd |
⊢ ( ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( 𝑧 ⊕ 𝑥 ) ∈ 𝑌 ) |
45 |
|
ovres |
⊢ ( ( 𝑦 ∈ 𝑆 ∧ ( 𝑧 ⊕ 𝑥 ) ∈ 𝑌 ) → ( 𝑦 ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) ( 𝑧 ⊕ 𝑥 ) ) = ( 𝑦 ⊕ ( 𝑧 ⊕ 𝑥 ) ) ) |
46 |
38 44 45
|
syl2anc |
⊢ ( ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( 𝑦 ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) ( 𝑧 ⊕ 𝑥 ) ) = ( 𝑦 ⊕ ( 𝑧 ⊕ 𝑥 ) ) ) |
47 |
|
ovres |
⊢ ( ( 𝑧 ∈ 𝑆 ∧ 𝑥 ∈ 𝑌 ) → ( 𝑧 ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = ( 𝑧 ⊕ 𝑥 ) ) |
48 |
41 43 47
|
syl2anc |
⊢ ( ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( 𝑧 ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = ( 𝑧 ⊕ 𝑥 ) ) |
49 |
48
|
oveq2d |
⊢ ( ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( 𝑦 ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) ( 𝑧 ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) ) = ( 𝑦 ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) ( 𝑧 ⊕ 𝑥 ) ) ) |
50 |
|
simplll |
⊢ ( ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ) |
51 |
40 38
|
sseldd |
⊢ ( ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑦 ∈ ( Base ‘ 𝐺 ) ) |
52 |
|
eqid |
⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 ) |
53 |
5 52
|
gaass |
⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐺 ) ∧ 𝑧 ∈ ( Base ‘ 𝐺 ) ∧ 𝑥 ∈ 𝑌 ) ) → ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ⊕ 𝑥 ) = ( 𝑦 ⊕ ( 𝑧 ⊕ 𝑥 ) ) ) |
54 |
50 51 42 43 53
|
syl13anc |
⊢ ( ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ⊕ 𝑥 ) = ( 𝑦 ⊕ ( 𝑧 ⊕ 𝑥 ) ) ) |
55 |
46 49 54
|
3eqtr4d |
⊢ ( ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( 𝑦 ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) ( 𝑧 ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) ) = ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ⊕ 𝑥 ) ) |
56 |
52
|
subgcl |
⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) |
57 |
56
|
3expb |
⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) |
58 |
19 57
|
sylan |
⊢ ( ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ) |
59 |
|
ovres |
⊢ ( ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ∈ 𝑆 ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ⊕ 𝑥 ) ) |
60 |
58 43 59
|
syl2anc |
⊢ ( ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ⊕ 𝑥 ) ) |
61 |
1 52
|
ressplusg |
⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐻 ) ) |
62 |
61
|
ad3antlr |
⊢ ( ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( +g ‘ 𝐺 ) = ( +g ‘ 𝐻 ) ) |
63 |
62
|
oveqd |
⊢ ( ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑦 ( +g ‘ 𝐻 ) 𝑧 ) ) |
64 |
63
|
oveq1d |
⊢ ( ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = ( ( 𝑦 ( +g ‘ 𝐻 ) 𝑧 ) ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) ) |
65 |
55 60 64
|
3eqtr2rd |
⊢ ( ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝑦 ( +g ‘ 𝐻 ) 𝑧 ) ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = ( 𝑦 ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) ( 𝑧 ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) ) ) |
66 |
37 65
|
syldan |
⊢ ( ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐻 ) ∧ 𝑧 ∈ ( Base ‘ 𝐻 ) ) ) → ( ( 𝑦 ( +g ‘ 𝐻 ) 𝑧 ) ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = ( 𝑦 ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) ( 𝑧 ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) ) ) |
67 |
66
|
ralrimivva |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) → ∀ 𝑦 ∈ ( Base ‘ 𝐻 ) ∀ 𝑧 ∈ ( Base ‘ 𝐻 ) ( ( 𝑦 ( +g ‘ 𝐻 ) 𝑧 ) ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = ( 𝑦 ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) ( 𝑧 ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) ) ) |
68 |
31 67
|
jca |
⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ 𝑥 ∈ 𝑌 ) → ( ( ( 0g ‘ 𝐻 ) ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐻 ) ∀ 𝑧 ∈ ( Base ‘ 𝐻 ) ( ( 𝑦 ( +g ‘ 𝐻 ) 𝑧 ) ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = ( 𝑦 ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) ( 𝑧 ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) ) ) ) |
69 |
68
|
ralrimiva |
⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ∀ 𝑥 ∈ 𝑌 ( ( ( 0g ‘ 𝐻 ) ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐻 ) ∀ 𝑧 ∈ ( Base ‘ 𝐻 ) ( ( 𝑦 ( +g ‘ 𝐻 ) 𝑧 ) ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = ( 𝑦 ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) ( 𝑧 ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) ) ) ) |
70 |
18 69
|
jca |
⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) : ( ( Base ‘ 𝐻 ) × 𝑌 ) ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑌 ( ( ( 0g ‘ 𝐻 ) ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐻 ) ∀ 𝑧 ∈ ( Base ‘ 𝐻 ) ( ( 𝑦 ( +g ‘ 𝐻 ) 𝑧 ) ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = ( 𝑦 ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) ( 𝑧 ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) ) ) ) ) |
71 |
|
eqid |
⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 ) |
72 |
|
eqid |
⊢ ( +g ‘ 𝐻 ) = ( +g ‘ 𝐻 ) |
73 |
|
eqid |
⊢ ( 0g ‘ 𝐻 ) = ( 0g ‘ 𝐻 ) |
74 |
71 72 73
|
isga |
⊢ ( ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) ∈ ( 𝐻 GrpAct 𝑌 ) ↔ ( ( 𝐻 ∈ Grp ∧ 𝑌 ∈ V ) ∧ ( ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) : ( ( Base ‘ 𝐻 ) × 𝑌 ) ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑌 ( ( ( 0g ‘ 𝐻 ) ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐻 ) ∀ 𝑧 ∈ ( Base ‘ 𝐻 ) ( ( 𝑦 ( +g ‘ 𝐻 ) 𝑧 ) ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) = ( 𝑦 ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) ( 𝑧 ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) 𝑥 ) ) ) ) ) ) |
75 |
4 70 74
|
sylanbrc |
⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑌 ) ∧ 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ⊕ ↾ ( 𝑆 × 𝑌 ) ) ∈ ( 𝐻 GrpAct 𝑌 ) ) |