Step | Hyp | Ref
| Expression |
1 | | imasgrp.u |
. . . 4
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) |
2 | | imasgrp.v |
. . . 4
⊢ (𝜑 → 𝑉 = (Base‘𝑅)) |
3 | | imasgrp.f |
. . . 4
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) |
4 | | imasgrp2.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ 𝑊) |
5 | 1, 2, 3, 4 | imasbas 17211 |
. . 3
⊢ (𝜑 → 𝐵 = (Base‘𝑈)) |
6 | | eqidd 2739 |
. . 3
⊢ (𝜑 → (+g‘𝑈) = (+g‘𝑈)) |
7 | | imasgrp.e |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)))) |
8 | | imasgrp.p |
. . . . . . . . . 10
⊢ (𝜑 → + =
(+g‘𝑅)) |
9 | 8 | oveqd 7285 |
. . . . . . . . 9
⊢ (𝜑 → (𝑎 + 𝑏) = (𝑎(+g‘𝑅)𝑏)) |
10 | 9 | fveq2d 6771 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑎(+g‘𝑅)𝑏))) |
11 | 8 | oveqd 7285 |
. . . . . . . . 9
⊢ (𝜑 → (𝑝 + 𝑞) = (𝑝(+g‘𝑅)𝑞)) |
12 | 11 | fveq2d 6771 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘(𝑝 + 𝑞)) = (𝐹‘(𝑝(+g‘𝑅)𝑞))) |
13 | 10, 12 | eqeq12d 2754 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)) ↔ (𝐹‘(𝑎(+g‘𝑅)𝑏)) = (𝐹‘(𝑝(+g‘𝑅)𝑞)))) |
14 | 13 | 3ad2ant1 1132 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → ((𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)) ↔ (𝐹‘(𝑎(+g‘𝑅)𝑏)) = (𝐹‘(𝑝(+g‘𝑅)𝑞)))) |
15 | 7, 14 | sylibd 238 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎(+g‘𝑅)𝑏)) = (𝐹‘(𝑝(+g‘𝑅)𝑞)))) |
16 | | eqid 2738 |
. . . . 5
⊢
(+g‘𝑅) = (+g‘𝑅) |
17 | | eqid 2738 |
. . . . 5
⊢
(+g‘𝑈) = (+g‘𝑈) |
18 | 11 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 + 𝑞) = (𝑝(+g‘𝑅)𝑞)) |
19 | | imasgrp2.1 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 + 𝑦) ∈ 𝑉) |
20 | 19 | 3expb 1119 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑥 + 𝑦) ∈ 𝑉) |
21 | 20 | caovclg 7455 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝 + 𝑞) ∈ 𝑉) |
22 | 18, 21 | eqeltrrd 2840 |
. . . . 5
⊢ ((𝜑 ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (𝑝(+g‘𝑅)𝑞) ∈ 𝑉) |
23 | 3, 15, 1, 2, 4, 16,
17, 22 | imasaddf 17232 |
. . . 4
⊢ (𝜑 → (+g‘𝑈):(𝐵 × 𝐵)⟶𝐵) |
24 | | fovrn 7433 |
. . . 4
⊢
(((+g‘𝑈):(𝐵 × 𝐵)⟶𝐵 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) → (𝑢(+g‘𝑈)𝑣) ∈ 𝐵) |
25 | 23, 24 | syl3an1 1162 |
. . 3
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) → (𝑢(+g‘𝑈)𝑣) ∈ 𝐵) |
26 | | forn 6684 |
. . . . . . . . . 10
⊢ (𝐹:𝑉–onto→𝐵 → ran 𝐹 = 𝐵) |
27 | 3, 26 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝐹 = 𝐵) |
28 | 27 | eleq2d 2824 |
. . . . . . . 8
⊢ (𝜑 → (𝑢 ∈ ran 𝐹 ↔ 𝑢 ∈ 𝐵)) |
29 | 27 | eleq2d 2824 |
. . . . . . . 8
⊢ (𝜑 → (𝑣 ∈ ran 𝐹 ↔ 𝑣 ∈ 𝐵)) |
30 | 27 | eleq2d 2824 |
. . . . . . . 8
⊢ (𝜑 → (𝑤 ∈ ran 𝐹 ↔ 𝑤 ∈ 𝐵)) |
31 | 28, 29, 30 | 3anbi123d 1435 |
. . . . . . 7
⊢ (𝜑 → ((𝑢 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹 ∧ 𝑤 ∈ ran 𝐹) ↔ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵))) |
32 | | fofn 6683 |
. . . . . . . . 9
⊢ (𝐹:𝑉–onto→𝐵 → 𝐹 Fn 𝑉) |
33 | 3, 32 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 Fn 𝑉) |
34 | | fvelrnb 6823 |
. . . . . . . . 9
⊢ (𝐹 Fn 𝑉 → (𝑢 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢)) |
35 | | fvelrnb 6823 |
. . . . . . . . 9
⊢ (𝐹 Fn 𝑉 → (𝑣 ∈ ran 𝐹 ↔ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣)) |
36 | | fvelrnb 6823 |
. . . . . . . . 9
⊢ (𝐹 Fn 𝑉 → (𝑤 ∈ ran 𝐹 ↔ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤)) |
37 | 34, 35, 36 | 3anbi123d 1435 |
. . . . . . . 8
⊢ (𝐹 Fn 𝑉 → ((𝑢 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹 ∧ 𝑤 ∈ ran 𝐹) ↔ (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 ∧ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣 ∧ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤))) |
38 | 33, 37 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((𝑢 ∈ ran 𝐹 ∧ 𝑣 ∈ ran 𝐹 ∧ 𝑤 ∈ ran 𝐹) ↔ (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 ∧ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣 ∧ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤))) |
39 | 31, 38 | bitr3d 280 |
. . . . . 6
⊢ (𝜑 → ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 ∧ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣 ∧ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤))) |
40 | | 3reeanv 3293 |
. . . . . 6
⊢
(∃𝑥 ∈
𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 ((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) ↔ (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 ∧ ∃𝑦 ∈ 𝑉 (𝐹‘𝑦) = 𝑣 ∧ ∃𝑧 ∈ 𝑉 (𝐹‘𝑧) = 𝑤)) |
41 | 39, 40 | bitr4di 289 |
. . . . 5
⊢ (𝜑 → ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ↔ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 ((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤))) |
42 | | imasgrp2.2 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘((𝑥 + 𝑦) + 𝑧)) = (𝐹‘(𝑥 + (𝑦 + 𝑧)))) |
43 | 8 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → + =
(+g‘𝑅)) |
44 | 43 | oveqd 7285 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 + 𝑦) + 𝑧) = ((𝑥 + 𝑦)(+g‘𝑅)𝑧)) |
45 | 44 | fveq2d 6771 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘((𝑥 + 𝑦) + 𝑧)) = (𝐹‘((𝑥 + 𝑦)(+g‘𝑅)𝑧))) |
46 | 43 | oveqd 7285 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑥 + (𝑦 + 𝑧)) = (𝑥(+g‘𝑅)(𝑦 + 𝑧))) |
47 | 46 | fveq2d 6771 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘(𝑥 + (𝑦 + 𝑧))) = (𝐹‘(𝑥(+g‘𝑅)(𝑦 + 𝑧)))) |
48 | 42, 45, 47 | 3eqtr3d 2786 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘((𝑥 + 𝑦)(+g‘𝑅)𝑧)) = (𝐹‘(𝑥(+g‘𝑅)(𝑦 + 𝑧)))) |
49 | | simpl 483 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝜑) |
50 | 19 | 3adant3r3 1183 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑥 + 𝑦) ∈ 𝑉) |
51 | | simpr3 1195 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑧 ∈ 𝑉) |
52 | 3, 15, 1, 2, 4, 16,
17 | imasaddval 17231 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 + 𝑦) ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → ((𝐹‘(𝑥 + 𝑦))(+g‘𝑈)(𝐹‘𝑧)) = (𝐹‘((𝑥 + 𝑦)(+g‘𝑅)𝑧))) |
53 | 49, 50, 51, 52 | syl3anc 1370 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘(𝑥 + 𝑦))(+g‘𝑈)(𝐹‘𝑧)) = (𝐹‘((𝑥 + 𝑦)(+g‘𝑅)𝑧))) |
54 | | simpr1 1193 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → 𝑥 ∈ 𝑉) |
55 | 21 | caovclg 7455 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑦 + 𝑧) ∈ 𝑉) |
56 | 55 | 3adantr1 1168 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑦 + 𝑧) ∈ 𝑉) |
57 | 3, 15, 1, 2, 4, 16,
17 | imasaddval 17231 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ (𝑦 + 𝑧) ∈ 𝑉) → ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘(𝑦 + 𝑧))) = (𝐹‘(𝑥(+g‘𝑅)(𝑦 + 𝑧)))) |
58 | 49, 54, 56, 57 | syl3anc 1370 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘(𝑦 + 𝑧))) = (𝐹‘(𝑥(+g‘𝑅)(𝑦 + 𝑧)))) |
59 | 48, 53, 58 | 3eqtr4d 2788 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘(𝑥 + 𝑦))(+g‘𝑈)(𝐹‘𝑧)) = ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘(𝑦 + 𝑧)))) |
60 | 3, 15, 1, 2, 4, 16,
17 | imasaddval 17231 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦)) = (𝐹‘(𝑥(+g‘𝑅)𝑦))) |
61 | 60 | 3adant3r3 1183 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦)) = (𝐹‘(𝑥(+g‘𝑅)𝑦))) |
62 | 43 | oveqd 7285 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑥 + 𝑦) = (𝑥(+g‘𝑅)𝑦)) |
63 | 62 | fveq2d 6771 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘(𝑥 + 𝑦)) = (𝐹‘(𝑥(+g‘𝑅)𝑦))) |
64 | 61, 63 | eqtr4d 2781 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦)) = (𝐹‘(𝑥 + 𝑦))) |
65 | 64 | oveq1d 7283 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦))(+g‘𝑈)(𝐹‘𝑧)) = ((𝐹‘(𝑥 + 𝑦))(+g‘𝑈)(𝐹‘𝑧))) |
66 | 3, 15, 1, 2, 4, 16,
17 | imasaddval 17231 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉) → ((𝐹‘𝑦)(+g‘𝑈)(𝐹‘𝑧)) = (𝐹‘(𝑦(+g‘𝑅)𝑧))) |
67 | 66 | 3adant3r1 1181 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑦)(+g‘𝑈)(𝐹‘𝑧)) = (𝐹‘(𝑦(+g‘𝑅)𝑧))) |
68 | 43 | oveqd 7285 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝑦 + 𝑧) = (𝑦(+g‘𝑅)𝑧)) |
69 | 68 | fveq2d 6771 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘(𝑦 + 𝑧)) = (𝐹‘(𝑦(+g‘𝑅)𝑧))) |
70 | 67, 69 | eqtr4d 2781 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑦)(+g‘𝑈)(𝐹‘𝑧)) = (𝐹‘(𝑦 + 𝑧))) |
71 | 70 | oveq2d 7284 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝐹‘𝑥)(+g‘𝑈)((𝐹‘𝑦)(+g‘𝑈)(𝐹‘𝑧))) = ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘(𝑦 + 𝑧)))) |
72 | 59, 65, 71 | 3eqtr4d 2788 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦))(+g‘𝑈)(𝐹‘𝑧)) = ((𝐹‘𝑥)(+g‘𝑈)((𝐹‘𝑦)(+g‘𝑈)(𝐹‘𝑧)))) |
73 | | simp1 1135 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → (𝐹‘𝑥) = 𝑢) |
74 | | simp2 1136 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → (𝐹‘𝑦) = 𝑣) |
75 | 73, 74 | oveq12d 7286 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦)) = (𝑢(+g‘𝑈)𝑣)) |
76 | | simp3 1137 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → (𝐹‘𝑧) = 𝑤) |
77 | 75, 76 | oveq12d 7286 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → (((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦))(+g‘𝑈)(𝐹‘𝑧)) = ((𝑢(+g‘𝑈)𝑣)(+g‘𝑈)𝑤)) |
78 | 74, 76 | oveq12d 7286 |
. . . . . . . . . . . 12
⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝐹‘𝑦)(+g‘𝑈)(𝐹‘𝑧)) = (𝑣(+g‘𝑈)𝑤)) |
79 | 73, 78 | oveq12d 7286 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝐹‘𝑥)(+g‘𝑈)((𝐹‘𝑦)(+g‘𝑈)(𝐹‘𝑧))) = (𝑢(+g‘𝑈)(𝑣(+g‘𝑈)𝑤))) |
80 | 77, 79 | eqeq12d 2754 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((((𝐹‘𝑥)(+g‘𝑈)(𝐹‘𝑦))(+g‘𝑈)(𝐹‘𝑧)) = ((𝐹‘𝑥)(+g‘𝑈)((𝐹‘𝑦)(+g‘𝑈)(𝐹‘𝑧))) ↔ ((𝑢(+g‘𝑈)𝑣)(+g‘𝑈)𝑤) = (𝑢(+g‘𝑈)(𝑣(+g‘𝑈)𝑤)))) |
81 | 72, 80 | syl5ibcom 244 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+g‘𝑈)𝑣)(+g‘𝑈)𝑤) = (𝑢(+g‘𝑈)(𝑣(+g‘𝑈)𝑤)))) |
82 | 81 | 3exp2 1353 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝑉 → (𝑦 ∈ 𝑉 → (𝑧 ∈ 𝑉 → (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+g‘𝑈)𝑣)(+g‘𝑈)𝑤) = (𝑢(+g‘𝑈)(𝑣(+g‘𝑈)𝑤))))))) |
83 | 82 | imp32 419 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑧 ∈ 𝑉 → (((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+g‘𝑈)𝑣)(+g‘𝑈)𝑤) = (𝑢(+g‘𝑈)(𝑣(+g‘𝑈)𝑤))))) |
84 | 83 | rexlimdv 3210 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (∃𝑧 ∈ 𝑉 ((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+g‘𝑈)𝑣)(+g‘𝑈)𝑤) = (𝑢(+g‘𝑈)(𝑣(+g‘𝑈)𝑤)))) |
85 | 84 | rexlimdvva 3221 |
. . . . 5
⊢ (𝜑 → (∃𝑥 ∈ 𝑉 ∃𝑦 ∈ 𝑉 ∃𝑧 ∈ 𝑉 ((𝐹‘𝑥) = 𝑢 ∧ (𝐹‘𝑦) = 𝑣 ∧ (𝐹‘𝑧) = 𝑤) → ((𝑢(+g‘𝑈)𝑣)(+g‘𝑈)𝑤) = (𝑢(+g‘𝑈)(𝑣(+g‘𝑈)𝑤)))) |
86 | 41, 85 | sylbid 239 |
. . . 4
⊢ (𝜑 → ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) → ((𝑢(+g‘𝑈)𝑣)(+g‘𝑈)𝑤) = (𝑢(+g‘𝑈)(𝑣(+g‘𝑈)𝑤)))) |
87 | 86 | imp 407 |
. . 3
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵)) → ((𝑢(+g‘𝑈)𝑣)(+g‘𝑈)𝑤) = (𝑢(+g‘𝑈)(𝑣(+g‘𝑈)𝑤))) |
88 | | fof 6681 |
. . . . 5
⊢ (𝐹:𝑉–onto→𝐵 → 𝐹:𝑉⟶𝐵) |
89 | 3, 88 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐹:𝑉⟶𝐵) |
90 | | imasgrp2.3 |
. . . 4
⊢ (𝜑 → 0 ∈ 𝑉) |
91 | 89, 90 | ffvelrnd 6955 |
. . 3
⊢ (𝜑 → (𝐹‘ 0 ) ∈ 𝐵) |
92 | 33, 34 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑢 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢)) |
93 | 28, 92 | bitr3d 280 |
. . . . 5
⊢ (𝜑 → (𝑢 ∈ 𝐵 ↔ ∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢)) |
94 | | simpl 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝜑) |
95 | 90 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 0 ∈ 𝑉) |
96 | | simpr 485 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑥 ∈ 𝑉) |
97 | 3, 15, 1, 2, 4, 16,
17 | imasaddval 17231 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 0 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘ 0
)(+g‘𝑈)(𝐹‘𝑥)) = (𝐹‘( 0 (+g‘𝑅)𝑥))) |
98 | 94, 95, 96, 97 | syl3anc 1370 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘ 0
)(+g‘𝑈)(𝐹‘𝑥)) = (𝐹‘( 0 (+g‘𝑅)𝑥))) |
99 | 8 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → + =
(+g‘𝑅)) |
100 | 99 | oveqd 7285 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ( 0 + 𝑥) = ( 0 (+g‘𝑅)𝑥)) |
101 | 100 | fveq2d 6771 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘( 0 + 𝑥)) = (𝐹‘( 0 (+g‘𝑅)𝑥))) |
102 | | imasgrp2.4 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘( 0 + 𝑥)) = (𝐹‘𝑥)) |
103 | 98, 101, 102 | 3eqtr2d 2784 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘ 0
)(+g‘𝑈)(𝐹‘𝑥)) = (𝐹‘𝑥)) |
104 | | oveq2 7276 |
. . . . . . . 8
⊢ ((𝐹‘𝑥) = 𝑢 → ((𝐹‘ 0
)(+g‘𝑈)(𝐹‘𝑥)) = ((𝐹‘ 0
)(+g‘𝑈)𝑢)) |
105 | | id 22 |
. . . . . . . 8
⊢ ((𝐹‘𝑥) = 𝑢 → (𝐹‘𝑥) = 𝑢) |
106 | 104, 105 | eqeq12d 2754 |
. . . . . . 7
⊢ ((𝐹‘𝑥) = 𝑢 → (((𝐹‘ 0
)(+g‘𝑈)(𝐹‘𝑥)) = (𝐹‘𝑥) ↔ ((𝐹‘ 0
)(+g‘𝑈)𝑢) = 𝑢)) |
107 | 103, 106 | syl5ibcom 244 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑥) = 𝑢 → ((𝐹‘ 0
)(+g‘𝑈)𝑢) = 𝑢)) |
108 | 107 | rexlimdva 3211 |
. . . . 5
⊢ (𝜑 → (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 → ((𝐹‘ 0
)(+g‘𝑈)𝑢) = 𝑢)) |
109 | 93, 108 | sylbid 239 |
. . . 4
⊢ (𝜑 → (𝑢 ∈ 𝐵 → ((𝐹‘ 0
)(+g‘𝑈)𝑢) = 𝑢)) |
110 | 109 | imp 407 |
. . 3
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) → ((𝐹‘ 0
)(+g‘𝑈)𝑢) = 𝑢) |
111 | 89 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝐹:𝑉⟶𝐵) |
112 | | imasgrp2.5 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑁 ∈ 𝑉) |
113 | 111, 112 | ffvelrnd 6955 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘𝑁) ∈ 𝐵) |
114 | 3, 15, 1, 2, 4, 16,
17 | imasaddval 17231 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑁)(+g‘𝑈)(𝐹‘𝑥)) = (𝐹‘(𝑁(+g‘𝑅)𝑥))) |
115 | 94, 112, 96, 114 | syl3anc 1370 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑁)(+g‘𝑈)(𝐹‘𝑥)) = (𝐹‘(𝑁(+g‘𝑅)𝑥))) |
116 | 99 | oveqd 7285 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝑁 + 𝑥) = (𝑁(+g‘𝑅)𝑥)) |
117 | 116 | fveq2d 6771 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘(𝑁 + 𝑥)) = (𝐹‘(𝑁(+g‘𝑅)𝑥))) |
118 | | imasgrp2.6 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘(𝑁 + 𝑥)) = (𝐹‘ 0 )) |
119 | 115, 117,
118 | 3eqtr2d 2784 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑁)(+g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 )) |
120 | | oveq1 7275 |
. . . . . . . . . 10
⊢ (𝑣 = (𝐹‘𝑁) → (𝑣(+g‘𝑈)(𝐹‘𝑥)) = ((𝐹‘𝑁)(+g‘𝑈)(𝐹‘𝑥))) |
121 | 120 | eqeq1d 2740 |
. . . . . . . . 9
⊢ (𝑣 = (𝐹‘𝑁) → ((𝑣(+g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ) ↔ ((𝐹‘𝑁)(+g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ))) |
122 | 121 | rspcev 3560 |
. . . . . . . 8
⊢ (((𝐹‘𝑁) ∈ 𝐵 ∧ ((𝐹‘𝑁)(+g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 )) → ∃𝑣 ∈ 𝐵 (𝑣(+g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 )) |
123 | 113, 119,
122 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ∃𝑣 ∈ 𝐵 (𝑣(+g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 )) |
124 | | oveq2 7276 |
. . . . . . . . 9
⊢ ((𝐹‘𝑥) = 𝑢 → (𝑣(+g‘𝑈)(𝐹‘𝑥)) = (𝑣(+g‘𝑈)𝑢)) |
125 | 124 | eqeq1d 2740 |
. . . . . . . 8
⊢ ((𝐹‘𝑥) = 𝑢 → ((𝑣(+g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ) ↔ (𝑣(+g‘𝑈)𝑢) = (𝐹‘ 0 ))) |
126 | 125 | rexbidv 3224 |
. . . . . . 7
⊢ ((𝐹‘𝑥) = 𝑢 → (∃𝑣 ∈ 𝐵 (𝑣(+g‘𝑈)(𝐹‘𝑥)) = (𝐹‘ 0 ) ↔ ∃𝑣 ∈ 𝐵 (𝑣(+g‘𝑈)𝑢) = (𝐹‘ 0 ))) |
127 | 123, 126 | syl5ibcom 244 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝐹‘𝑥) = 𝑢 → ∃𝑣 ∈ 𝐵 (𝑣(+g‘𝑈)𝑢) = (𝐹‘ 0 ))) |
128 | 127 | rexlimdva 3211 |
. . . . 5
⊢ (𝜑 → (∃𝑥 ∈ 𝑉 (𝐹‘𝑥) = 𝑢 → ∃𝑣 ∈ 𝐵 (𝑣(+g‘𝑈)𝑢) = (𝐹‘ 0 ))) |
129 | 93, 128 | sylbid 239 |
. . . 4
⊢ (𝜑 → (𝑢 ∈ 𝐵 → ∃𝑣 ∈ 𝐵 (𝑣(+g‘𝑈)𝑢) = (𝐹‘ 0 ))) |
130 | 129 | imp 407 |
. . 3
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐵) → ∃𝑣 ∈ 𝐵 (𝑣(+g‘𝑈)𝑢) = (𝐹‘ 0 )) |
131 | 5, 6, 25, 87, 91, 110, 130 | isgrpde 18588 |
. 2
⊢ (𝜑 → 𝑈 ∈ Grp) |
132 | 5, 6, 91, 110, 131 | grpidd2 18605 |
. 2
⊢ (𝜑 → (𝐹‘ 0 ) =
(0g‘𝑈)) |
133 | 131, 132 | jca 512 |
1
⊢ (𝜑 → (𝑈 ∈ Grp ∧ (𝐹‘ 0 ) =
(0g‘𝑈))) |