Proof of Theorem sylow2blem1
Step | Hyp | Ref
| Expression |
1 | | simp2 1055 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → 𝐵 ∈ 𝐻) |
2 | | sylow2b.r |
. . . . 5
⊢ ∼ =
(𝐺 ~QG
𝐾) |
3 | | ovex 6577 |
. . . . 5
⊢ (𝐺 ~QG 𝐾) ∈ V |
4 | 2, 3 | eqeltri 2684 |
. . . 4
⊢ ∼ ∈
V |
5 | | simp3 1056 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → 𝐶 ∈ 𝑋) |
6 | | ecelqsg 7689 |
. . . 4
⊢ (( ∼ ∈
V ∧ 𝐶 ∈ 𝑋) → [𝐶] ∼ ∈ (𝑋 / ∼ )) |
7 | 4, 5, 6 | sylancr 694 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → [𝐶] ∼ ∈ (𝑋 / ∼ )) |
8 | | simpr 476 |
. . . . . 6
⊢ ((𝑥 = 𝐵 ∧ 𝑦 = [𝐶] ∼ ) → 𝑦 = [𝐶] ∼ ) |
9 | | simpl 472 |
. . . . . . 7
⊢ ((𝑥 = 𝐵 ∧ 𝑦 = [𝐶] ∼ ) → 𝑥 = 𝐵) |
10 | 9 | oveq1d 6564 |
. . . . . 6
⊢ ((𝑥 = 𝐵 ∧ 𝑦 = [𝐶] ∼ ) → (𝑥 + 𝑧) = (𝐵 + 𝑧)) |
11 | 8, 10 | mpteq12dv 4663 |
. . . . 5
⊢ ((𝑥 = 𝐵 ∧ 𝑦 = [𝐶] ∼ ) → (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) = (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧))) |
12 | 11 | rneqd 5274 |
. . . 4
⊢ ((𝑥 = 𝐵 ∧ 𝑦 = [𝐶] ∼ ) → ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧))) |
13 | | sylow2b.m |
. . . 4
⊢ · =
(𝑥 ∈ 𝐻, 𝑦 ∈ (𝑋 / ∼ ) ↦ ran
(𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) |
14 | | ecexg 7633 |
. . . . . . 7
⊢ ( ∼ ∈
V → [𝐶] ∼ ∈
V) |
15 | 4, 14 | ax-mp 5 |
. . . . . 6
⊢ [𝐶] ∼ ∈
V |
16 | 15 | mptex 6390 |
. . . . 5
⊢ (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) ∈ V |
17 | 16 | rnex 6992 |
. . . 4
⊢ ran
(𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) ∈ V |
18 | 12, 13, 17 | ovmpt2a 6689 |
. . 3
⊢ ((𝐵 ∈ 𝐻 ∧ [𝐶] ∼ ∈ (𝑋 / ∼ )) → (𝐵 · [𝐶] ∼ ) = ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧))) |
19 | 1, 7, 18 | syl2anc 691 |
. 2
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝐵 · [𝐶] ∼ ) = ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧))) |
20 | | sylow2b.xf |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ Fin) |
21 | | sylow2b.k |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺)) |
22 | | sylow2b.x |
. . . . . . . 8
⊢ 𝑋 = (Base‘𝐺) |
23 | 22, 2 | eqger 17467 |
. . . . . . 7
⊢ (𝐾 ∈ (SubGrp‘𝐺) → ∼ Er 𝑋) |
24 | 21, 23 | syl 17 |
. . . . . 6
⊢ (𝜑 → ∼ Er 𝑋) |
25 | 24 | ecss 7675 |
. . . . 5
⊢ (𝜑 → [(𝐵 + 𝐶)] ∼ ⊆ 𝑋) |
26 | | ssfi 8065 |
. . . . 5
⊢ ((𝑋 ∈ Fin ∧ [(𝐵 + 𝐶)] ∼ ⊆ 𝑋) → [(𝐵 + 𝐶)] ∼ ∈
Fin) |
27 | 20, 25, 26 | syl2anc 691 |
. . . 4
⊢ (𝜑 → [(𝐵 + 𝐶)] ∼ ∈
Fin) |
28 | 27 | 3ad2ant1 1075 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → [(𝐵 + 𝐶)] ∼ ∈
Fin) |
29 | | vex 3176 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
30 | | elecg 7672 |
. . . . . . . 8
⊢ ((𝑧 ∈ V ∧ 𝐶 ∈ 𝑋) → (𝑧 ∈ [𝐶] ∼ ↔ 𝐶 ∼ 𝑧)) |
31 | 29, 5, 30 | sylancr 694 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝑧 ∈ [𝐶] ∼ ↔ 𝐶 ∼ 𝑧)) |
32 | 31 | biimpa 500 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝑧 ∈ [𝐶] ∼ ) → 𝐶 ∼ 𝑧) |
33 | | sylow2b.h |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐻 ∈ (SubGrp‘𝐺)) |
34 | | subgrcl 17422 |
. . . . . . . . . . . 12
⊢ (𝐻 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ Grp) |
36 | 35 | 3ad2ant1 1075 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → 𝐺 ∈ Grp) |
37 | 22 | subgss 17418 |
. . . . . . . . . . . . 13
⊢ (𝐻 ∈ (SubGrp‘𝐺) → 𝐻 ⊆ 𝑋) |
38 | 33, 37 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐻 ⊆ 𝑋) |
39 | 38 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → 𝐻 ⊆ 𝑋) |
40 | 39, 1 | sseldd 3569 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → 𝐵 ∈ 𝑋) |
41 | | sylow2b.a |
. . . . . . . . . . 11
⊢ + =
(+g‘𝐺) |
42 | 22, 41 | grpcl 17253 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐵 + 𝐶) ∈ 𝑋) |
43 | 36, 40, 5, 42 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝐵 + 𝐶) ∈ 𝑋) |
44 | 43 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → (𝐵 + 𝐶) ∈ 𝑋) |
45 | 36 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → 𝐺 ∈ Grp) |
46 | 40 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → 𝐵 ∈ 𝑋) |
47 | 22 | subgss 17418 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ (SubGrp‘𝐺) → 𝐾 ⊆ 𝑋) |
48 | 21, 47 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ⊆ 𝑋) |
49 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(invg‘𝐺) = (invg‘𝐺) |
50 | 22, 49, 41, 2 | eqgval 17466 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Grp ∧ 𝐾 ⊆ 𝑋) → (𝐶 ∼ 𝑧 ↔ (𝐶 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐶) + 𝑧) ∈ 𝐾))) |
51 | 35, 48, 50 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶 ∼ 𝑧 ↔ (𝐶 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐶) + 𝑧) ∈ 𝐾))) |
52 | 51 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝐶 ∼ 𝑧 ↔ (𝐶 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐶) + 𝑧) ∈ 𝐾))) |
53 | 52 | biimpa 500 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → (𝐶 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐶) + 𝑧) ∈ 𝐾)) |
54 | 53 | simp2d 1067 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → 𝑧 ∈ 𝑋) |
55 | 22, 41 | grpcl 17253 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝐵 + 𝑧) ∈ 𝑋) |
56 | 45, 46, 54, 55 | syl3anc 1318 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → (𝐵 + 𝑧) ∈ 𝑋) |
57 | 22, 49 | grpinvcl 17290 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Grp ∧ (𝐵 + 𝐶) ∈ 𝑋) → ((invg‘𝐺)‘(𝐵 + 𝐶)) ∈ 𝑋) |
58 | 36, 43, 57 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ((invg‘𝐺)‘(𝐵 + 𝐶)) ∈ 𝑋) |
59 | 58 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → ((invg‘𝐺)‘(𝐵 + 𝐶)) ∈ 𝑋) |
60 | 22, 41 | grpass 17254 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧
(((invg‘𝐺)‘(𝐵 + 𝐶)) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((((invg‘𝐺)‘(𝐵 + 𝐶)) + 𝐵) + 𝑧) = (((invg‘𝐺)‘(𝐵 + 𝐶)) + (𝐵 + 𝑧))) |
61 | 45, 59, 46, 54, 60 | syl13anc 1320 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → ((((invg‘𝐺)‘(𝐵 + 𝐶)) + 𝐵) + 𝑧) = (((invg‘𝐺)‘(𝐵 + 𝐶)) + (𝐵 + 𝑧))) |
62 | 22, 41, 49 | grpinvadd 17316 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((invg‘𝐺)‘(𝐵 + 𝐶)) = (((invg‘𝐺)‘𝐶) +
((invg‘𝐺)‘𝐵))) |
63 | 36, 40, 5, 62 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ((invg‘𝐺)‘(𝐵 + 𝐶)) = (((invg‘𝐺)‘𝐶) +
((invg‘𝐺)‘𝐵))) |
64 | 22, 49 | grpinvcl 17290 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 ∈ Grp ∧ 𝐶 ∈ 𝑋) → ((invg‘𝐺)‘𝐶) ∈ 𝑋) |
65 | 36, 5, 64 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ((invg‘𝐺)‘𝐶) ∈ 𝑋) |
66 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢
(-g‘𝐺) = (-g‘𝐺) |
67 | 22, 41, 49, 66 | grpsubval 17288 |
. . . . . . . . . . . . . . . 16
⊢
((((invg‘𝐺)‘𝐶) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((invg‘𝐺)‘𝐶)(-g‘𝐺)𝐵) = (((invg‘𝐺)‘𝐶) +
((invg‘𝐺)‘𝐵))) |
68 | 65, 40, 67 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (((invg‘𝐺)‘𝐶)(-g‘𝐺)𝐵) = (((invg‘𝐺)‘𝐶) +
((invg‘𝐺)‘𝐵))) |
69 | 63, 68 | eqtr4d 2647 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ((invg‘𝐺)‘(𝐵 + 𝐶)) = (((invg‘𝐺)‘𝐶)(-g‘𝐺)𝐵)) |
70 | 69 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (((invg‘𝐺)‘(𝐵 + 𝐶)) + 𝐵) = ((((invg‘𝐺)‘𝐶)(-g‘𝐺)𝐵) + 𝐵)) |
71 | 22, 41, 66 | grpnpcan 17330 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Grp ∧
((invg‘𝐺)‘𝐶) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((((invg‘𝐺)‘𝐶)(-g‘𝐺)𝐵) + 𝐵) = ((invg‘𝐺)‘𝐶)) |
72 | 36, 65, 40, 71 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ((((invg‘𝐺)‘𝐶)(-g‘𝐺)𝐵) + 𝐵) = ((invg‘𝐺)‘𝐶)) |
73 | 70, 72 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (((invg‘𝐺)‘(𝐵 + 𝐶)) + 𝐵) = ((invg‘𝐺)‘𝐶)) |
74 | 73 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ((((invg‘𝐺)‘(𝐵 + 𝐶)) + 𝐵) + 𝑧) = (((invg‘𝐺)‘𝐶) + 𝑧)) |
75 | 74 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → ((((invg‘𝐺)‘(𝐵 + 𝐶)) + 𝐵) + 𝑧) = (((invg‘𝐺)‘𝐶) + 𝑧)) |
76 | 61, 75 | eqtr3d 2646 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → (((invg‘𝐺)‘(𝐵 + 𝐶)) + (𝐵 + 𝑧)) = (((invg‘𝐺)‘𝐶) + 𝑧)) |
77 | 53 | simp3d 1068 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → (((invg‘𝐺)‘𝐶) + 𝑧) ∈ 𝐾) |
78 | 76, 77 | eqeltrd 2688 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → (((invg‘𝐺)‘(𝐵 + 𝐶)) + (𝐵 + 𝑧)) ∈ 𝐾) |
79 | 22, 49, 41, 2 | eqgval 17466 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝐾 ⊆ 𝑋) → ((𝐵 + 𝐶) ∼ (𝐵 + 𝑧) ↔ ((𝐵 + 𝐶) ∈ 𝑋 ∧ (𝐵 + 𝑧) ∈ 𝑋 ∧ (((invg‘𝐺)‘(𝐵 + 𝐶)) + (𝐵 + 𝑧)) ∈ 𝐾))) |
80 | 35, 48, 79 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐵 + 𝐶) ∼ (𝐵 + 𝑧) ↔ ((𝐵 + 𝐶) ∈ 𝑋 ∧ (𝐵 + 𝑧) ∈ 𝑋 ∧ (((invg‘𝐺)‘(𝐵 + 𝐶)) + (𝐵 + 𝑧)) ∈ 𝐾))) |
81 | 80 | 3ad2ant1 1075 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ((𝐵 + 𝐶) ∼ (𝐵 + 𝑧) ↔ ((𝐵 + 𝐶) ∈ 𝑋 ∧ (𝐵 + 𝑧) ∈ 𝑋 ∧ (((invg‘𝐺)‘(𝐵 + 𝐶)) + (𝐵 + 𝑧)) ∈ 𝐾))) |
82 | 81 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → ((𝐵 + 𝐶) ∼ (𝐵 + 𝑧) ↔ ((𝐵 + 𝐶) ∈ 𝑋 ∧ (𝐵 + 𝑧) ∈ 𝑋 ∧ (((invg‘𝐺)‘(𝐵 + 𝐶)) + (𝐵 + 𝑧)) ∈ 𝐾))) |
83 | 44, 56, 78, 82 | mpbir3and 1238 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → (𝐵 + 𝐶) ∼ (𝐵 + 𝑧)) |
84 | | ovex 6577 |
. . . . . . . 8
⊢ (𝐵 + 𝑧) ∈ V |
85 | | ovex 6577 |
. . . . . . . 8
⊢ (𝐵 + 𝐶) ∈ V |
86 | 84, 85 | elec 7673 |
. . . . . . 7
⊢ ((𝐵 + 𝑧) ∈ [(𝐵 + 𝐶)] ∼ ↔ (𝐵 + 𝐶) ∼ (𝐵 + 𝑧)) |
87 | 83, 86 | sylibr 223 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → (𝐵 + 𝑧) ∈ [(𝐵 + 𝐶)] ∼ ) |
88 | 32, 87 | syldan 486 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝑧 ∈ [𝐶] ∼ ) → (𝐵 + 𝑧) ∈ [(𝐵 + 𝐶)] ∼ ) |
89 | | eqid 2610 |
. . . . 5
⊢ (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) = (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) |
90 | 88, 89 | fmptd 6292 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)):[𝐶] ∼ ⟶[(𝐵 + 𝐶)] ∼ ) |
91 | | frn 5966 |
. . . 4
⊢ ((𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)):[𝐶] ∼ ⟶[(𝐵 + 𝐶)] ∼ → ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) ⊆ [(𝐵 + 𝐶)] ∼ ) |
92 | 90, 91 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) ⊆ [(𝐵 + 𝐶)] ∼ ) |
93 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)) = (𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)) |
94 | 22, 41, 93 | grplmulf1o 17312 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)):𝑋–1-1-onto→𝑋) |
95 | 36, 40, 94 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)):𝑋–1-1-onto→𝑋) |
96 | | f1of1 6049 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)):𝑋–1-1-onto→𝑋 → (𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)):𝑋–1-1→𝑋) |
97 | 95, 96 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)):𝑋–1-1→𝑋) |
98 | 24 | ecss 7675 |
. . . . . . . . 9
⊢ (𝜑 → [𝐶] ∼ ⊆ 𝑋) |
99 | 98 | 3ad2ant1 1075 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → [𝐶] ∼ ⊆ 𝑋) |
100 | | f1ssres 6021 |
. . . . . . . 8
⊢ (((𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)):𝑋–1-1→𝑋 ∧ [𝐶] ∼ ⊆ 𝑋) → ((𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)) ↾ [𝐶] ∼ ):[𝐶] ∼ –1-1→𝑋) |
101 | 97, 99, 100 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ((𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)) ↾ [𝐶] ∼ ):[𝐶] ∼ –1-1→𝑋) |
102 | | resmpt 5369 |
. . . . . . . 8
⊢ ([𝐶] ∼ ⊆ 𝑋 → ((𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)) ↾ [𝐶] ∼ ) = (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧))) |
103 | | f1eq1 6009 |
. . . . . . . 8
⊢ (((𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)) ↾ [𝐶] ∼ ) = (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) → (((𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)) ↾ [𝐶] ∼ ):[𝐶] ∼ –1-1→𝑋 ↔ (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)):[𝐶] ∼ –1-1→𝑋)) |
104 | 99, 102, 103 | 3syl 18 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (((𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)) ↾ [𝐶] ∼ ):[𝐶] ∼ –1-1→𝑋 ↔ (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)):[𝐶] ∼ –1-1→𝑋)) |
105 | 101, 104 | mpbid 221 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)):[𝐶] ∼ –1-1→𝑋) |
106 | | f1f1orn 6061 |
. . . . . 6
⊢ ((𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)):[𝐶] ∼ –1-1→𝑋 → (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)):[𝐶] ∼ –1-1-onto→ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧))) |
107 | 105, 106 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)):[𝐶] ∼ –1-1-onto→ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧))) |
108 | 15 | f1oen 7862 |
. . . . 5
⊢ ((𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)):[𝐶] ∼ –1-1-onto→ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) → [𝐶] ∼ ≈ ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧))) |
109 | | ensym 7891 |
. . . . 5
⊢ ([𝐶] ∼ ≈ ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) → ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) ≈ [𝐶] ∼ ) |
110 | 107, 108,
109 | 3syl 18 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) ≈ [𝐶] ∼ ) |
111 | 21 | 3ad2ant1 1075 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → 𝐾 ∈ (SubGrp‘𝐺)) |
112 | 22, 2 | eqgen 17470 |
. . . . . . 7
⊢ ((𝐾 ∈ (SubGrp‘𝐺) ∧ [𝐶] ∼ ∈ (𝑋 / ∼ )) → 𝐾 ≈ [𝐶] ∼ ) |
113 | 111, 7, 112 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → 𝐾 ≈ [𝐶] ∼ ) |
114 | | ensym 7891 |
. . . . . 6
⊢ (𝐾 ≈ [𝐶] ∼ → [𝐶] ∼ ≈ 𝐾) |
115 | 113, 114 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → [𝐶] ∼ ≈ 𝐾) |
116 | | ecelqsg 7689 |
. . . . . . 7
⊢ (( ∼ ∈
V ∧ (𝐵 + 𝐶) ∈ 𝑋) → [(𝐵 + 𝐶)] ∼ ∈ (𝑋 / ∼ )) |
117 | 4, 43, 116 | sylancr 694 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → [(𝐵 + 𝐶)] ∼ ∈ (𝑋 / ∼ )) |
118 | 22, 2 | eqgen 17470 |
. . . . . 6
⊢ ((𝐾 ∈ (SubGrp‘𝐺) ∧ [(𝐵 + 𝐶)] ∼ ∈ (𝑋 / ∼ )) → 𝐾 ≈ [(𝐵 + 𝐶)] ∼ ) |
119 | 111, 117,
118 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → 𝐾 ≈ [(𝐵 + 𝐶)] ∼ ) |
120 | | entr 7894 |
. . . . 5
⊢ (([𝐶] ∼ ≈ 𝐾 ∧ 𝐾 ≈ [(𝐵 + 𝐶)] ∼ ) → [𝐶] ∼ ≈ [(𝐵 + 𝐶)] ∼ ) |
121 | 115, 119,
120 | syl2anc 691 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → [𝐶] ∼ ≈ [(𝐵 + 𝐶)] ∼ ) |
122 | | entr 7894 |
. . . 4
⊢ ((ran
(𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) ≈ [𝐶] ∼ ∧ [𝐶] ∼ ≈ [(𝐵 + 𝐶)] ∼ ) → ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) ≈ [(𝐵 + 𝐶)] ∼ ) |
123 | 110, 121,
122 | syl2anc 691 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) ≈ [(𝐵 + 𝐶)] ∼ ) |
124 | | fisseneq 8056 |
. . 3
⊢ (([(𝐵 + 𝐶)] ∼ ∈ Fin ∧
ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) ⊆ [(𝐵 + 𝐶)] ∼ ∧ ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) ≈ [(𝐵 + 𝐶)] ∼ ) → ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) = [(𝐵 + 𝐶)] ∼ ) |
125 | 28, 92, 123, 124 | syl3anc 1318 |
. 2
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) = [(𝐵 + 𝐶)] ∼ ) |
126 | 19, 125 | eqtrd 2644 |
1
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝐵 · [𝐶] ∼ ) = [(𝐵 + 𝐶)] ∼ ) |