| Step | Hyp | Ref
| Expression |
| 1 | | gaset 19311 |
. . 3
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑌) → 𝑌 ∈ V) |
| 2 | | gasubg.1 |
. . . 4
⊢ 𝐻 = (𝐺 ↾s 𝑆) |
| 3 | 2 | subggrp 19147 |
. . 3
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐻 ∈ Grp) |
| 4 | 1, 3 | anim12ci 614 |
. 2
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (𝐻 ∈ Grp ∧ 𝑌 ∈ V)) |
| 5 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘𝐺) =
(Base‘𝐺) |
| 6 | 5 | gaf 19313 |
. . . . . 6
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑌) → ⊕ :((Base‘𝐺) × 𝑌)⟶𝑌) |
| 7 | 6 | adantr 480 |
. . . . 5
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ⊕ :((Base‘𝐺) × 𝑌)⟶𝑌) |
| 8 | | simpr 484 |
. . . . . . 7
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝑆 ∈ (SubGrp‘𝐺)) |
| 9 | 5 | subgss 19145 |
. . . . . . 7
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ (Base‘𝐺)) |
| 10 | 8, 9 | syl 17 |
. . . . . 6
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝑆 ⊆ (Base‘𝐺)) |
| 11 | | xpss1 5704 |
. . . . . 6
⊢ (𝑆 ⊆ (Base‘𝐺) → (𝑆 × 𝑌) ⊆ ((Base‘𝐺) × 𝑌)) |
| 12 | 10, 11 | syl 17 |
. . . . 5
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (𝑆 × 𝑌) ⊆ ((Base‘𝐺) × 𝑌)) |
| 13 | 7, 12 | fssresd 6775 |
. . . 4
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ( ⊕ ↾ (𝑆 × 𝑌)):(𝑆 × 𝑌)⟶𝑌) |
| 14 | 2 | subgbas 19148 |
. . . . . . 7
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 = (Base‘𝐻)) |
| 15 | 8, 14 | syl 17 |
. . . . . 6
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝑆 = (Base‘𝐻)) |
| 16 | 15 | xpeq1d 5714 |
. . . . 5
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (𝑆 × 𝑌) = ((Base‘𝐻) × 𝑌)) |
| 17 | 16 | feq2d 6722 |
. . . 4
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (( ⊕ ↾ (𝑆 × 𝑌)):(𝑆 × 𝑌)⟶𝑌 ↔ ( ⊕ ↾ (𝑆 × 𝑌)):((Base‘𝐻) × 𝑌)⟶𝑌)) |
| 18 | 13, 17 | mpbid 232 |
. . 3
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ( ⊕ ↾ (𝑆 × 𝑌)):((Base‘𝐻) × 𝑌)⟶𝑌) |
| 19 | 8 | adantr 480 |
. . . . . . . 8
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) → 𝑆 ∈ (SubGrp‘𝐺)) |
| 20 | | eqid 2737 |
. . . . . . . . 9
⊢
(0g‘𝐺) = (0g‘𝐺) |
| 21 | 20 | subg0cl 19152 |
. . . . . . . 8
⊢ (𝑆 ∈ (SubGrp‘𝐺) →
(0g‘𝐺)
∈ 𝑆) |
| 22 | 19, 21 | syl 17 |
. . . . . . 7
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) → (0g‘𝐺) ∈ 𝑆) |
| 23 | | simpr 484 |
. . . . . . 7
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) → 𝑥 ∈ 𝑌) |
| 24 | | ovres 7599 |
. . . . . . 7
⊢
(((0g‘𝐺) ∈ 𝑆 ∧ 𝑥 ∈ 𝑌) → ((0g‘𝐺)( ⊕ ↾ (𝑆 × 𝑌))𝑥) = ((0g‘𝐺) ⊕ 𝑥)) |
| 25 | 22, 23, 24 | syl2anc 584 |
. . . . . 6
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) → ((0g‘𝐺)( ⊕ ↾ (𝑆 × 𝑌))𝑥) = ((0g‘𝐺) ⊕ 𝑥)) |
| 26 | 2, 20 | subg0 19150 |
. . . . . . . 8
⊢ (𝑆 ∈ (SubGrp‘𝐺) →
(0g‘𝐺) =
(0g‘𝐻)) |
| 27 | 19, 26 | syl 17 |
. . . . . . 7
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) → (0g‘𝐺) = (0g‘𝐻)) |
| 28 | 27 | oveq1d 7446 |
. . . . . 6
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) → ((0g‘𝐺)( ⊕ ↾ (𝑆 × 𝑌))𝑥) = ((0g‘𝐻)( ⊕ ↾ (𝑆 × 𝑌))𝑥)) |
| 29 | 20 | gagrpid 19312 |
. . . . . . 7
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑥 ∈ 𝑌) → ((0g‘𝐺) ⊕ 𝑥) = 𝑥) |
| 30 | 29 | adantlr 715 |
. . . . . 6
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) → ((0g‘𝐺) ⊕ 𝑥) = 𝑥) |
| 31 | 25, 28, 30 | 3eqtr3d 2785 |
. . . . 5
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) → ((0g‘𝐻)( ⊕ ↾ (𝑆 × 𝑌))𝑥) = 𝑥) |
| 32 | | eqimss2 4043 |
. . . . . . . . . . 11
⊢ (𝑆 = (Base‘𝐻) → (Base‘𝐻) ⊆ 𝑆) |
| 33 | 15, 32 | syl 17 |
. . . . . . . . . 10
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (Base‘𝐻) ⊆ 𝑆) |
| 34 | 33 | adantr 480 |
. . . . . . . . 9
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) → (Base‘𝐻) ⊆ 𝑆) |
| 35 | 34 | sselda 3983 |
. . . . . . . 8
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑦 ∈ (Base‘𝐻)) → 𝑦 ∈ 𝑆) |
| 36 | 34 | sselda 3983 |
. . . . . . . 8
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) ∧ 𝑧 ∈ (Base‘𝐻)) → 𝑧 ∈ 𝑆) |
| 37 | 35, 36 | anim12dan 619 |
. . . . . . 7
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) ∧ (𝑦 ∈ (Base‘𝐻) ∧ 𝑧 ∈ (Base‘𝐻))) → (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) |
| 38 | | simprl 771 |
. . . . . . . . . 10
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑦 ∈ 𝑆) |
| 39 | 7 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ⊕ :((Base‘𝐺) × 𝑌)⟶𝑌) |
| 40 | 9 | ad3antlr 731 |
. . . . . . . . . . . 12
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑆 ⊆ (Base‘𝐺)) |
| 41 | | simprr 773 |
. . . . . . . . . . . 12
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑧 ∈ 𝑆) |
| 42 | 40, 41 | sseldd 3984 |
. . . . . . . . . . 11
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑧 ∈ (Base‘𝐺)) |
| 43 | 23 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑥 ∈ 𝑌) |
| 44 | 39, 42, 43 | fovcdmd 7605 |
. . . . . . . . . 10
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑧 ⊕ 𝑥) ∈ 𝑌) |
| 45 | | ovres 7599 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝑆 ∧ (𝑧 ⊕ 𝑥) ∈ 𝑌) → (𝑦( ⊕ ↾ (𝑆 × 𝑌))(𝑧 ⊕ 𝑥)) = (𝑦 ⊕ (𝑧 ⊕ 𝑥))) |
| 46 | 38, 44, 45 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑦( ⊕ ↾ (𝑆 × 𝑌))(𝑧 ⊕ 𝑥)) = (𝑦 ⊕ (𝑧 ⊕ 𝑥))) |
| 47 | | ovres 7599 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑥 ∈ 𝑌) → (𝑧( ⊕ ↾ (𝑆 × 𝑌))𝑥) = (𝑧 ⊕ 𝑥)) |
| 48 | 41, 43, 47 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑧( ⊕ ↾ (𝑆 × 𝑌))𝑥) = (𝑧 ⊕ 𝑥)) |
| 49 | 48 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑦( ⊕ ↾ (𝑆 × 𝑌))(𝑧( ⊕ ↾ (𝑆 × 𝑌))𝑥)) = (𝑦( ⊕ ↾ (𝑆 × 𝑌))(𝑧 ⊕ 𝑥))) |
| 50 | | simplll 775 |
. . . . . . . . . 10
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ⊕ ∈ (𝐺 GrpAct 𝑌)) |
| 51 | 40, 38 | sseldd 3984 |
. . . . . . . . . 10
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑦 ∈ (Base‘𝐺)) |
| 52 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(+g‘𝐺) = (+g‘𝐺) |
| 53 | 5, 52 | gaass 19315 |
. . . . . . . . . 10
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺) ∧ 𝑥 ∈ 𝑌)) → ((𝑦(+g‘𝐺)𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥))) |
| 54 | 50, 51, 42, 43, 53 | syl13anc 1374 |
. . . . . . . . 9
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑦(+g‘𝐺)𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥))) |
| 55 | 46, 49, 54 | 3eqtr4d 2787 |
. . . . . . . 8
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑦( ⊕ ↾ (𝑆 × 𝑌))(𝑧( ⊕ ↾ (𝑆 × 𝑌))𝑥)) = ((𝑦(+g‘𝐺)𝑧) ⊕ 𝑥)) |
| 56 | 52 | subgcl 19154 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) → (𝑦(+g‘𝐺)𝑧) ∈ 𝑆) |
| 57 | 56 | 3expb 1121 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑦(+g‘𝐺)𝑧) ∈ 𝑆) |
| 58 | 19, 57 | sylan 580 |
. . . . . . . . 9
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑦(+g‘𝐺)𝑧) ∈ 𝑆) |
| 59 | | ovres 7599 |
. . . . . . . . 9
⊢ (((𝑦(+g‘𝐺)𝑧) ∈ 𝑆 ∧ 𝑥 ∈ 𝑌) → ((𝑦(+g‘𝐺)𝑧)( ⊕ ↾ (𝑆 × 𝑌))𝑥) = ((𝑦(+g‘𝐺)𝑧) ⊕ 𝑥)) |
| 60 | 58, 43, 59 | syl2anc 584 |
. . . . . . . 8
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑦(+g‘𝐺)𝑧)( ⊕ ↾ (𝑆 × 𝑌))𝑥) = ((𝑦(+g‘𝐺)𝑧) ⊕ 𝑥)) |
| 61 | 2, 52 | ressplusg 17334 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ (SubGrp‘𝐺) →
(+g‘𝐺) =
(+g‘𝐻)) |
| 62 | 61 | ad3antlr 731 |
. . . . . . . . . 10
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (+g‘𝐺) = (+g‘𝐻)) |
| 63 | 62 | oveqd 7448 |
. . . . . . . . 9
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑦(+g‘𝐺)𝑧) = (𝑦(+g‘𝐻)𝑧)) |
| 64 | 63 | oveq1d 7446 |
. . . . . . . 8
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑦(+g‘𝐺)𝑧)( ⊕ ↾ (𝑆 × 𝑌))𝑥) = ((𝑦(+g‘𝐻)𝑧)( ⊕ ↾ (𝑆 × 𝑌))𝑥)) |
| 65 | 55, 60, 64 | 3eqtr2rd 2784 |
. . . . . . 7
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → ((𝑦(+g‘𝐻)𝑧)( ⊕ ↾ (𝑆 × 𝑌))𝑥) = (𝑦( ⊕ ↾ (𝑆 × 𝑌))(𝑧( ⊕ ↾ (𝑆 × 𝑌))𝑥))) |
| 66 | 37, 65 | syldan 591 |
. . . . . 6
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) ∧ (𝑦 ∈ (Base‘𝐻) ∧ 𝑧 ∈ (Base‘𝐻))) → ((𝑦(+g‘𝐻)𝑧)( ⊕ ↾ (𝑆 × 𝑌))𝑥) = (𝑦( ⊕ ↾ (𝑆 × 𝑌))(𝑧( ⊕ ↾ (𝑆 × 𝑌))𝑥))) |
| 67 | 66 | ralrimivva 3202 |
. . . . 5
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) → ∀𝑦 ∈ (Base‘𝐻)∀𝑧 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑧)( ⊕ ↾ (𝑆 × 𝑌))𝑥) = (𝑦( ⊕ ↾ (𝑆 × 𝑌))(𝑧( ⊕ ↾ (𝑆 × 𝑌))𝑥))) |
| 68 | 31, 67 | jca 511 |
. . . 4
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ 𝑥 ∈ 𝑌) → (((0g‘𝐻)( ⊕ ↾ (𝑆 × 𝑌))𝑥) = 𝑥 ∧ ∀𝑦 ∈ (Base‘𝐻)∀𝑧 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑧)( ⊕ ↾ (𝑆 × 𝑌))𝑥) = (𝑦( ⊕ ↾ (𝑆 × 𝑌))(𝑧( ⊕ ↾ (𝑆 × 𝑌))𝑥)))) |
| 69 | 68 | ralrimiva 3146 |
. . 3
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ∀𝑥 ∈ 𝑌 (((0g‘𝐻)( ⊕ ↾ (𝑆 × 𝑌))𝑥) = 𝑥 ∧ ∀𝑦 ∈ (Base‘𝐻)∀𝑧 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑧)( ⊕ ↾ (𝑆 × 𝑌))𝑥) = (𝑦( ⊕ ↾ (𝑆 × 𝑌))(𝑧( ⊕ ↾ (𝑆 × 𝑌))𝑥)))) |
| 70 | 18, 69 | jca 511 |
. 2
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (( ⊕ ↾ (𝑆 × 𝑌)):((Base‘𝐻) × 𝑌)⟶𝑌 ∧ ∀𝑥 ∈ 𝑌 (((0g‘𝐻)( ⊕ ↾ (𝑆 × 𝑌))𝑥) = 𝑥 ∧ ∀𝑦 ∈ (Base‘𝐻)∀𝑧 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑧)( ⊕ ↾ (𝑆 × 𝑌))𝑥) = (𝑦( ⊕ ↾ (𝑆 × 𝑌))(𝑧( ⊕ ↾ (𝑆 × 𝑌))𝑥))))) |
| 71 | | eqid 2737 |
. . 3
⊢
(Base‘𝐻) =
(Base‘𝐻) |
| 72 | | eqid 2737 |
. . 3
⊢
(+g‘𝐻) = (+g‘𝐻) |
| 73 | | eqid 2737 |
. . 3
⊢
(0g‘𝐻) = (0g‘𝐻) |
| 74 | 71, 72, 73 | isga 19309 |
. 2
⊢ (( ⊕
↾ (𝑆 × 𝑌)) ∈ (𝐻 GrpAct 𝑌) ↔ ((𝐻 ∈ Grp ∧ 𝑌 ∈ V) ∧ (( ⊕ ↾ (𝑆 × 𝑌)):((Base‘𝐻) × 𝑌)⟶𝑌 ∧ ∀𝑥 ∈ 𝑌 (((0g‘𝐻)( ⊕ ↾ (𝑆 × 𝑌))𝑥) = 𝑥 ∧ ∀𝑦 ∈ (Base‘𝐻)∀𝑧 ∈ (Base‘𝐻)((𝑦(+g‘𝐻)𝑧)( ⊕ ↾ (𝑆 × 𝑌))𝑥) = (𝑦( ⊕ ↾ (𝑆 × 𝑌))(𝑧( ⊕ ↾ (𝑆 × 𝑌))𝑥)))))) |
| 75 | 4, 70, 74 | sylanbrc 583 |
1
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ( ⊕ ↾ (𝑆 × 𝑌)) ∈ (𝐻 GrpAct 𝑌)) |