Step | Hyp | Ref
| Expression |
1 | | eqidd 2623 |
. 2
⊢ (𝐴 ∈ 𝑉 → (Base‘𝐺) = (Base‘𝐺)) |
2 | | eqidd 2623 |
. 2
⊢ (𝐴 ∈ 𝑉 → (+g‘𝐺) = (+g‘𝐺)) |
3 | | symggrp.1 |
. . . 4
⊢ 𝐺 = (SymGrp‘𝐴) |
4 | | eqid 2622 |
. . . 4
⊢
(Base‘𝐺) =
(Base‘𝐺) |
5 | | eqid 2622 |
. . . 4
⊢
(+g‘𝐺) = (+g‘𝐺) |
6 | 3, 4, 5 | symgcl 17811 |
. . 3
⊢ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺)) |
7 | 6 | 3adant1 1079 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺)) |
8 | | coass 5654 |
. . . 4
⊢ ((𝑥 ∘ 𝑦) ∘ 𝑧) = (𝑥 ∘ (𝑦 ∘ 𝑧)) |
9 | | simpr1 1067 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑥 ∈ (Base‘𝐺)) |
10 | | simpr2 1068 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑦 ∈ (Base‘𝐺)) |
11 | 3, 4, 5 | symgov 17810 |
. . . . . 6
⊢ ((𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺)) → (𝑥(+g‘𝐺)𝑦) = (𝑥 ∘ 𝑦)) |
12 | 9, 10, 11 | syl2anc 693 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑥(+g‘𝐺)𝑦) = (𝑥 ∘ 𝑦)) |
13 | 12 | coeq1d 5283 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → ((𝑥(+g‘𝐺)𝑦) ∘ 𝑧) = ((𝑥 ∘ 𝑦) ∘ 𝑧)) |
14 | | simpr3 1069 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → 𝑧 ∈ (Base‘𝐺)) |
15 | 3, 4, 5 | symgov 17810 |
. . . . . 6
⊢ ((𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺)) → (𝑦(+g‘𝐺)𝑧) = (𝑦 ∘ 𝑧)) |
16 | 10, 14, 15 | syl2anc 693 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑦(+g‘𝐺)𝑧) = (𝑦 ∘ 𝑧)) |
17 | 16 | coeq2d 5284 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑥 ∘ (𝑦(+g‘𝐺)𝑧)) = (𝑥 ∘ (𝑦 ∘ 𝑧))) |
18 | 8, 13, 17 | 3eqtr4a 2682 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → ((𝑥(+g‘𝐺)𝑦) ∘ 𝑧) = (𝑥 ∘ (𝑦(+g‘𝐺)𝑧))) |
19 | 9, 10, 6 | syl2anc 693 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺)) |
20 | 3, 4, 5 | symgov 17810 |
. . . 4
⊢ (((𝑥(+g‘𝐺)𝑦) ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺)) → ((𝑥(+g‘𝐺)𝑦)(+g‘𝐺)𝑧) = ((𝑥(+g‘𝐺)𝑦) ∘ 𝑧)) |
21 | 19, 14, 20 | syl2anc 693 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → ((𝑥(+g‘𝐺)𝑦)(+g‘𝐺)𝑧) = ((𝑥(+g‘𝐺)𝑦) ∘ 𝑧)) |
22 | 3, 4, 5 | symgcl 17811 |
. . . . 5
⊢ ((𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺)) → (𝑦(+g‘𝐺)𝑧) ∈ (Base‘𝐺)) |
23 | 10, 14, 22 | syl2anc 693 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑦(+g‘𝐺)𝑧) ∈ (Base‘𝐺)) |
24 | 3, 4, 5 | symgov 17810 |
. . . 4
⊢ ((𝑥 ∈ (Base‘𝐺) ∧ (𝑦(+g‘𝐺)𝑧) ∈ (Base‘𝐺)) → (𝑥(+g‘𝐺)(𝑦(+g‘𝐺)𝑧)) = (𝑥 ∘ (𝑦(+g‘𝐺)𝑧))) |
25 | 9, 23, 24 | syl2anc 693 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → (𝑥(+g‘𝐺)(𝑦(+g‘𝐺)𝑧)) = (𝑥 ∘ (𝑦(+g‘𝐺)𝑧))) |
26 | 18, 21, 25 | 3eqtr4d 2666 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑥 ∈ (Base‘𝐺) ∧ 𝑦 ∈ (Base‘𝐺) ∧ 𝑧 ∈ (Base‘𝐺))) → ((𝑥(+g‘𝐺)𝑦)(+g‘𝐺)𝑧) = (𝑥(+g‘𝐺)(𝑦(+g‘𝐺)𝑧))) |
27 | | f1oi 6174 |
. . 3
⊢ ( I
↾ 𝐴):𝐴–1-1-onto→𝐴 |
28 | 3, 4 | elsymgbas 17802 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (( I ↾ 𝐴) ∈ (Base‘𝐺) ↔ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴)) |
29 | 27, 28 | mpbiri 248 |
. 2
⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ (Base‘𝐺)) |
30 | 3, 4, 5 | symgov 17810 |
. . . 4
⊢ ((( I
↾ 𝐴) ∈
(Base‘𝐺) ∧ 𝑥 ∈ (Base‘𝐺)) → (( I ↾ 𝐴)(+g‘𝐺)𝑥) = (( I ↾ 𝐴) ∘ 𝑥)) |
31 | 29, 30 | sylan 488 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → (( I ↾ 𝐴)(+g‘𝐺)𝑥) = (( I ↾ 𝐴) ∘ 𝑥)) |
32 | 3, 4 | elsymgbas 17802 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (Base‘𝐺) ↔ 𝑥:𝐴–1-1-onto→𝐴)) |
33 | 32 | biimpa 501 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → 𝑥:𝐴–1-1-onto→𝐴) |
34 | | f1of 6137 |
. . . 4
⊢ (𝑥:𝐴–1-1-onto→𝐴 → 𝑥:𝐴⟶𝐴) |
35 | | fcoi2 6079 |
. . . 4
⊢ (𝑥:𝐴⟶𝐴 → (( I ↾ 𝐴) ∘ 𝑥) = 𝑥) |
36 | 33, 34, 35 | 3syl 18 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → (( I ↾ 𝐴) ∘ 𝑥) = 𝑥) |
37 | 31, 36 | eqtrd 2656 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → (( I ↾ 𝐴)(+g‘𝐺)𝑥) = 𝑥) |
38 | | f1ocnv 6149 |
. . . . 5
⊢ (𝑥:𝐴–1-1-onto→𝐴 → ◡𝑥:𝐴–1-1-onto→𝐴) |
39 | 38 | a1i 11 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → (𝑥:𝐴–1-1-onto→𝐴 → ◡𝑥:𝐴–1-1-onto→𝐴)) |
40 | 3, 4 | elsymgbas 17802 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → (◡𝑥 ∈ (Base‘𝐺) ↔ ◡𝑥:𝐴–1-1-onto→𝐴)) |
41 | 39, 32, 40 | 3imtr4d 283 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ (Base‘𝐺) → ◡𝑥 ∈ (Base‘𝐺))) |
42 | 41 | imp 445 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → ◡𝑥 ∈ (Base‘𝐺)) |
43 | 3, 4, 5 | symgov 17810 |
. . . 4
⊢ ((◡𝑥 ∈ (Base‘𝐺) ∧ 𝑥 ∈ (Base‘𝐺)) → (◡𝑥(+g‘𝐺)𝑥) = (◡𝑥 ∘ 𝑥)) |
44 | 42, 43 | sylancom 701 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → (◡𝑥(+g‘𝐺)𝑥) = (◡𝑥 ∘ 𝑥)) |
45 | | f1ococnv1 6165 |
. . . 4
⊢ (𝑥:𝐴–1-1-onto→𝐴 → (◡𝑥 ∘ 𝑥) = ( I ↾ 𝐴)) |
46 | 33, 45 | syl 17 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → (◡𝑥 ∘ 𝑥) = ( I ↾ 𝐴)) |
47 | 44, 46 | eqtrd 2656 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 ∈ (Base‘𝐺)) → (◡𝑥(+g‘𝐺)𝑥) = ( I ↾ 𝐴)) |
48 | 1, 2, 7, 26, 29, 37, 42, 47 | isgrpd 17444 |
1
⊢ (𝐴 ∈ 𝑉 → 𝐺 ∈ Grp) |