Step | Hyp | Ref
| Expression |
1 | | sylow3lem2.h |
. 2
⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐾) = 𝐾} |
2 | | sylow3lem2.n |
. . . . 5
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝐾 ↔ (𝑦 + 𝑥) ∈ 𝐾)} |
3 | 2 | ssrab3 3995 |
. . . 4
⊢ 𝑁 ⊆ 𝑋 |
4 | | sseqin2 4130 |
. . . 4
⊢ (𝑁 ⊆ 𝑋 ↔ (𝑋 ∩ 𝑁) = 𝑁) |
5 | 3, 4 | mpbi 233 |
. . 3
⊢ (𝑋 ∩ 𝑁) = 𝑁 |
6 | | simpr 488 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → 𝑢 ∈ 𝑋) |
7 | | sylow3lem2.k |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ (𝑃 pSyl 𝐺)) |
8 | 7 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → 𝐾 ∈ (𝑃 pSyl 𝐺)) |
9 | | mptexg 7037 |
. . . . . . . . 9
⊢ (𝐾 ∈ (𝑃 pSyl 𝐺) → (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V) |
10 | | rnexg 7682 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V → ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V) |
11 | 8, 9, 10 | 3syl 18 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V) |
12 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → 𝑦 = 𝐾) |
13 | | simpl 486 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → 𝑥 = 𝑢) |
14 | 13 | oveq1d 7228 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → (𝑥 + 𝑧) = (𝑢 + 𝑧)) |
15 | 14, 13 | oveq12d 7231 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → ((𝑥 + 𝑧) − 𝑥) = ((𝑢 + 𝑧) − 𝑢)) |
16 | 12, 15 | mpteq12dv 5140 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))) |
17 | 16 | rneqd 5807 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑢 ∧ 𝑦 = 𝐾) → ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥)) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))) |
18 | | sylow3lem1.m |
. . . . . . . . 9
⊢ ⊕ =
(𝑥 ∈ 𝑋, 𝑦 ∈ (𝑃 pSyl 𝐺) ↦ ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥))) |
19 | 17, 18 | ovmpoga 7363 |
. . . . . . . 8
⊢ ((𝑢 ∈ 𝑋 ∧ 𝐾 ∈ (𝑃 pSyl 𝐺) ∧ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ∈ V) → (𝑢 ⊕ 𝐾) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))) |
20 | 6, 8, 11, 19 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → (𝑢 ⊕ 𝐾) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))) |
21 | 20 | adantr 484 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ 𝑢 ∈ 𝑁) → (𝑢 ⊕ 𝐾) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))) |
22 | | slwsubg 18999 |
. . . . . . . . 9
⊢ (𝐾 ∈ (𝑃 pSyl 𝐺) → 𝐾 ∈ (SubGrp‘𝐺)) |
23 | 7, 22 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺)) |
24 | 23 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → 𝐾 ∈ (SubGrp‘𝐺)) |
25 | | sylow3.x |
. . . . . . . 8
⊢ 𝑋 = (Base‘𝐺) |
26 | | sylow3lem1.a |
. . . . . . . 8
⊢ + =
(+g‘𝐺) |
27 | | sylow3lem1.d |
. . . . . . . 8
⊢ − =
(-g‘𝐺) |
28 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) = (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) |
29 | 25, 26, 27, 28, 2 | conjnmz 18656 |
. . . . . . 7
⊢ ((𝐾 ∈ (SubGrp‘𝐺) ∧ 𝑢 ∈ 𝑁) → 𝐾 = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))) |
30 | 24, 29 | sylan 583 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ 𝑢 ∈ 𝑁) → 𝐾 = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))) |
31 | 21, 30 | eqtr4d 2780 |
. . . . 5
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ 𝑢 ∈ 𝑁) → (𝑢 ⊕ 𝐾) = 𝐾) |
32 | | simplr 769 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ (𝑢 ⊕ 𝐾) = 𝐾) → 𝑢 ∈ 𝑋) |
33 | | simprl 771 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → (𝑢 ⊕ 𝐾) = 𝐾) |
34 | 20 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → (𝑢 ⊕ 𝐾) = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))) |
35 | 33, 34 | eqtr3d 2779 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → 𝐾 = ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))) |
36 | 35 | eleq2d 2823 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → ((𝑢 + 𝑤) ∈ 𝐾 ↔ (𝑢 + 𝑤) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))) |
37 | | ovex 7246 |
. . . . . . . . . . . 12
⊢ (𝑢 + 𝑤) ∈ V |
38 | | eqeq1 2741 |
. . . . . . . . . . . . 13
⊢ (𝑣 = (𝑢 + 𝑤) → (𝑣 = ((𝑢 + 𝑧) − 𝑢) ↔ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) |
39 | 38 | rexbidv 3216 |
. . . . . . . . . . . 12
⊢ (𝑣 = (𝑢 + 𝑤) → (∃𝑧 ∈ 𝐾 𝑣 = ((𝑢 + 𝑧) − 𝑢) ↔ ∃𝑧 ∈ 𝐾 (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) |
40 | 28 | rnmpt 5824 |
. . . . . . . . . . . 12
⊢ ran
(𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) = {𝑣 ∣ ∃𝑧 ∈ 𝐾 𝑣 = ((𝑢 + 𝑧) − 𝑢)} |
41 | 37, 39, 40 | elab2 3591 |
. . . . . . . . . . 11
⊢ ((𝑢 + 𝑤) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ↔ ∃𝑧 ∈ 𝐾 (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢)) |
42 | | simprr 773 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢)) |
43 | | sylow3.g |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐺 ∈ Grp) |
44 | 43 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → 𝐺 ∈ Grp) |
45 | | simpllr 776 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → 𝑢 ∈ 𝑋) |
46 | 25 | subgss 18544 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐾 ∈ (SubGrp‘𝐺) → 𝐾 ⊆ 𝑋) |
47 | 23, 46 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐾 ⊆ 𝑋) |
48 | 47 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → 𝐾 ⊆ 𝑋) |
49 | | simprl 771 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → 𝑧 ∈ 𝐾) |
50 | 48, 49 | sseldd 3902 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → 𝑧 ∈ 𝑋) |
51 | 25, 26, 27 | grpaddsubass 18453 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 ∈ Grp ∧ (𝑢 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋)) → ((𝑢 + 𝑧) − 𝑢) = (𝑢 + (𝑧 − 𝑢))) |
52 | 44, 45, 50, 45, 51 | syl13anc 1374 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → ((𝑢 + 𝑧) − 𝑢) = (𝑢 + (𝑧 − 𝑢))) |
53 | 42, 52 | eqtr2d 2778 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → (𝑢 + (𝑧 − 𝑢)) = (𝑢 + 𝑤)) |
54 | 25, 27 | grpsubcl 18443 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 ∈ Grp ∧ 𝑧 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋) → (𝑧 − 𝑢) ∈ 𝑋) |
55 | 44, 50, 45, 54 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → (𝑧 − 𝑢) ∈ 𝑋) |
56 | | simplrr 778 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → 𝑤 ∈ 𝑋) |
57 | 25, 26 | grplcan 18425 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ∈ Grp ∧ ((𝑧 − 𝑢) ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋)) → ((𝑢 + (𝑧 − 𝑢)) = (𝑢 + 𝑤) ↔ (𝑧 − 𝑢) = 𝑤)) |
58 | 44, 55, 56, 45, 57 | syl13anc 1374 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → ((𝑢 + (𝑧 − 𝑢)) = (𝑢 + 𝑤) ↔ (𝑧 − 𝑢) = 𝑤)) |
59 | 53, 58 | mpbid 235 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → (𝑧 − 𝑢) = 𝑤) |
60 | 25, 26, 27 | grpsubadd 18451 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ Grp ∧ (𝑧 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋)) → ((𝑧 − 𝑢) = 𝑤 ↔ (𝑤 + 𝑢) = 𝑧)) |
61 | 44, 50, 45, 56, 60 | syl13anc 1374 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → ((𝑧 − 𝑢) = 𝑤 ↔ (𝑤 + 𝑢) = 𝑧)) |
62 | 59, 61 | mpbid 235 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → (𝑤 + 𝑢) = 𝑧) |
63 | 62, 49 | eqeltrd 2838 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑧 ∈ 𝐾 ∧ (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢))) → (𝑤 + 𝑢) ∈ 𝐾) |
64 | 63 | rexlimdvaa 3204 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → (∃𝑧 ∈ 𝐾 (𝑢 + 𝑤) = ((𝑢 + 𝑧) − 𝑢) → (𝑤 + 𝑢) ∈ 𝐾)) |
65 | 41, 64 | syl5bi 245 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → ((𝑢 + 𝑤) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) → (𝑤 + 𝑢) ∈ 𝐾)) |
66 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → (𝑤 + 𝑢) ∈ 𝐾) |
67 | | oveq2 7221 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑤 + 𝑢) → (𝑢 + 𝑧) = (𝑢 + (𝑤 + 𝑢))) |
68 | 67 | oveq1d 7228 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑤 + 𝑢) → ((𝑢 + 𝑧) − 𝑢) = ((𝑢 + (𝑤 + 𝑢)) − 𝑢)) |
69 | | ovex 7246 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 + (𝑤 + 𝑢)) − 𝑢) ∈ V |
70 | 68, 28, 69 | fvmpt 6818 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 + 𝑢) ∈ 𝐾 → ((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))‘(𝑤 + 𝑢)) = ((𝑢 + (𝑤 + 𝑢)) − 𝑢)) |
71 | 66, 70 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → ((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))‘(𝑤 + 𝑢)) = ((𝑢 + (𝑤 + 𝑢)) − 𝑢)) |
72 | 43 | ad3antrrr 730 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → 𝐺 ∈ Grp) |
73 | | simpllr 776 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → 𝑢 ∈ 𝑋) |
74 | | simplrr 778 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → 𝑤 ∈ 𝑋) |
75 | 25, 26 | grpass 18374 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ Grp ∧ (𝑢 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝑢 ∈ 𝑋)) → ((𝑢 + 𝑤) + 𝑢) = (𝑢 + (𝑤 + 𝑢))) |
76 | 72, 73, 74, 73, 75 | syl13anc 1374 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → ((𝑢 + 𝑤) + 𝑢) = (𝑢 + (𝑤 + 𝑢))) |
77 | 76 | oveq1d 7228 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → (((𝑢 + 𝑤) + 𝑢) − 𝑢) = ((𝑢 + (𝑤 + 𝑢)) − 𝑢)) |
78 | 25, 26 | grpcl 18373 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ Grp ∧ 𝑢 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋) → (𝑢 + 𝑤) ∈ 𝑋) |
79 | 72, 73, 74, 78 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → (𝑢 + 𝑤) ∈ 𝑋) |
80 | 25, 26, 27 | grppncan 18454 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Grp ∧ (𝑢 + 𝑤) ∈ 𝑋 ∧ 𝑢 ∈ 𝑋) → (((𝑢 + 𝑤) + 𝑢) − 𝑢) = (𝑢 + 𝑤)) |
81 | 72, 79, 73, 80 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → (((𝑢 + 𝑤) + 𝑢) − 𝑢) = (𝑢 + 𝑤)) |
82 | 71, 77, 81 | 3eqtr2d 2783 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → ((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))‘(𝑤 + 𝑢)) = (𝑢 + 𝑤)) |
83 | | ovex 7246 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 + 𝑧) − 𝑢) ∈ V |
84 | 83, 28 | fnmpti 6521 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) Fn 𝐾 |
85 | | fnfvelrn 6901 |
. . . . . . . . . . . . 13
⊢ (((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) Fn 𝐾 ∧ (𝑤 + 𝑢) ∈ 𝐾) → ((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))‘(𝑤 + 𝑢)) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))) |
86 | 84, 66, 85 | sylancr 590 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → ((𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))‘(𝑤 + 𝑢)) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))) |
87 | 82, 86 | eqeltrrd 2839 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) ∧ (𝑤 + 𝑢) ∈ 𝐾) → (𝑢 + 𝑤) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢))) |
88 | 87 | ex 416 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → ((𝑤 + 𝑢) ∈ 𝐾 → (𝑢 + 𝑤) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)))) |
89 | 65, 88 | impbid 215 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → ((𝑢 + 𝑤) ∈ ran (𝑧 ∈ 𝐾 ↦ ((𝑢 + 𝑧) − 𝑢)) ↔ (𝑤 + 𝑢) ∈ 𝐾)) |
90 | 36, 89 | bitrd 282 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ ((𝑢 ⊕ 𝐾) = 𝐾 ∧ 𝑤 ∈ 𝑋)) → ((𝑢 + 𝑤) ∈ 𝐾 ↔ (𝑤 + 𝑢) ∈ 𝐾)) |
91 | 90 | anassrs 471 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ (𝑢 ⊕ 𝐾) = 𝐾) ∧ 𝑤 ∈ 𝑋) → ((𝑢 + 𝑤) ∈ 𝐾 ↔ (𝑤 + 𝑢) ∈ 𝐾)) |
92 | 91 | ralrimiva 3105 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ (𝑢 ⊕ 𝐾) = 𝐾) → ∀𝑤 ∈ 𝑋 ((𝑢 + 𝑤) ∈ 𝐾 ↔ (𝑤 + 𝑢) ∈ 𝐾)) |
93 | 2 | elnmz 18579 |
. . . . . 6
⊢ (𝑢 ∈ 𝑁 ↔ (𝑢 ∈ 𝑋 ∧ ∀𝑤 ∈ 𝑋 ((𝑢 + 𝑤) ∈ 𝐾 ↔ (𝑤 + 𝑢) ∈ 𝐾))) |
94 | 32, 92, 93 | sylanbrc 586 |
. . . . 5
⊢ (((𝜑 ∧ 𝑢 ∈ 𝑋) ∧ (𝑢 ⊕ 𝐾) = 𝐾) → 𝑢 ∈ 𝑁) |
95 | 31, 94 | impbida 801 |
. . . 4
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑋) → (𝑢 ∈ 𝑁 ↔ (𝑢 ⊕ 𝐾) = 𝐾)) |
96 | 95 | rabbi2dva 4132 |
. . 3
⊢ (𝜑 → (𝑋 ∩ 𝑁) = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐾) = 𝐾}) |
97 | 5, 96 | eqtr3id 2792 |
. 2
⊢ (𝜑 → 𝑁 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐾) = 𝐾}) |
98 | 1, 97 | eqtr4id 2797 |
1
⊢ (𝜑 → 𝐻 = 𝑁) |