Step | Hyp | Ref
| Expression |
1 | | eqidd 2779 |
. 2
⊢ (𝐴 ∈ 𝑉 → (Base‘𝐺) = (Base‘𝐺)) |
2 | | eqidd 2779 |
. 2
⊢ (𝐴 ∈ 𝑉 → (+g‘𝐺) = (+g‘𝐺)) |
3 | | symggrp.1 |
. . . 4
⊢ 𝐺 = (SymGrp‘𝐴) |
4 | | eqid 2778 |
. . . 4
⊢
(Base‘𝐺) =
(Base‘𝐺) |
5 | | eqid 2778 |
. . . 4
⊢
(+g‘𝐺) = (+g‘𝐺) |
6 | 3, 4, 5 | symgcl 18280 |
. . 3
⊢ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺)) |
7 | 6 | 3adant1 1110 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺)) |
8 | | coass 5957 |
. . . 4
⊢ ((𝑥 ∘ 𝑦) ∘ 𝑧) = (𝑥 ∘ (𝑦 ∘ 𝑧)) |
9 | | simpr1 1174 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑥 ∈ (Base‘𝐺)) |
10 | | simpr2 1175 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑦 ∈ (Base‘𝐺)) |
11 | 3, 4, 5 | symgov 18279 |
. . . . . 6
⊢ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑥(+g‘𝐺)𝑦) = (𝑥 ∘ 𝑦)) |
12 | 9, 10, 11 | syl2anc 576 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑥(+g‘𝐺)𝑦) = (𝑥 ∘ 𝑦)) |
13 | 12 | coeq1d 5582 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → ((𝑥(+g‘𝐺)𝑦) ∘ 𝑧) = ((𝑥 ∘ 𝑦) ∘ 𝑧)) |
14 | | simpr3 1176 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑧 ∈ (Base‘𝐺)) |
15 | 3, 4, 5 | symgov 18279 |
. . . . . 6
⊢ ((𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺)) → (𝑦(+g‘𝐺)𝑧) = (𝑦 ∘ 𝑧)) |
16 | 10, 14, 15 | syl2anc 576 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑦(+g‘𝐺)𝑧) = (𝑦 ∘ 𝑧)) |
17 | 16 | coeq2d 5583 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑥 ∘ (𝑦(+g‘𝐺)𝑧)) = (𝑥 ∘ (𝑦 ∘ 𝑧))) |
18 | 8, 13, 17 | 3eqtr4a 2840 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → ((𝑥(+g‘𝐺)𝑦) ∘ 𝑧) = (𝑥 ∘ (𝑦(+g‘𝐺)𝑧))) |
19 | 9, 10, 6 | syl2anc 576 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺)) |
20 | 3, 4, 5 | symgov 18279 |
. . . 4
⊢ (((𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺)) → ((𝑥(+g‘𝐺)𝑦)(+g‘𝐺)𝑧) = ((𝑥(+g‘𝐺)𝑦) ∘ 𝑧)) |
21 | 19, 14, 20 | syl2anc 576 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → ((𝑥(+g‘𝐺)𝑦)(+g‘𝐺)𝑧) = ((𝑥(+g‘𝐺)𝑦) ∘ 𝑧)) |
22 | 3, 4, 5 | symgcl 18280 |
. . . . 5
⊢ ((𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺)) → (𝑦(+g‘𝐺)𝑧) ∈ (Base‘𝐺)) |
23 | 10, 14, 22 | syl2anc 576 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑦(+g‘𝐺)𝑧) ∈ (Base‘𝐺)) |
24 | 3, 4, 5 | symgov 18279 |
. . . 4
⊢ ((𝑥 ∈ (Base‘𝐺) ∧ (𝑦(+g‘𝐺)𝑧) ∈ (Base‘𝐺)) → (𝑥(+g‘𝐺)(𝑦(+g‘𝐺)𝑧)) = (𝑥 ∘ (𝑦(+g‘𝐺)𝑧))) |
25 | 9, 23, 24 | syl2anc 576 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑥(+g‘𝐺)(𝑦(+g‘𝐺)𝑧)) = (𝑥 ∘ (𝑦(+g‘𝐺)𝑧))) |
26 | 18, 21, 25 | 3eqtr4d 2824 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → ((𝑥(+g‘𝐺)𝑦)(+g‘𝐺)𝑧) = (𝑥(+g‘𝐺)(𝑦(+g‘𝐺)𝑧))) |
27 | | f1oi 6481 |
. . 3
⊢ ( I
↾ 𝐴):𝐴–1-1-onto→𝐴 |
28 | 3, 4 | elsymgbas 18271 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (( I ↾ 𝐴) ∈ (Base‘𝐺) ↔ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴)) |
29 | 27, 28 | mpbiri 250 |
. 2
⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ (Base‘𝐺)) |
30 | 3, 4, 5 | symgov 18279 |
. . . 4
⊢ ((( I
↾ 𝐴) ∈
(Base‘𝐺) ∧ 𝑥 ∈ (Base‘𝐺)) → (( I ↾ 𝐴)(+g‘𝐺)𝑥) = (( I ↾ 𝐴) ∘ 𝑥)) |
31 | 29, 30 | sylan 572 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → (( I ↾ 𝐴)(+g‘𝐺)𝑥) = (( I ↾ 𝐴) ∘ 𝑥)) |
32 | 3, 4 | elsymgbas 18271 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (Base‘𝐺) ↔ 𝑥:𝐴–1-1-onto→𝐴)) |
33 | 32 | biimpa 469 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → 𝑥:𝐴–1-1-onto→𝐴) |
34 | | f1of 6444 |
. . . 4
⊢ (𝑥:𝐴–1-1-onto→𝐴 → 𝑥:𝐴⟶𝐴) |
35 | | fcoi2 6382 |
. . . 4
⊢ (𝑥:𝐴⟶𝐴 → (( I ↾ 𝐴) ∘ 𝑥) = 𝑥) |
36 | 33, 34, 35 | 3syl 18 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → (( I ↾ 𝐴) ∘ 𝑥) = 𝑥) |
37 | 31, 36 | eqtrd 2814 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → (( I ↾ 𝐴)(+g‘𝐺)𝑥) = 𝑥) |
38 | | f1ocnv 6456 |
. . . . 5
⊢ (𝑥:𝐴–1-1-onto→𝐴 → ◡𝑥:𝐴–1-1-onto→𝐴) |
39 | 38 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → (𝑥:𝐴–1-1-onto→𝐴 → ◡𝑥:𝐴–1-1-onto→𝐴)) |
40 | 3, 4 | elsymgbas 18271 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → (◡𝑥 ∈ (Base‘𝐺) ↔ ◡𝑥:𝐴–1-1-onto→𝐴)) |
41 | 39, 32, 40 | 3imtr4d 286 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (Base‘𝐺) → ◡𝑥 ∈ (Base‘𝐺))) |
42 | 41 | imp 398 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → ◡𝑥 ∈ (Base‘𝐺)) |
43 | 3, 4, 5 | symgov 18279 |
. . . 4
⊢ ((◡𝑥 ∈ (Base‘𝐺) ∧ 𝑥 ∈ (Base‘𝐺)) → (◡𝑥(+g‘𝐺)𝑥) = (◡𝑥 ∘ 𝑥)) |
44 | 42, 43 | sylancom 579 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → (◡𝑥(+g‘𝐺)𝑥) = (◡𝑥 ∘ 𝑥)) |
45 | | f1ococnv1 6472 |
. . . 4
⊢ (𝑥:𝐴–1-1-onto→𝐴 → (◡𝑥 ∘ 𝑥) = ( I ↾ 𝐴)) |
46 | 33, 45 | syl 17 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → (◡𝑥 ∘ 𝑥) = ( I ↾ 𝐴)) |
47 | 44, 46 | eqtrd 2814 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → (◡𝑥(+g‘𝐺)𝑥) = ( I ↾ 𝐴)) |
48 | 1, 2, 7, 26, 29, 37, 42, 47 | isgrpd 17913 |
1
⊢ (𝐴 ∈ 𝑉 → 𝐺 ∈ Grp) |