Step | Hyp | Ref
| Expression |
1 | | ovres 6698 |
. . . . 5
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑍) → (𝑥( ⊕ ↾ (𝑋 × 𝑍))𝑦) = (𝑥 ⊕ 𝑦)) |
2 | 1 | adantl 481 |
. . . 4
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ( ⊕ ↾ (𝑋 × 𝑍)) ∈ (𝐺 GrpAct 𝑍)) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑍)) → (𝑥( ⊕ ↾ (𝑋 × 𝑍))𝑦) = (𝑥 ⊕ 𝑦)) |
3 | | gass.1 |
. . . . . . 7
⊢ 𝑋 = (Base‘𝐺) |
4 | 3 | gaf 17551 |
. . . . . 6
⊢ (( ⊕
↾ (𝑋 × 𝑍)) ∈ (𝐺 GrpAct 𝑍) → ( ⊕ ↾ (𝑋 × 𝑍)):(𝑋 × 𝑍)⟶𝑍) |
5 | 4 | adantl 481 |
. . . . 5
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ( ⊕ ↾ (𝑋 × 𝑍)) ∈ (𝐺 GrpAct 𝑍)) → ( ⊕ ↾ (𝑋 × 𝑍)):(𝑋 × 𝑍)⟶𝑍) |
6 | 5 | fovrnda 6703 |
. . . 4
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ( ⊕ ↾ (𝑋 × 𝑍)) ∈ (𝐺 GrpAct 𝑍)) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑍)) → (𝑥( ⊕ ↾ (𝑋 × 𝑍))𝑦) ∈ 𝑍) |
7 | 2, 6 | eqeltrrd 2689 |
. . 3
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ( ⊕ ↾ (𝑋 × 𝑍)) ∈ (𝐺 GrpAct 𝑍)) ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑍)) → (𝑥 ⊕ 𝑦) ∈ 𝑍) |
8 | 7 | ralrimivva 2954 |
. 2
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ( ⊕ ↾ (𝑋 × 𝑍)) ∈ (𝐺 GrpAct 𝑍)) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) |
9 | | gagrp 17548 |
. . . . 5
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑌) → 𝐺 ∈ Grp) |
10 | 9 | ad2antrr 758 |
. . . 4
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → 𝐺 ∈ Grp) |
11 | | gaset 17549 |
. . . . . . 7
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑌) → 𝑌 ∈ V) |
12 | 11 | adantr 480 |
. . . . . 6
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) → 𝑌 ∈ V) |
13 | | simpr 476 |
. . . . . 6
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) → 𝑍 ⊆ 𝑌) |
14 | 12, 13 | ssexd 4733 |
. . . . 5
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) → 𝑍 ∈ V) |
15 | 14 | adantr 480 |
. . . 4
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → 𝑍 ∈ V) |
16 | 10, 15 | jca 553 |
. . 3
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → (𝐺 ∈ Grp ∧ 𝑍 ∈ V)) |
17 | 3 | gaf 17551 |
. . . . . . . 8
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑌) → ⊕ :(𝑋 × 𝑌)⟶𝑌) |
18 | 17 | ad2antrr 758 |
. . . . . . 7
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → ⊕ :(𝑋 × 𝑌)⟶𝑌) |
19 | | ffn 5958 |
. . . . . . 7
⊢ ( ⊕
:(𝑋 × 𝑌)⟶𝑌 → ⊕ Fn (𝑋 × 𝑌)) |
20 | 18, 19 | syl 17 |
. . . . . 6
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → ⊕ Fn (𝑋 × 𝑌)) |
21 | | simplr 788 |
. . . . . . 7
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → 𝑍 ⊆ 𝑌) |
22 | | xpss2 5152 |
. . . . . . 7
⊢ (𝑍 ⊆ 𝑌 → (𝑋 × 𝑍) ⊆ (𝑋 × 𝑌)) |
23 | 21, 22 | syl 17 |
. . . . . 6
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → (𝑋 × 𝑍) ⊆ (𝑋 × 𝑌)) |
24 | | fnssres 5918 |
. . . . . 6
⊢ (( ⊕ Fn
(𝑋 × 𝑌) ∧ (𝑋 × 𝑍) ⊆ (𝑋 × 𝑌)) → ( ⊕ ↾ (𝑋 × 𝑍)) Fn (𝑋 × 𝑍)) |
25 | 20, 23, 24 | syl2anc 691 |
. . . . 5
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → ( ⊕ ↾ (𝑋 × 𝑍)) Fn (𝑋 × 𝑍)) |
26 | | simpr 476 |
. . . . . 6
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) |
27 | 1 | eleq1d 2672 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑍) → ((𝑥( ⊕ ↾ (𝑋 × 𝑍))𝑦) ∈ 𝑍 ↔ (𝑥 ⊕ 𝑦) ∈ 𝑍)) |
28 | 27 | ralbidva 2968 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑋 → (∀𝑦 ∈ 𝑍 (𝑥( ⊕ ↾ (𝑋 × 𝑍))𝑦) ∈ 𝑍 ↔ ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍)) |
29 | 28 | ralbiia 2962 |
. . . . . 6
⊢
(∀𝑥 ∈
𝑋 ∀𝑦 ∈ 𝑍 (𝑥( ⊕ ↾ (𝑋 × 𝑍))𝑦) ∈ 𝑍 ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) |
30 | 26, 29 | sylibr 223 |
. . . . 5
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥( ⊕ ↾ (𝑋 × 𝑍))𝑦) ∈ 𝑍) |
31 | | ffnov 6662 |
. . . . 5
⊢ (( ⊕
↾ (𝑋 × 𝑍)):(𝑋 × 𝑍)⟶𝑍 ↔ (( ⊕ ↾ (𝑋 × 𝑍)) Fn (𝑋 × 𝑍) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥( ⊕ ↾ (𝑋 × 𝑍))𝑦) ∈ 𝑍)) |
32 | 25, 30, 31 | sylanbrc 695 |
. . . 4
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → ( ⊕ ↾ (𝑋 × 𝑍)):(𝑋 × 𝑍)⟶𝑍) |
33 | | eqid 2610 |
. . . . . . . . . 10
⊢
(0g‘𝐺) = (0g‘𝐺) |
34 | 3, 33 | grpidcl 17273 |
. . . . . . . . 9
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ 𝑋) |
35 | 10, 34 | syl 17 |
. . . . . . . 8
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → (0g‘𝐺) ∈ 𝑋) |
36 | | ovres 6698 |
. . . . . . . 8
⊢
(((0g‘𝐺) ∈ 𝑋 ∧ 𝑧 ∈ 𝑍) → ((0g‘𝐺)( ⊕ ↾ (𝑋 × 𝑍))𝑧) = ((0g‘𝐺) ⊕ 𝑧)) |
37 | 35, 36 | sylan 487 |
. . . . . . 7
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) → ((0g‘𝐺)( ⊕ ↾ (𝑋 × 𝑍))𝑧) = ((0g‘𝐺) ⊕ 𝑧)) |
38 | 21 | sselda 3568 |
. . . . . . . 8
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) → 𝑧 ∈ 𝑌) |
39 | | simpll 786 |
. . . . . . . . 9
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → ⊕ ∈ (𝐺 GrpAct 𝑌)) |
40 | 33 | gagrpid 17550 |
. . . . . . . . 9
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑧 ∈ 𝑌) → ((0g‘𝐺) ⊕ 𝑧) = 𝑧) |
41 | 39, 40 | sylan 487 |
. . . . . . . 8
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑌) → ((0g‘𝐺) ⊕ 𝑧) = 𝑧) |
42 | 38, 41 | syldan 486 |
. . . . . . 7
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) → ((0g‘𝐺) ⊕ 𝑧) = 𝑧) |
43 | 37, 42 | eqtrd 2644 |
. . . . . 6
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) → ((0g‘𝐺)( ⊕ ↾ (𝑋 × 𝑍))𝑧) = 𝑧) |
44 | 39 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ⊕ ∈ (𝐺 GrpAct 𝑌)) |
45 | | simprl 790 |
. . . . . . . . . 10
⊢ (((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → 𝑢 ∈ 𝑋) |
46 | | simprr 792 |
. . . . . . . . . 10
⊢ (((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → 𝑣 ∈ 𝑋) |
47 | 38 | adantr 480 |
. . . . . . . . . 10
⊢ (((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → 𝑧 ∈ 𝑌) |
48 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(+g‘𝐺) = (+g‘𝐺) |
49 | 3, 48 | gaass 17553 |
. . . . . . . . . 10
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋 ∧ 𝑧 ∈ 𝑌)) → ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧) = (𝑢 ⊕ (𝑣 ⊕ 𝑧))) |
50 | 44, 45, 46, 47, 49 | syl13anc 1320 |
. . . . . . . . 9
⊢ (((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧) = (𝑢 ⊕ (𝑣 ⊕ 𝑧))) |
51 | | simplr 788 |
. . . . . . . . . . 11
⊢ (((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → 𝑧 ∈ 𝑍) |
52 | | simpllr 795 |
. . . . . . . . . . 11
⊢ (((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) |
53 | | ovrspc2v 6571 |
. . . . . . . . . . 11
⊢ (((𝑣 ∈ 𝑋 ∧ 𝑧 ∈ 𝑍) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → (𝑣 ⊕ 𝑧) ∈ 𝑍) |
54 | 46, 51, 52, 53 | syl21anc 1317 |
. . . . . . . . . 10
⊢ (((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑣 ⊕ 𝑧) ∈ 𝑍) |
55 | | ovres 6698 |
. . . . . . . . . 10
⊢ ((𝑢 ∈ 𝑋 ∧ (𝑣 ⊕ 𝑧) ∈ 𝑍) → (𝑢( ⊕ ↾ (𝑋 × 𝑍))(𝑣 ⊕ 𝑧)) = (𝑢 ⊕ (𝑣 ⊕ 𝑧))) |
56 | 45, 54, 55 | syl2anc 691 |
. . . . . . . . 9
⊢ (((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑢( ⊕ ↾ (𝑋 × 𝑍))(𝑣 ⊕ 𝑧)) = (𝑢 ⊕ (𝑣 ⊕ 𝑧))) |
57 | 50, 56 | eqtr4d 2647 |
. . . . . . . 8
⊢ (((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧) = (𝑢( ⊕ ↾ (𝑋 × 𝑍))(𝑣 ⊕ 𝑧))) |
58 | 10 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → 𝐺 ∈ Grp) |
59 | 3, 48 | grpcl 17253 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋) → (𝑢(+g‘𝐺)𝑣) ∈ 𝑋) |
60 | 58, 45, 46, 59 | syl3anc 1318 |
. . . . . . . . 9
⊢ (((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑢(+g‘𝐺)𝑣) ∈ 𝑋) |
61 | | ovres 6698 |
. . . . . . . . 9
⊢ (((𝑢(+g‘𝐺)𝑣) ∈ 𝑋 ∧ 𝑧 ∈ 𝑍) → ((𝑢(+g‘𝐺)𝑣)( ⊕ ↾ (𝑋 × 𝑍))𝑧) = ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧)) |
62 | 60, 51, 61 | syl2anc 691 |
. . . . . . . 8
⊢ (((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝑢(+g‘𝐺)𝑣)( ⊕ ↾ (𝑋 × 𝑍))𝑧) = ((𝑢(+g‘𝐺)𝑣) ⊕ 𝑧)) |
63 | | ovres 6698 |
. . . . . . . . . 10
⊢ ((𝑣 ∈ 𝑋 ∧ 𝑧 ∈ 𝑍) → (𝑣( ⊕ ↾ (𝑋 × 𝑍))𝑧) = (𝑣 ⊕ 𝑧)) |
64 | 46, 51, 63 | syl2anc 691 |
. . . . . . . . 9
⊢ (((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑣( ⊕ ↾ (𝑋 × 𝑍))𝑧) = (𝑣 ⊕ 𝑧)) |
65 | 64 | oveq2d 6565 |
. . . . . . . 8
⊢ (((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → (𝑢( ⊕ ↾ (𝑋 × 𝑍))(𝑣( ⊕ ↾ (𝑋 × 𝑍))𝑧)) = (𝑢( ⊕ ↾ (𝑋 × 𝑍))(𝑣 ⊕ 𝑧))) |
66 | 57, 62, 65 | 3eqtr4d 2654 |
. . . . . . 7
⊢ (((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) ∧ (𝑢 ∈ 𝑋 ∧ 𝑣 ∈ 𝑋)) → ((𝑢(+g‘𝐺)𝑣)( ⊕ ↾ (𝑋 × 𝑍))𝑧) = (𝑢( ⊕ ↾ (𝑋 × 𝑍))(𝑣( ⊕ ↾ (𝑋 × 𝑍))𝑧))) |
67 | 66 | ralrimivva 2954 |
. . . . . 6
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) → ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 ((𝑢(+g‘𝐺)𝑣)( ⊕ ↾ (𝑋 × 𝑍))𝑧) = (𝑢( ⊕ ↾ (𝑋 × 𝑍))(𝑣( ⊕ ↾ (𝑋 × 𝑍))𝑧))) |
68 | 43, 67 | jca 553 |
. . . . 5
⊢ ((((
⊕
∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) ∧ 𝑧 ∈ 𝑍) → (((0g‘𝐺)( ⊕ ↾ (𝑋 × 𝑍))𝑧) = 𝑧 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 ((𝑢(+g‘𝐺)𝑣)( ⊕ ↾ (𝑋 × 𝑍))𝑧) = (𝑢( ⊕ ↾ (𝑋 × 𝑍))(𝑣( ⊕ ↾ (𝑋 × 𝑍))𝑧)))) |
69 | 68 | ralrimiva 2949 |
. . . 4
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → ∀𝑧 ∈ 𝑍 (((0g‘𝐺)( ⊕ ↾ (𝑋 × 𝑍))𝑧) = 𝑧 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 ((𝑢(+g‘𝐺)𝑣)( ⊕ ↾ (𝑋 × 𝑍))𝑧) = (𝑢( ⊕ ↾ (𝑋 × 𝑍))(𝑣( ⊕ ↾ (𝑋 × 𝑍))𝑧)))) |
70 | 32, 69 | jca 553 |
. . 3
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → (( ⊕ ↾ (𝑋 × 𝑍)):(𝑋 × 𝑍)⟶𝑍 ∧ ∀𝑧 ∈ 𝑍 (((0g‘𝐺)( ⊕ ↾ (𝑋 × 𝑍))𝑧) = 𝑧 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 ((𝑢(+g‘𝐺)𝑣)( ⊕ ↾ (𝑋 × 𝑍))𝑧) = (𝑢( ⊕ ↾ (𝑋 × 𝑍))(𝑣( ⊕ ↾ (𝑋 × 𝑍))𝑧))))) |
71 | 3, 48, 33 | isga 17547 |
. . 3
⊢ (( ⊕
↾ (𝑋 × 𝑍)) ∈ (𝐺 GrpAct 𝑍) ↔ ((𝐺 ∈ Grp ∧ 𝑍 ∈ V) ∧ (( ⊕ ↾ (𝑋 × 𝑍)):(𝑋 × 𝑍)⟶𝑍 ∧ ∀𝑧 ∈ 𝑍 (((0g‘𝐺)( ⊕ ↾ (𝑋 × 𝑍))𝑧) = 𝑧 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 ((𝑢(+g‘𝐺)𝑣)( ⊕ ↾ (𝑋 × 𝑍))𝑧) = (𝑢( ⊕ ↾ (𝑋 × 𝑍))(𝑣( ⊕ ↾ (𝑋 × 𝑍))𝑧)))))) |
72 | 16, 70, 71 | sylanbrc 695 |
. 2
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍) → ( ⊕ ↾ (𝑋 × 𝑍)) ∈ (𝐺 GrpAct 𝑍)) |
73 | 8, 72 | impbida 873 |
1
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) → (( ⊕ ↾ (𝑋 × 𝑍)) ∈ (𝐺 GrpAct 𝑍) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍)) |