Step | Hyp | Ref
| Expression |
1 | | df-ga 17546 |
. . 3
⊢ GrpAct =
(𝑔 ∈ Grp, 𝑠 ∈ V ↦
⦋(Base‘𝑔) / 𝑏⦌{𝑚 ∈ (𝑠 ↑𝑚 (𝑏 × 𝑠)) ∣ ∀𝑥 ∈ 𝑠 (((0g‘𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑦(+g‘𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))}) |
2 | 1 | elmpt2cl 6774 |
. 2
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑌) → (𝐺 ∈ Grp ∧ 𝑌 ∈ V)) |
3 | | fvex 6113 |
. . . . . . . 8
⊢
(Base‘𝑔)
∈ V |
4 | 3 | a1i 11 |
. . . . . . 7
⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) → (Base‘𝑔) ∈ V) |
5 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → 𝑠 = 𝑌) |
6 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑏 = (Base‘𝑔) → 𝑏 = (Base‘𝑔)) |
7 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) → 𝑔 = 𝐺) |
8 | 7 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) → (Base‘𝑔) = (Base‘𝐺)) |
9 | | isga.1 |
. . . . . . . . . . . 12
⊢ 𝑋 = (Base‘𝐺) |
10 | 8, 9 | syl6eqr 2662 |
. . . . . . . . . . 11
⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) → (Base‘𝑔) = 𝑋) |
11 | 6, 10 | sylan9eqr 2666 |
. . . . . . . . . 10
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → 𝑏 = 𝑋) |
12 | 11, 5 | xpeq12d 5064 |
. . . . . . . . 9
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (𝑏 × 𝑠) = (𝑋 × 𝑌)) |
13 | 5, 12 | oveq12d 6567 |
. . . . . . . 8
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (𝑠 ↑𝑚 (𝑏 × 𝑠)) = (𝑌 ↑𝑚 (𝑋 × 𝑌))) |
14 | | simpll 786 |
. . . . . . . . . . . . . 14
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → 𝑔 = 𝐺) |
15 | 14 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (0g‘𝑔) = (0g‘𝐺)) |
16 | | isga.3 |
. . . . . . . . . . . . 13
⊢ 0 =
(0g‘𝐺) |
17 | 15, 16 | syl6eqr 2662 |
. . . . . . . . . . . 12
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (0g‘𝑔) = 0 ) |
18 | 17 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → ((0g‘𝑔)𝑚𝑥) = ( 0 𝑚𝑥)) |
19 | 18 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (((0g‘𝑔)𝑚𝑥) = 𝑥 ↔ ( 0 𝑚𝑥) = 𝑥)) |
20 | 14 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (+g‘𝑔) = (+g‘𝐺)) |
21 | | isga.2 |
. . . . . . . . . . . . . . . 16
⊢ + =
(+g‘𝐺) |
22 | 20, 21 | syl6eqr 2662 |
. . . . . . . . . . . . . . 15
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (+g‘𝑔) = + ) |
23 | 22 | oveqd 6566 |
. . . . . . . . . . . . . 14
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (𝑦(+g‘𝑔)𝑧) = (𝑦 + 𝑧)) |
24 | 23 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → ((𝑦(+g‘𝑔)𝑧)𝑚𝑥) = ((𝑦 + 𝑧)𝑚𝑥)) |
25 | 24 | eqeq1d 2612 |
. . . . . . . . . . . 12
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (((𝑦(+g‘𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)) ↔ ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))) |
26 | 11, 25 | raleqbidv 3129 |
. . . . . . . . . . 11
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (∀𝑧 ∈ 𝑏 ((𝑦(+g‘𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)) ↔ ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))) |
27 | 11, 26 | raleqbidv 3129 |
. . . . . . . . . 10
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑦(+g‘𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)) ↔ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))) |
28 | 19, 27 | anbi12d 743 |
. . . . . . . . 9
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → ((((0g‘𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑦(+g‘𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))) ↔ (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))))) |
29 | 5, 28 | raleqbidv 3129 |
. . . . . . . 8
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → (∀𝑥 ∈ 𝑠 (((0g‘𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑦(+g‘𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))) ↔ ∀𝑥 ∈ 𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))))) |
30 | 13, 29 | rabeqbidv 3168 |
. . . . . . 7
⊢ (((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) ∧ 𝑏 = (Base‘𝑔)) → {𝑚 ∈ (𝑠 ↑𝑚 (𝑏 × 𝑠)) ∣ ∀𝑥 ∈ 𝑠 (((0g‘𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑦(+g‘𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))} = {𝑚 ∈ (𝑌 ↑𝑚 (𝑋 × 𝑌)) ∣ ∀𝑥 ∈ 𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))}) |
31 | 4, 30 | csbied 3526 |
. . . . . 6
⊢ ((𝑔 = 𝐺 ∧ 𝑠 = 𝑌) → ⦋(Base‘𝑔) / 𝑏⦌{𝑚 ∈ (𝑠 ↑𝑚 (𝑏 × 𝑠)) ∣ ∀𝑥 ∈ 𝑠 (((0g‘𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑦(+g‘𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))} = {𝑚 ∈ (𝑌 ↑𝑚 (𝑋 × 𝑌)) ∣ ∀𝑥 ∈ 𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))}) |
32 | | ovex 6577 |
. . . . . . 7
⊢ (𝑌 ↑𝑚
(𝑋 × 𝑌)) ∈ V |
33 | 32 | rabex 4740 |
. . . . . 6
⊢ {𝑚 ∈ (𝑌 ↑𝑚 (𝑋 × 𝑌)) ∣ ∀𝑥 ∈ 𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))} ∈ V |
34 | 31, 1, 33 | ovmpt2a 6689 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → (𝐺 GrpAct 𝑌) = {𝑚 ∈ (𝑌 ↑𝑚 (𝑋 × 𝑌)) ∣ ∀𝑥 ∈ 𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))}) |
35 | 34 | eleq2d 2673 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → ( ⊕ ∈
(𝐺 GrpAct 𝑌) ↔ ⊕ ∈ {𝑚 ∈ (𝑌 ↑𝑚 (𝑋 × 𝑌)) ∣ ∀𝑥 ∈ 𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))})) |
36 | | oveq 6555 |
. . . . . . . 8
⊢ (𝑚 = ⊕ → ( 0 𝑚𝑥) = ( 0 ⊕ 𝑥)) |
37 | 36 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑚 = ⊕ → (( 0 𝑚𝑥) = 𝑥 ↔ ( 0 ⊕ 𝑥) = 𝑥)) |
38 | | oveq 6555 |
. . . . . . . . 9
⊢ (𝑚 = ⊕ → ((𝑦 + 𝑧)𝑚𝑥) = ((𝑦 + 𝑧) ⊕ 𝑥)) |
39 | | oveq 6555 |
. . . . . . . . . 10
⊢ (𝑚 = ⊕ → (𝑦𝑚(𝑧𝑚𝑥)) = (𝑦 ⊕ (𝑧𝑚𝑥))) |
40 | | oveq 6555 |
. . . . . . . . . . 11
⊢ (𝑚 = ⊕ → (𝑧𝑚𝑥) = (𝑧 ⊕ 𝑥)) |
41 | 40 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑚 = ⊕ → (𝑦 ⊕ (𝑧𝑚𝑥)) = (𝑦 ⊕ (𝑧 ⊕ 𝑥))) |
42 | 39, 41 | eqtrd 2644 |
. . . . . . . . 9
⊢ (𝑚 = ⊕ → (𝑦𝑚(𝑧𝑚𝑥)) = (𝑦 ⊕ (𝑧 ⊕ 𝑥))) |
43 | 38, 42 | eqeq12d 2625 |
. . . . . . . 8
⊢ (𝑚 = ⊕ → (((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)) ↔ ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥)))) |
44 | 43 | 2ralbidv 2972 |
. . . . . . 7
⊢ (𝑚 = ⊕ →
(∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)) ↔ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥)))) |
45 | 37, 44 | anbi12d 743 |
. . . . . 6
⊢ (𝑚 = ⊕ → ((( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))) ↔ (( 0 ⊕ 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥))))) |
46 | 45 | ralbidv 2969 |
. . . . 5
⊢ (𝑚 = ⊕ →
(∀𝑥 ∈ 𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥))) ↔ ∀𝑥 ∈ 𝑌 (( 0 ⊕ 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥))))) |
47 | 46 | elrab 3331 |
. . . 4
⊢ ( ⊕ ∈
{𝑚 ∈ (𝑌 ↑𝑚
(𝑋 × 𝑌)) ∣ ∀𝑥 ∈ 𝑌 (( 0 𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))} ↔ ( ⊕ ∈ (𝑌 ↑𝑚
(𝑋 × 𝑌)) ∧ ∀𝑥 ∈ 𝑌 (( 0 ⊕ 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥))))) |
48 | 35, 47 | syl6bb 275 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → ( ⊕ ∈
(𝐺 GrpAct 𝑌) ↔ ( ⊕ ∈ (𝑌 ↑𝑚
(𝑋 × 𝑌)) ∧ ∀𝑥 ∈ 𝑌 (( 0 ⊕ 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥)))))) |
49 | | simpr 476 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → 𝑌 ∈ V) |
50 | | fvex 6113 |
. . . . . . 7
⊢
(Base‘𝐺)
∈ V |
51 | 9, 50 | eqeltri 2684 |
. . . . . 6
⊢ 𝑋 ∈ V |
52 | | xpexg 6858 |
. . . . . 6
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → (𝑋 × 𝑌) ∈ V) |
53 | 51, 49, 52 | sylancr 694 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → (𝑋 × 𝑌) ∈ V) |
54 | 49, 53 | elmapd 7758 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → ( ⊕ ∈
(𝑌
↑𝑚 (𝑋 × 𝑌)) ↔ ⊕ :(𝑋 × 𝑌)⟶𝑌)) |
55 | 54 | anbi1d 737 |
. . 3
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → (( ⊕ ∈
(𝑌
↑𝑚 (𝑋 × 𝑌)) ∧ ∀𝑥 ∈ 𝑌 (( 0 ⊕ 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥)))) ↔ ( ⊕ :(𝑋 × 𝑌)⟶𝑌 ∧ ∀𝑥 ∈ 𝑌 (( 0 ⊕ 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥)))))) |
56 | 48, 55 | bitrd 267 |
. 2
⊢ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) → ( ⊕ ∈
(𝐺 GrpAct 𝑌) ↔ ( ⊕ :(𝑋 × 𝑌)⟶𝑌 ∧ ∀𝑥 ∈ 𝑌 (( 0 ⊕ 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥)))))) |
57 | 2, 56 | biadan2 672 |
1
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑌) ↔ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) ∧ ( ⊕ :(𝑋 × 𝑌)⟶𝑌 ∧ ∀𝑥 ∈ 𝑌 (( 0 ⊕ 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥)))))) |