Step | Hyp | Ref
| Expression |
1 | | subgga.3 |
. . . 4
⊢ 𝐻 = (𝐺 ↾s 𝑌) |
2 | 1 | subggrp 17420 |
. . 3
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝐻 ∈ Grp) |
3 | | subgga.1 |
. . . 4
⊢ 𝑋 = (Base‘𝐺) |
4 | | fvex 6113 |
. . . 4
⊢
(Base‘𝐺)
∈ V |
5 | 3, 4 | eqeltri 2684 |
. . 3
⊢ 𝑋 ∈ V |
6 | 2, 5 | jctir 559 |
. 2
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (𝐻 ∈ Grp ∧ 𝑋 ∈ V)) |
7 | | subgrcl 17422 |
. . . . . . . 8
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
8 | 7 | adantr 480 |
. . . . . . 7
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋)) → 𝐺 ∈ Grp) |
9 | 3 | subgss 17418 |
. . . . . . . . 9
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝑌 ⊆ 𝑋) |
10 | 9 | sselda 3568 |
. . . . . . . 8
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑌) → 𝑥 ∈ 𝑋) |
11 | 10 | adantrr 749 |
. . . . . . 7
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋)) → 𝑥 ∈ 𝑋) |
12 | | simprr 792 |
. . . . . . 7
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ 𝑋) |
13 | | subgga.2 |
. . . . . . . 8
⊢ + =
(+g‘𝐺) |
14 | 3, 13 | grpcl 17253 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥 + 𝑦) ∈ 𝑋) |
15 | 8, 11, 12, 14 | syl3anc 1318 |
. . . . . 6
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋)) → (𝑥 + 𝑦) ∈ 𝑋) |
16 | 15 | ralrimivva 2954 |
. . . . 5
⊢ (𝑌 ∈ (SubGrp‘𝐺) → ∀𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑋 (𝑥 + 𝑦) ∈ 𝑋) |
17 | | subgga.4 |
. . . . . 6
⊢ 𝐹 = (𝑥 ∈ 𝑌, 𝑦 ∈ 𝑋 ↦ (𝑥 + 𝑦)) |
18 | 17 | fmpt2 7126 |
. . . . 5
⊢
(∀𝑥 ∈
𝑌 ∀𝑦 ∈ 𝑋 (𝑥 + 𝑦) ∈ 𝑋 ↔ 𝐹:(𝑌 × 𝑋)⟶𝑋) |
19 | 16, 18 | sylib 207 |
. . . 4
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝐹:(𝑌 × 𝑋)⟶𝑋) |
20 | 1 | subgbas 17421 |
. . . . . 6
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝑌 = (Base‘𝐻)) |
21 | 20 | xpeq1d 5062 |
. . . . 5
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (𝑌 × 𝑋) = ((Base‘𝐻) × 𝑋)) |
22 | 21 | feq2d 5944 |
. . . 4
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (𝐹:(𝑌 × 𝑋)⟶𝑋 ↔ 𝐹:((Base‘𝐻) × 𝑋)⟶𝑋)) |
23 | 19, 22 | mpbid 221 |
. . 3
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝐹:((Base‘𝐻) × 𝑋)⟶𝑋) |
24 | | eqid 2610 |
. . . . . . . 8
⊢
(0g‘𝐺) = (0g‘𝐺) |
25 | 24 | subg0cl 17425 |
. . . . . . 7
⊢ (𝑌 ∈ (SubGrp‘𝐺) →
(0g‘𝐺)
∈ 𝑌) |
26 | | oveq12 6558 |
. . . . . . . 8
⊢ ((𝑥 = (0g‘𝐺) ∧ 𝑦 = 𝑢) → (𝑥 + 𝑦) = ((0g‘𝐺) + 𝑢)) |
27 | | ovex 6577 |
. . . . . . . 8
⊢
((0g‘𝐺) + 𝑢) ∈ V |
28 | 26, 17, 27 | ovmpt2a 6689 |
. . . . . . 7
⊢
(((0g‘𝐺) ∈ 𝑌 ∧ 𝑢 ∈ 𝑋) → ((0g‘𝐺)𝐹𝑢) = ((0g‘𝐺) + 𝑢)) |
29 | 25, 28 | sylan 487 |
. . . . . 6
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) → ((0g‘𝐺)𝐹𝑢) = ((0g‘𝐺) + 𝑢)) |
30 | 1, 24 | subg0 17423 |
. . . . . . . 8
⊢ (𝑌 ∈ (SubGrp‘𝐺) →
(0g‘𝐺) =
(0g‘𝐻)) |
31 | 30 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑌 ∈ (SubGrp‘𝐺) →
((0g‘𝐺)𝐹𝑢) = ((0g‘𝐻)𝐹𝑢)) |
32 | 31 | adantr 480 |
. . . . . 6
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) → ((0g‘𝐺)𝐹𝑢) = ((0g‘𝐻)𝐹𝑢)) |
33 | 3, 13, 24 | grplid 17275 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ 𝑋) → ((0g‘𝐺) + 𝑢) = 𝑢) |
34 | 7, 33 | sylan 487 |
. . . . . 6
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) → ((0g‘𝐺) + 𝑢) = 𝑢) |
35 | 29, 32, 34 | 3eqtr3d 2652 |
. . . . 5
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) → ((0g‘𝐻)𝐹𝑢) = 𝑢) |
36 | 7 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝐺 ∈ Grp) |
37 | 9 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝑌 ⊆ 𝑋) |
38 | | simprl 790 |
. . . . . . . . . . 11
⊢ (((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝑣 ∈ 𝑌) |
39 | 37, 38 | sseldd 3569 |
. . . . . . . . . 10
⊢ (((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝑣 ∈ 𝑋) |
40 | | simprr 792 |
. . . . . . . . . . 11
⊢ (((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝑤 ∈ 𝑌) |
41 | 37, 40 | sseldd 3569 |
. . . . . . . . . 10
⊢ (((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝑤 ∈ 𝑋) |
42 | | simplr 788 |
. . . . . . . . . 10
⊢ (((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝑢 ∈ 𝑋) |
43 | 3, 13 | grpass 17254 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋)) → ((𝑣 + 𝑤) + 𝑢) = (𝑣 + (𝑤 + 𝑢))) |
44 | 36, 39, 41, 42, 43 | syl13anc 1320 |
. . . . . . . . 9
⊢ (((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → ((𝑣 + 𝑤) + 𝑢) = (𝑣 + (𝑤 + 𝑢))) |
45 | 3, 13 | grpcl 17253 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑤 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋) → (𝑤 + 𝑢) ∈ 𝑋) |
46 | 36, 41, 42, 45 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (𝑤 + 𝑢) ∈ 𝑋) |
47 | | oveq12 6558 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = (𝑤 + 𝑢)) → (𝑥 + 𝑦) = (𝑣 + (𝑤 + 𝑢))) |
48 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (𝑣 + (𝑤 + 𝑢)) ∈ V |
49 | 47, 17, 48 | ovmpt2a 6689 |
. . . . . . . . . 10
⊢ ((𝑣 ∈ 𝑌 ∧ (𝑤 + 𝑢) ∈ 𝑋) → (𝑣𝐹(𝑤 + 𝑢)) = (𝑣 + (𝑤 + 𝑢))) |
50 | 38, 46, 49 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (𝑣𝐹(𝑤 + 𝑢)) = (𝑣 + (𝑤 + 𝑢))) |
51 | 44, 50 | eqtr4d 2647 |
. . . . . . . 8
⊢ (((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → ((𝑣 + 𝑤) + 𝑢) = (𝑣𝐹(𝑤 + 𝑢))) |
52 | 13 | subgcl 17427 |
. . . . . . . . . . 11
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌) → (𝑣 + 𝑤) ∈ 𝑌) |
53 | 52 | 3expb 1258 |
. . . . . . . . . 10
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (𝑣 + 𝑤) ∈ 𝑌) |
54 | 53 | adantlr 747 |
. . . . . . . . 9
⊢ (((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (𝑣 + 𝑤) ∈ 𝑌) |
55 | | oveq12 6558 |
. . . . . . . . . 10
⊢ ((𝑥 = (𝑣 + 𝑤) ∧ 𝑦 = 𝑢) → (𝑥 + 𝑦) = ((𝑣 + 𝑤) + 𝑢)) |
56 | | ovex 6577 |
. . . . . . . . . 10
⊢ ((𝑣 + 𝑤) + 𝑢) ∈ V |
57 | 55, 17, 56 | ovmpt2a 6689 |
. . . . . . . . 9
⊢ (((𝑣 + 𝑤) ∈ 𝑌 ∧ 𝑢 ∈ 𝑋) → ((𝑣 + 𝑤)𝐹𝑢) = ((𝑣 + 𝑤) + 𝑢)) |
58 | 54, 42, 57 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → ((𝑣 + 𝑤)𝐹𝑢) = ((𝑣 + 𝑤) + 𝑢)) |
59 | | oveq12 6558 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑢) → (𝑥 + 𝑦) = (𝑤 + 𝑢)) |
60 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (𝑤 + 𝑢) ∈ V |
61 | 59, 17, 60 | ovmpt2a 6689 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ 𝑌 ∧ 𝑢 ∈ 𝑋) → (𝑤𝐹𝑢) = (𝑤 + 𝑢)) |
62 | 40, 42, 61 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (𝑤𝐹𝑢) = (𝑤 + 𝑢)) |
63 | 62 | oveq2d 6565 |
. . . . . . . 8
⊢ (((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (𝑣𝐹(𝑤𝐹𝑢)) = (𝑣𝐹(𝑤 + 𝑢))) |
64 | 51, 58, 63 | 3eqtr4d 2654 |
. . . . . . 7
⊢ (((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → ((𝑣 + 𝑤)𝐹𝑢) = (𝑣𝐹(𝑤𝐹𝑢))) |
65 | 64 | ralrimivva 2954 |
. . . . . 6
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) → ∀𝑣 ∈ 𝑌 ∀𝑤 ∈ 𝑌 ((𝑣 + 𝑤)𝐹𝑢) = (𝑣𝐹(𝑤𝐹𝑢))) |
66 | 1, 13 | ressplusg 15818 |
. . . . . . . . . . . 12
⊢ (𝑌 ∈ (SubGrp‘𝐺) → + =
(+g‘𝐻)) |
67 | 66 | oveqd 6566 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (𝑣 + 𝑤) = (𝑣(+g‘𝐻)𝑤)) |
68 | 67 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑌 ∈ (SubGrp‘𝐺) → ((𝑣 + 𝑤)𝐹𝑢) = ((𝑣(+g‘𝐻)𝑤)𝐹𝑢)) |
69 | 68 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (((𝑣 + 𝑤)𝐹𝑢) = (𝑣𝐹(𝑤𝐹𝑢)) ↔ ((𝑣(+g‘𝐻)𝑤)𝐹𝑢) = (𝑣𝐹(𝑤𝐹𝑢)))) |
70 | 20, 69 | raleqbidv 3129 |
. . . . . . . 8
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (∀𝑤 ∈ 𝑌 ((𝑣 + 𝑤)𝐹𝑢) = (𝑣𝐹(𝑤𝐹𝑢)) ↔ ∀𝑤 ∈ (Base‘𝐻)((𝑣(+g‘𝐻)𝑤)𝐹𝑢) = (𝑣𝐹(𝑤𝐹𝑢)))) |
71 | 20, 70 | raleqbidv 3129 |
. . . . . . 7
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (∀𝑣 ∈ 𝑌 ∀𝑤 ∈ 𝑌 ((𝑣 + 𝑤)𝐹𝑢) = (𝑣𝐹(𝑤𝐹𝑢)) ↔ ∀𝑣 ∈ (Base‘𝐻)∀𝑤 ∈ (Base‘𝐻)((𝑣(+g‘𝐻)𝑤)𝐹𝑢) = (𝑣𝐹(𝑤𝐹𝑢)))) |
72 | 71 | biimpa 500 |
. . . . . 6
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ ∀𝑣 ∈ 𝑌 ∀𝑤 ∈ 𝑌 ((𝑣 + 𝑤)𝐹𝑢) = (𝑣𝐹(𝑤𝐹𝑢))) → ∀𝑣 ∈ (Base‘𝐻)∀𝑤 ∈ (Base‘𝐻)((𝑣(+g‘𝐻)𝑤)𝐹𝑢) = (𝑣𝐹(𝑤𝐹𝑢))) |
73 | 65, 72 | syldan 486 |
. . . . 5
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) → ∀𝑣 ∈ (Base‘𝐻)∀𝑤 ∈ (Base‘𝐻)((𝑣(+g‘𝐻)𝑤)𝐹𝑢) = (𝑣𝐹(𝑤𝐹𝑢))) |
74 | 35, 73 | jca 553 |
. . . 4
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) → (((0g‘𝐻)𝐹𝑢) = 𝑢 ∧ ∀𝑣 ∈ (Base‘𝐻)∀𝑤 ∈ (Base‘𝐻)((𝑣(+g‘𝐻)𝑤)𝐹𝑢) = (𝑣𝐹(𝑤𝐹𝑢)))) |
75 | 74 | ralrimiva 2949 |
. . 3
⊢ (𝑌 ∈ (SubGrp‘𝐺) → ∀𝑢 ∈ 𝑋 (((0g‘𝐻)𝐹𝑢) = 𝑢 ∧ ∀𝑣 ∈ (Base‘𝐻)∀𝑤 ∈ (Base‘𝐻)((𝑣(+g‘𝐻)𝑤)𝐹𝑢) = (𝑣𝐹(𝑤𝐹𝑢)))) |
76 | 23, 75 | jca 553 |
. 2
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (𝐹:((Base‘𝐻) × 𝑋)⟶𝑋 ∧ ∀𝑢 ∈ 𝑋 (((0g‘𝐻)𝐹𝑢) = 𝑢 ∧ ∀𝑣 ∈ (Base‘𝐻)∀𝑤 ∈ (Base‘𝐻)((𝑣(+g‘𝐻)𝑤)𝐹𝑢) = (𝑣𝐹(𝑤𝐹𝑢))))) |
77 | | eqid 2610 |
. . 3
⊢
(Base‘𝐻) =
(Base‘𝐻) |
78 | | eqid 2610 |
. . 3
⊢
(+g‘𝐻) = (+g‘𝐻) |
79 | | eqid 2610 |
. . 3
⊢
(0g‘𝐻) = (0g‘𝐻) |
80 | 77, 78, 79 | isga 17547 |
. 2
⊢ (𝐹 ∈ (𝐻 GrpAct 𝑋) ↔ ((𝐻 ∈ Grp ∧ 𝑋 ∈ V) ∧ (𝐹:((Base‘𝐻) × 𝑋)⟶𝑋 ∧ ∀𝑢 ∈ 𝑋 (((0g‘𝐻)𝐹𝑢) = 𝑢 ∧ ∀𝑣 ∈ (Base‘𝐻)∀𝑤 ∈ (Base‘𝐻)((𝑣(+g‘𝐻)𝑤)𝐹𝑢) = (𝑣𝐹(𝑤𝐹𝑢)))))) |
81 | 6, 76, 80 | sylanbrc 695 |
1
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝐹 ∈ (𝐻 GrpAct 𝑋)) |