| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | subgga.3 | . . . 4
⊢ 𝐻 = (𝐺 ↾s 𝑌) | 
| 2 | 1 | subggrp 19148 | . . 3
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝐻 ∈ Grp) | 
| 3 |  | subgga.1 | . . . 4
⊢ 𝑋 = (Base‘𝐺) | 
| 4 | 3 | fvexi 6919 | . . 3
⊢ 𝑋 ∈ V | 
| 5 | 2, 4 | jctir 520 | . 2
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (𝐻 ∈ Grp ∧ 𝑋 ∈ V)) | 
| 6 |  | subgrcl 19150 | . . . . . . . 8
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) | 
| 7 | 6 | adantr 480 | . . . . . . 7
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋)) → 𝐺 ∈ Grp) | 
| 8 | 3 | subgss 19146 | . . . . . . . . 9
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝑌 ⊆ 𝑋) | 
| 9 | 8 | sselda 3982 | . . . . . . . 8
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑥 ∈ 𝑌) → 𝑥 ∈ 𝑋) | 
| 10 | 9 | adantrr 717 | . . . . . . 7
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋)) → 𝑥 ∈ 𝑋) | 
| 11 |  | simprr 772 | . . . . . . 7
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋)) → 𝑦 ∈ 𝑋) | 
| 12 |  | subgga.2 | . . . . . . . 8
⊢  + =
(+g‘𝐺) | 
| 13 | 3, 12 | grpcl 18960 | . . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝑥 + 𝑦) ∈ 𝑋) | 
| 14 | 7, 10, 11, 13 | syl3anc 1372 | . . . . . 6
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑋)) → (𝑥 + 𝑦) ∈ 𝑋) | 
| 15 | 14 | ralrimivva 3201 | . . . . 5
⊢ (𝑌 ∈ (SubGrp‘𝐺) → ∀𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑋 (𝑥 + 𝑦) ∈ 𝑋) | 
| 16 |  | subgga.4 | . . . . . 6
⊢ 𝐹 = (𝑥 ∈ 𝑌, 𝑦 ∈ 𝑋 ↦ (𝑥 + 𝑦)) | 
| 17 | 16 | fmpo 8094 | . . . . 5
⊢
(∀𝑥 ∈
𝑌 ∀𝑦 ∈ 𝑋 (𝑥 + 𝑦) ∈ 𝑋 ↔ 𝐹:(𝑌 × 𝑋)⟶𝑋) | 
| 18 | 15, 17 | sylib 218 | . . . 4
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝐹:(𝑌 × 𝑋)⟶𝑋) | 
| 19 | 1 | subgbas 19149 | . . . . . 6
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝑌 = (Base‘𝐻)) | 
| 20 | 19 | xpeq1d 5713 | . . . . 5
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (𝑌 × 𝑋) = ((Base‘𝐻) × 𝑋)) | 
| 21 | 20 | feq2d 6721 | . . . 4
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (𝐹:(𝑌 × 𝑋)⟶𝑋 ↔ 𝐹:((Base‘𝐻) × 𝑋)⟶𝑋)) | 
| 22 | 18, 21 | mpbid 232 | . . 3
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝐹:((Base‘𝐻) × 𝑋)⟶𝑋) | 
| 23 |  | eqid 2736 | . . . . . . . 8
⊢
(0g‘𝐺) = (0g‘𝐺) | 
| 24 | 23 | subg0cl 19153 | . . . . . . 7
⊢ (𝑌 ∈ (SubGrp‘𝐺) →
(0g‘𝐺)
∈ 𝑌) | 
| 25 |  | oveq12 7441 | . . . . . . . 8
⊢ ((𝑥 = (0g‘𝐺) ∧ 𝑦 = 𝑢) → (𝑥 + 𝑦) = ((0g‘𝐺) + 𝑢)) | 
| 26 |  | ovex 7465 | . . . . . . . 8
⊢
((0g‘𝐺) + 𝑢) ∈ V | 
| 27 | 25, 16, 26 | ovmpoa 7589 | . . . . . . 7
⊢
(((0g‘𝐺) ∈ 𝑌 ∧ 𝑢 ∈ 𝑋) → ((0g‘𝐺)𝐹𝑢) = ((0g‘𝐺) + 𝑢)) | 
| 28 | 24, 27 | sylan 580 | . . . . . 6
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) → ((0g‘𝐺)𝐹𝑢) = ((0g‘𝐺) + 𝑢)) | 
| 29 | 1, 23 | subg0 19151 | . . . . . . . 8
⊢ (𝑌 ∈ (SubGrp‘𝐺) →
(0g‘𝐺) =
(0g‘𝐻)) | 
| 30 | 29 | oveq1d 7447 | . . . . . . 7
⊢ (𝑌 ∈ (SubGrp‘𝐺) →
((0g‘𝐺)𝐹𝑢) = ((0g‘𝐻)𝐹𝑢)) | 
| 31 | 30 | adantr 480 | . . . . . 6
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) → ((0g‘𝐺)𝐹𝑢) = ((0g‘𝐻)𝐹𝑢)) | 
| 32 | 3, 12, 23 | grplid 18986 | . . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ 𝑋) → ((0g‘𝐺) + 𝑢) = 𝑢) | 
| 33 | 6, 32 | sylan 580 | . . . . . 6
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) → ((0g‘𝐺) + 𝑢) = 𝑢) | 
| 34 | 28, 31, 33 | 3eqtr3d 2784 | . . . . 5
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) → ((0g‘𝐻)𝐹𝑢) = 𝑢) | 
| 35 | 6 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝐺 ∈ Grp) | 
| 36 | 8 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝑌 ⊆ 𝑋) | 
| 37 |  | simprl 770 | . . . . . . . . . . 11
⊢ (((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝑣 ∈ 𝑌) | 
| 38 | 36, 37 | sseldd 3983 | . . . . . . . . . 10
⊢ (((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝑣 ∈ 𝑋) | 
| 39 |  | simprr 772 | . . . . . . . . . . 11
⊢ (((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝑤 ∈ 𝑌) | 
| 40 | 36, 39 | sseldd 3983 | . . . . . . . . . 10
⊢ (((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝑤 ∈ 𝑋) | 
| 41 |  | simplr 768 | . . . . . . . . . 10
⊢ (((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → 𝑢 ∈ 𝑋) | 
| 42 | 3, 12 | grpass 18961 | . . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ (𝑣 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋)) → ((𝑣 + 𝑤) + 𝑢) = (𝑣 + (𝑤 + 𝑢))) | 
| 43 | 35, 38, 40, 41, 42 | syl13anc 1373 | . . . . . . . . 9
⊢ (((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → ((𝑣 + 𝑤) + 𝑢) = (𝑣 + (𝑤 + 𝑢))) | 
| 44 | 3, 12 | grpcl 18960 | . . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑤 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋) → (𝑤 + 𝑢) ∈ 𝑋) | 
| 45 | 35, 40, 41, 44 | syl3anc 1372 | . . . . . . . . . 10
⊢ (((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (𝑤 + 𝑢) ∈ 𝑋) | 
| 46 |  | oveq12 7441 | . . . . . . . . . . 11
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = (𝑤 + 𝑢)) → (𝑥 + 𝑦) = (𝑣 + (𝑤 + 𝑢))) | 
| 47 |  | ovex 7465 | . . . . . . . . . . 11
⊢ (𝑣 + (𝑤 + 𝑢)) ∈ V | 
| 48 | 46, 16, 47 | ovmpoa 7589 | . . . . . . . . . 10
⊢ ((𝑣 ∈ 𝑌 ∧ (𝑤 + 𝑢) ∈ 𝑋) → (𝑣𝐹(𝑤 + 𝑢)) = (𝑣 + (𝑤 + 𝑢))) | 
| 49 | 37, 45, 48 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (𝑣𝐹(𝑤 + 𝑢)) = (𝑣 + (𝑤 + 𝑢))) | 
| 50 | 43, 49 | eqtr4d 2779 | . . . . . . . 8
⊢ (((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → ((𝑣 + 𝑤) + 𝑢) = (𝑣𝐹(𝑤 + 𝑢))) | 
| 51 | 12 | subgcl 19155 | . . . . . . . . . . 11
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌) → (𝑣 + 𝑤) ∈ 𝑌) | 
| 52 | 51 | 3expb 1120 | . . . . . . . . . 10
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (𝑣 + 𝑤) ∈ 𝑌) | 
| 53 | 52 | adantlr 715 | . . . . . . . . 9
⊢ (((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (𝑣 + 𝑤) ∈ 𝑌) | 
| 54 |  | oveq12 7441 | . . . . . . . . . 10
⊢ ((𝑥 = (𝑣 + 𝑤) ∧ 𝑦 = 𝑢) → (𝑥 + 𝑦) = ((𝑣 + 𝑤) + 𝑢)) | 
| 55 |  | ovex 7465 | . . . . . . . . . 10
⊢ ((𝑣 + 𝑤) + 𝑢) ∈ V | 
| 56 | 54, 16, 55 | ovmpoa 7589 | . . . . . . . . 9
⊢ (((𝑣 + 𝑤) ∈ 𝑌 ∧ 𝑢 ∈ 𝑋) → ((𝑣 + 𝑤)𝐹𝑢) = ((𝑣 + 𝑤) + 𝑢)) | 
| 57 | 53, 41, 56 | syl2anc 584 | . . . . . . . 8
⊢ (((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → ((𝑣 + 𝑤)𝐹𝑢) = ((𝑣 + 𝑤) + 𝑢)) | 
| 58 |  | oveq12 7441 | . . . . . . . . . . 11
⊢ ((𝑥 = 𝑤 ∧ 𝑦 = 𝑢) → (𝑥 + 𝑦) = (𝑤 + 𝑢)) | 
| 59 |  | ovex 7465 | . . . . . . . . . . 11
⊢ (𝑤 + 𝑢) ∈ V | 
| 60 | 58, 16, 59 | ovmpoa 7589 | . . . . . . . . . 10
⊢ ((𝑤 ∈ 𝑌 ∧ 𝑢 ∈ 𝑋) → (𝑤𝐹𝑢) = (𝑤 + 𝑢)) | 
| 61 | 39, 41, 60 | syl2anc 584 | . . . . . . . . 9
⊢ (((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (𝑤𝐹𝑢) = (𝑤 + 𝑢)) | 
| 62 | 61 | oveq2d 7448 | . . . . . . . 8
⊢ (((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → (𝑣𝐹(𝑤𝐹𝑢)) = (𝑣𝐹(𝑤 + 𝑢))) | 
| 63 | 50, 57, 62 | 3eqtr4d 2786 | . . . . . . 7
⊢ (((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) ∧ (𝑣 ∈ 𝑌 ∧ 𝑤 ∈ 𝑌)) → ((𝑣 + 𝑤)𝐹𝑢) = (𝑣𝐹(𝑤𝐹𝑢))) | 
| 64 | 63 | ralrimivva 3201 | . . . . . 6
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) → ∀𝑣 ∈ 𝑌 ∀𝑤 ∈ 𝑌 ((𝑣 + 𝑤)𝐹𝑢) = (𝑣𝐹(𝑤𝐹𝑢))) | 
| 65 | 1, 12 | ressplusg 17335 | . . . . . . . . . . . 12
⊢ (𝑌 ∈ (SubGrp‘𝐺) → + =
(+g‘𝐻)) | 
| 66 | 65 | oveqd 7449 | . . . . . . . . . . 11
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (𝑣 + 𝑤) = (𝑣(+g‘𝐻)𝑤)) | 
| 67 | 66 | oveq1d 7447 | . . . . . . . . . 10
⊢ (𝑌 ∈ (SubGrp‘𝐺) → ((𝑣 + 𝑤)𝐹𝑢) = ((𝑣(+g‘𝐻)𝑤)𝐹𝑢)) | 
| 68 | 67 | eqeq1d 2738 | . . . . . . . . 9
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (((𝑣 + 𝑤)𝐹𝑢) = (𝑣𝐹(𝑤𝐹𝑢)) ↔ ((𝑣(+g‘𝐻)𝑤)𝐹𝑢) = (𝑣𝐹(𝑤𝐹𝑢)))) | 
| 69 | 19, 68 | raleqbidv 3345 | . . . . . . . 8
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (∀𝑤 ∈ 𝑌 ((𝑣 + 𝑤)𝐹𝑢) = (𝑣𝐹(𝑤𝐹𝑢)) ↔ ∀𝑤 ∈ (Base‘𝐻)((𝑣(+g‘𝐻)𝑤)𝐹𝑢) = (𝑣𝐹(𝑤𝐹𝑢)))) | 
| 70 | 19, 69 | raleqbidv 3345 | . . . . . . 7
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (∀𝑣 ∈ 𝑌 ∀𝑤 ∈ 𝑌 ((𝑣 + 𝑤)𝐹𝑢) = (𝑣𝐹(𝑤𝐹𝑢)) ↔ ∀𝑣 ∈ (Base‘𝐻)∀𝑤 ∈ (Base‘𝐻)((𝑣(+g‘𝐻)𝑤)𝐹𝑢) = (𝑣𝐹(𝑤𝐹𝑢)))) | 
| 71 | 70 | biimpa 476 | . . . . . 6
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ ∀𝑣 ∈ 𝑌 ∀𝑤 ∈ 𝑌 ((𝑣 + 𝑤)𝐹𝑢) = (𝑣𝐹(𝑤𝐹𝑢))) → ∀𝑣 ∈ (Base‘𝐻)∀𝑤 ∈ (Base‘𝐻)((𝑣(+g‘𝐻)𝑤)𝐹𝑢) = (𝑣𝐹(𝑤𝐹𝑢))) | 
| 72 | 64, 71 | syldan 591 | . . . . 5
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) → ∀𝑣 ∈ (Base‘𝐻)∀𝑤 ∈ (Base‘𝐻)((𝑣(+g‘𝐻)𝑤)𝐹𝑢) = (𝑣𝐹(𝑤𝐹𝑢))) | 
| 73 | 34, 72 | jca 511 | . . . 4
⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑋) → (((0g‘𝐻)𝐹𝑢) = 𝑢 ∧ ∀𝑣 ∈ (Base‘𝐻)∀𝑤 ∈ (Base‘𝐻)((𝑣(+g‘𝐻)𝑤)𝐹𝑢) = (𝑣𝐹(𝑤𝐹𝑢)))) | 
| 74 | 73 | ralrimiva 3145 | . . 3
⊢ (𝑌 ∈ (SubGrp‘𝐺) → ∀𝑢 ∈ 𝑋 (((0g‘𝐻)𝐹𝑢) = 𝑢 ∧ ∀𝑣 ∈ (Base‘𝐻)∀𝑤 ∈ (Base‘𝐻)((𝑣(+g‘𝐻)𝑤)𝐹𝑢) = (𝑣𝐹(𝑤𝐹𝑢)))) | 
| 75 | 22, 74 | jca 511 | . 2
⊢ (𝑌 ∈ (SubGrp‘𝐺) → (𝐹:((Base‘𝐻) × 𝑋)⟶𝑋 ∧ ∀𝑢 ∈ 𝑋 (((0g‘𝐻)𝐹𝑢) = 𝑢 ∧ ∀𝑣 ∈ (Base‘𝐻)∀𝑤 ∈ (Base‘𝐻)((𝑣(+g‘𝐻)𝑤)𝐹𝑢) = (𝑣𝐹(𝑤𝐹𝑢))))) | 
| 76 |  | eqid 2736 | . . 3
⊢
(Base‘𝐻) =
(Base‘𝐻) | 
| 77 |  | eqid 2736 | . . 3
⊢
(+g‘𝐻) = (+g‘𝐻) | 
| 78 |  | eqid 2736 | . . 3
⊢
(0g‘𝐻) = (0g‘𝐻) | 
| 79 | 76, 77, 78 | isga 19310 | . 2
⊢ (𝐹 ∈ (𝐻 GrpAct 𝑋) ↔ ((𝐻 ∈ Grp ∧ 𝑋 ∈ V) ∧ (𝐹:((Base‘𝐻) × 𝑋)⟶𝑋 ∧ ∀𝑢 ∈ 𝑋 (((0g‘𝐻)𝐹𝑢) = 𝑢 ∧ ∀𝑣 ∈ (Base‘𝐻)∀𝑤 ∈ (Base‘𝐻)((𝑣(+g‘𝐻)𝑤)𝐹𝑢) = (𝑣𝐹(𝑤𝐹𝑢)))))) | 
| 80 | 5, 75, 79 | sylanbrc 583 | 1
⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝐹 ∈ (𝐻 GrpAct 𝑋)) |