Proof of Theorem sylow2blem1
Step | Hyp | Ref
| Expression |
1 | | simp2 1062 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → 𝐵 ∈ 𝐻) |
2 | | sylow2b.r |
. . . . 5
⊢ ∼ =
(𝐺 ~QG
𝐾) |
3 | | ovex 6678 |
. . . . 5
⊢ (𝐺 ~QG 𝐾) ∈ V |
4 | 2, 3 | eqeltri 2697 |
. . . 4
⊢ ∼ ∈
V |
5 | | simp3 1063 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → 𝐶 ∈ 𝑋) |
6 | | ecelqsg 7802 |
. . . 4
⊢ (( ∼ ∈
V ∧ 𝐶 ∈ 𝑋) → [𝐶] ∼ ∈ (𝑋 / ∼ )) |
7 | 4, 5, 6 | sylancr 695 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → [𝐶] ∼ ∈ (𝑋 / ∼ )) |
8 | | simpr 477 |
. . . . . 6
⊢ ((𝑥 = 𝐵 ∧ 𝑦 = [𝐶] ∼ ) → 𝑦 = [𝐶] ∼ ) |
9 | | simpl 473 |
. . . . . . 7
⊢ ((𝑥 = 𝐵 ∧ 𝑦 = [𝐶] ∼ ) → 𝑥 = 𝐵) |
10 | 9 | oveq1d 6665 |
. . . . . 6
⊢ ((𝑥 = 𝐵 ∧ 𝑦 = [𝐶] ∼ ) → (𝑥 + 𝑧) = (𝐵 + 𝑧)) |
11 | 8, 10 | mpteq12dv 4733 |
. . . . 5
⊢ ((𝑥 = 𝐵 ∧ 𝑦 = [𝐶] ∼ ) → (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) = (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧))) |
12 | 11 | rneqd 5353 |
. . . 4
⊢ ((𝑥 = 𝐵 ∧ 𝑦 = [𝐶] ∼ ) → ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧))) |
13 | | sylow2b.m |
. . . 4
⊢ · =
(𝑥 ∈ 𝐻, 𝑦 ∈ (𝑋 / ∼ ) ↦ ran
(𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) |
14 | | ecexg 7746 |
. . . . . . 7
⊢ ( ∼ ∈
V → [𝐶] ∼ ∈
V) |
15 | 4, 14 | ax-mp 5 |
. . . . . 6
⊢ [𝐶] ∼ ∈
V |
16 | 15 | mptex 6486 |
. . . . 5
⊢ (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) ∈ V |
17 | 16 | rnex 7100 |
. . . 4
⊢ ran
(𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) ∈ V |
18 | 12, 13, 17 | ovmpt2a 6791 |
. . 3
⊢ ((𝐵 ∈ 𝐻 ∧ [𝐶] ∼ ∈ (𝑋 / ∼ )) → (𝐵 · [𝐶] ∼ ) = ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧))) |
19 | 1, 7, 18 | syl2anc 693 |
. 2
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝐵 · [𝐶] ∼ ) = ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧))) |
20 | | sylow2b.xf |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ Fin) |
21 | | sylow2b.k |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺)) |
22 | | sylow2b.x |
. . . . . . . 8
⊢ 𝑋 = (Base‘𝐺) |
23 | 22, 2 | eqger 17644 |
. . . . . . 7
⊢ (𝐾 ∈ (SubGrp‘𝐺) → ∼ Er 𝑋) |
24 | 21, 23 | syl 17 |
. . . . . 6
⊢ (𝜑 → ∼ Er 𝑋) |
25 | 24 | ecss 7788 |
. . . . 5
⊢ (𝜑 → [(𝐵 + 𝐶)] ∼ ⊆ 𝑋) |
26 | | ssfi 8180 |
. . . . 5
⊢ ((𝑋 ∈ Fin ∧ [(𝐵 + 𝐶)] ∼ ⊆ 𝑋) → [(𝐵 + 𝐶)] ∼ ∈
Fin) |
27 | 20, 25, 26 | syl2anc 693 |
. . . 4
⊢ (𝜑 → [(𝐵 + 𝐶)] ∼ ∈
Fin) |
28 | 27 | 3ad2ant1 1082 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → [(𝐵 + 𝐶)] ∼ ∈
Fin) |
29 | | vex 3203 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
30 | | elecg 7785 |
. . . . . . . 8
⊢ ((𝑧 ∈ V ∧ 𝐶 ∈ 𝑋) → (𝑧 ∈ [𝐶] ∼ ↔ 𝐶 ∼ 𝑧)) |
31 | 29, 5, 30 | sylancr 695 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝑧 ∈ [𝐶] ∼ ↔ 𝐶 ∼ 𝑧)) |
32 | 31 | biimpa 501 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝑧 ∈ [𝐶] ∼ ) → 𝐶 ∼ 𝑧) |
33 | | sylow2b.h |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐻 ∈ (SubGrp‘𝐺)) |
34 | | subgrcl 17599 |
. . . . . . . . . . . 12
⊢ (𝐻 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ Grp) |
36 | 35 | 3ad2ant1 1082 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → 𝐺 ∈ Grp) |
37 | 22 | subgss 17595 |
. . . . . . . . . . . . 13
⊢ (𝐻 ∈ (SubGrp‘𝐺) → 𝐻 ⊆ 𝑋) |
38 | 33, 37 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐻 ⊆ 𝑋) |
39 | 38 | 3ad2ant1 1082 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → 𝐻 ⊆ 𝑋) |
40 | 39, 1 | sseldd 3604 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → 𝐵 ∈ 𝑋) |
41 | | sylow2b.a |
. . . . . . . . . . 11
⊢ + =
(+g‘𝐺) |
42 | 22, 41 | grpcl 17430 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐵 + 𝐶) ∈ 𝑋) |
43 | 36, 40, 5, 42 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝐵 + 𝐶) ∈ 𝑋) |
44 | 43 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → (𝐵 + 𝐶) ∈ 𝑋) |
45 | 36 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → 𝐺 ∈ Grp) |
46 | 40 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → 𝐵 ∈ 𝑋) |
47 | 22 | subgss 17595 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ (SubGrp‘𝐺) → 𝐾 ⊆ 𝑋) |
48 | 21, 47 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ⊆ 𝑋) |
49 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(invg‘𝐺) = (invg‘𝐺) |
50 | 22, 49, 41, 2 | eqgval 17643 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Grp ∧ 𝐾 ⊆ 𝑋) → (𝐶 ∼ 𝑧 ↔ (𝐶 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐶) + 𝑧) ∈ 𝐾))) |
51 | 35, 48, 50 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶 ∼ 𝑧 ↔ (𝐶 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐶) + 𝑧) ∈ 𝐾))) |
52 | 51 | 3ad2ant1 1082 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝐶 ∼ 𝑧 ↔ (𝐶 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐶) + 𝑧) ∈ 𝐾))) |
53 | 52 | biimpa 501 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → (𝐶 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐶) + 𝑧) ∈ 𝐾)) |
54 | 53 | simp2d 1074 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → 𝑧 ∈ 𝑋) |
55 | 22, 41 | grpcl 17430 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝐵 + 𝑧) ∈ 𝑋) |
56 | 45, 46, 54, 55 | syl3anc 1326 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → (𝐵 + 𝑧) ∈ 𝑋) |
57 | 22, 49 | grpinvcl 17467 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Grp ∧ (𝐵 + 𝐶) ∈ 𝑋) → ((invg‘𝐺)‘(𝐵 + 𝐶)) ∈ 𝑋) |
58 | 36, 43, 57 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ((invg‘𝐺)‘(𝐵 + 𝐶)) ∈ 𝑋) |
59 | 58 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → ((invg‘𝐺)‘(𝐵 + 𝐶)) ∈ 𝑋) |
60 | 22, 41 | grpass 17431 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧
(((invg‘𝐺)‘(𝐵 + 𝐶)) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((((invg‘𝐺)‘(𝐵 + 𝐶)) + 𝐵) + 𝑧) = (((invg‘𝐺)‘(𝐵 + 𝐶)) + (𝐵 + 𝑧))) |
61 | 45, 59, 46, 54, 60 | syl13anc 1328 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → ((((invg‘𝐺)‘(𝐵 + 𝐶)) + 𝐵) + 𝑧) = (((invg‘𝐺)‘(𝐵 + 𝐶)) + (𝐵 + 𝑧))) |
62 | 22, 41, 49 | grpinvadd 17493 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((invg‘𝐺)‘(𝐵 + 𝐶)) = (((invg‘𝐺)‘𝐶) +
((invg‘𝐺)‘𝐵))) |
63 | 36, 40, 5, 62 | syl3anc 1326 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ((invg‘𝐺)‘(𝐵 + 𝐶)) = (((invg‘𝐺)‘𝐶) +
((invg‘𝐺)‘𝐵))) |
64 | 22, 49 | grpinvcl 17467 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 ∈ Grp ∧ 𝐶 ∈ 𝑋) → ((invg‘𝐺)‘𝐶) ∈ 𝑋) |
65 | 36, 5, 64 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ((invg‘𝐺)‘𝐶) ∈ 𝑋) |
66 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
⊢
(-g‘𝐺) = (-g‘𝐺) |
67 | 22, 41, 49, 66 | grpsubval 17465 |
. . . . . . . . . . . . . . . 16
⊢
((((invg‘𝐺)‘𝐶) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((invg‘𝐺)‘𝐶)(-g‘𝐺)𝐵) = (((invg‘𝐺)‘𝐶) +
((invg‘𝐺)‘𝐵))) |
68 | 65, 40, 67 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (((invg‘𝐺)‘𝐶)(-g‘𝐺)𝐵) = (((invg‘𝐺)‘𝐶) +
((invg‘𝐺)‘𝐵))) |
69 | 63, 68 | eqtr4d 2659 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ((invg‘𝐺)‘(𝐵 + 𝐶)) = (((invg‘𝐺)‘𝐶)(-g‘𝐺)𝐵)) |
70 | 69 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (((invg‘𝐺)‘(𝐵 + 𝐶)) + 𝐵) = ((((invg‘𝐺)‘𝐶)(-g‘𝐺)𝐵) + 𝐵)) |
71 | 22, 41, 66 | grpnpcan 17507 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Grp ∧
((invg‘𝐺)‘𝐶) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((((invg‘𝐺)‘𝐶)(-g‘𝐺)𝐵) + 𝐵) = ((invg‘𝐺)‘𝐶)) |
72 | 36, 65, 40, 71 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ((((invg‘𝐺)‘𝐶)(-g‘𝐺)𝐵) + 𝐵) = ((invg‘𝐺)‘𝐶)) |
73 | 70, 72 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (((invg‘𝐺)‘(𝐵 + 𝐶)) + 𝐵) = ((invg‘𝐺)‘𝐶)) |
74 | 73 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ((((invg‘𝐺)‘(𝐵 + 𝐶)) + 𝐵) + 𝑧) = (((invg‘𝐺)‘𝐶) + 𝑧)) |
75 | 74 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → ((((invg‘𝐺)‘(𝐵 + 𝐶)) + 𝐵) + 𝑧) = (((invg‘𝐺)‘𝐶) + 𝑧)) |
76 | 61, 75 | eqtr3d 2658 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → (((invg‘𝐺)‘(𝐵 + 𝐶)) + (𝐵 + 𝑧)) = (((invg‘𝐺)‘𝐶) + 𝑧)) |
77 | 53 | simp3d 1075 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → (((invg‘𝐺)‘𝐶) + 𝑧) ∈ 𝐾) |
78 | 76, 77 | eqeltrd 2701 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → (((invg‘𝐺)‘(𝐵 + 𝐶)) + (𝐵 + 𝑧)) ∈ 𝐾) |
79 | 22, 49, 41, 2 | eqgval 17643 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝐾 ⊆ 𝑋) → ((𝐵 + 𝐶) ∼ (𝐵 + 𝑧) ↔ ((𝐵 + 𝐶) ∈ 𝑋 ∧ (𝐵 + 𝑧) ∈ 𝑋 ∧ (((invg‘𝐺)‘(𝐵 + 𝐶)) + (𝐵 + 𝑧)) ∈ 𝐾))) |
80 | 35, 48, 79 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐵 + 𝐶) ∼ (𝐵 + 𝑧) ↔ ((𝐵 + 𝐶) ∈ 𝑋 ∧ (𝐵 + 𝑧) ∈ 𝑋 ∧ (((invg‘𝐺)‘(𝐵 + 𝐶)) + (𝐵 + 𝑧)) ∈ 𝐾))) |
81 | 80 | 3ad2ant1 1082 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ((𝐵 + 𝐶) ∼ (𝐵 + 𝑧) ↔ ((𝐵 + 𝐶) ∈ 𝑋 ∧ (𝐵 + 𝑧) ∈ 𝑋 ∧ (((invg‘𝐺)‘(𝐵 + 𝐶)) + (𝐵 + 𝑧)) ∈ 𝐾))) |
82 | 81 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → ((𝐵 + 𝐶) ∼ (𝐵 + 𝑧) ↔ ((𝐵 + 𝐶) ∈ 𝑋 ∧ (𝐵 + 𝑧) ∈ 𝑋 ∧ (((invg‘𝐺)‘(𝐵 + 𝐶)) + (𝐵 + 𝑧)) ∈ 𝐾))) |
83 | 44, 56, 78, 82 | mpbir3and 1245 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → (𝐵 + 𝐶) ∼ (𝐵 + 𝑧)) |
84 | | ovex 6678 |
. . . . . . . 8
⊢ (𝐵 + 𝑧) ∈ V |
85 | | ovex 6678 |
. . . . . . . 8
⊢ (𝐵 + 𝐶) ∈ V |
86 | 84, 85 | elec 7786 |
. . . . . . 7
⊢ ((𝐵 + 𝑧) ∈ [(𝐵 + 𝐶)] ∼ ↔ (𝐵 + 𝐶) ∼ (𝐵 + 𝑧)) |
87 | 83, 86 | sylibr 224 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → (𝐵 + 𝑧) ∈ [(𝐵 + 𝐶)] ∼ ) |
88 | 32, 87 | syldan 487 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝑧 ∈ [𝐶] ∼ ) → (𝐵 + 𝑧) ∈ [(𝐵 + 𝐶)] ∼ ) |
89 | | eqid 2622 |
. . . . 5
⊢ (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) = (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) |
90 | 88, 89 | fmptd 6385 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)):[𝐶] ∼ ⟶[(𝐵 + 𝐶)] ∼ ) |
91 | | frn 6053 |
. . . 4
⊢ ((𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)):[𝐶] ∼ ⟶[(𝐵 + 𝐶)] ∼ → ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) ⊆ [(𝐵 + 𝐶)] ∼ ) |
92 | 90, 91 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) ⊆ [(𝐵 + 𝐶)] ∼ ) |
93 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)) = (𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)) |
94 | 22, 41, 93 | grplmulf1o 17489 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)):𝑋–1-1-onto→𝑋) |
95 | 36, 40, 94 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)):𝑋–1-1-onto→𝑋) |
96 | | f1of1 6136 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)):𝑋–1-1-onto→𝑋 → (𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)):𝑋–1-1→𝑋) |
97 | 95, 96 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)):𝑋–1-1→𝑋) |
98 | 24 | ecss 7788 |
. . . . . . . . 9
⊢ (𝜑 → [𝐶] ∼ ⊆ 𝑋) |
99 | 98 | 3ad2ant1 1082 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → [𝐶] ∼ ⊆ 𝑋) |
100 | | f1ssres 6108 |
. . . . . . . 8
⊢ (((𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)):𝑋–1-1→𝑋 ∧ [𝐶] ∼ ⊆ 𝑋) → ((𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)) ↾ [𝐶] ∼ ):[𝐶] ∼ –1-1→𝑋) |
101 | 97, 99, 100 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ((𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)) ↾ [𝐶] ∼ ):[𝐶] ∼ –1-1→𝑋) |
102 | | resmpt 5449 |
. . . . . . . 8
⊢ ([𝐶] ∼ ⊆ 𝑋 → ((𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)) ↾ [𝐶] ∼ ) = (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧))) |
103 | | f1eq1 6096 |
. . . . . . . 8
⊢ (((𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)) ↾ [𝐶] ∼ ) = (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) → (((𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)) ↾ [𝐶] ∼ ):[𝐶] ∼ –1-1→𝑋 ↔ (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)):[𝐶] ∼ –1-1→𝑋)) |
104 | 99, 102, 103 | 3syl 18 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (((𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)) ↾ [𝐶] ∼ ):[𝐶] ∼ –1-1→𝑋 ↔ (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)):[𝐶] ∼ –1-1→𝑋)) |
105 | 101, 104 | mpbid 222 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)):[𝐶] ∼ –1-1→𝑋) |
106 | | f1f1orn 6148 |
. . . . . 6
⊢ ((𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)):[𝐶] ∼ –1-1→𝑋 → (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)):[𝐶] ∼ –1-1-onto→ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧))) |
107 | 105, 106 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)):[𝐶] ∼ –1-1-onto→ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧))) |
108 | 15 | f1oen 7976 |
. . . . 5
⊢ ((𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)):[𝐶] ∼ –1-1-onto→ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) → [𝐶] ∼ ≈ ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧))) |
109 | | ensym 8005 |
. . . . 5
⊢ ([𝐶] ∼ ≈ ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) → ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) ≈ [𝐶] ∼ ) |
110 | 107, 108,
109 | 3syl 18 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) ≈ [𝐶] ∼ ) |
111 | 21 | 3ad2ant1 1082 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → 𝐾 ∈ (SubGrp‘𝐺)) |
112 | 22, 2 | eqgen 17647 |
. . . . . . 7
⊢ ((𝐾 ∈ (SubGrp‘𝐺) ∧ [𝐶] ∼ ∈ (𝑋 / ∼ )) → 𝐾 ≈ [𝐶] ∼ ) |
113 | 111, 7, 112 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → 𝐾 ≈ [𝐶] ∼ ) |
114 | | ensym 8005 |
. . . . . 6
⊢ (𝐾 ≈ [𝐶] ∼ → [𝐶] ∼ ≈ 𝐾) |
115 | 113, 114 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → [𝐶] ∼ ≈ 𝐾) |
116 | | ecelqsg 7802 |
. . . . . . 7
⊢ (( ∼ ∈
V ∧ (𝐵 + 𝐶) ∈ 𝑋) → [(𝐵 + 𝐶)] ∼ ∈ (𝑋 / ∼ )) |
117 | 4, 43, 116 | sylancr 695 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → [(𝐵 + 𝐶)] ∼ ∈ (𝑋 / ∼ )) |
118 | 22, 2 | eqgen 17647 |
. . . . . 6
⊢ ((𝐾 ∈ (SubGrp‘𝐺) ∧ [(𝐵 + 𝐶)] ∼ ∈ (𝑋 / ∼ )) → 𝐾 ≈ [(𝐵 + 𝐶)] ∼ ) |
119 | 111, 117,
118 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → 𝐾 ≈ [(𝐵 + 𝐶)] ∼ ) |
120 | | entr 8008 |
. . . . 5
⊢ (([𝐶] ∼ ≈ 𝐾 ∧ 𝐾 ≈ [(𝐵 + 𝐶)] ∼ ) → [𝐶] ∼ ≈ [(𝐵 + 𝐶)] ∼ ) |
121 | 115, 119,
120 | syl2anc 693 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → [𝐶] ∼ ≈ [(𝐵 + 𝐶)] ∼ ) |
122 | | entr 8008 |
. . . 4
⊢ ((ran
(𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) ≈ [𝐶] ∼ ∧ [𝐶] ∼ ≈ [(𝐵 + 𝐶)] ∼ ) → ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) ≈ [(𝐵 + 𝐶)] ∼ ) |
123 | 110, 121,
122 | syl2anc 693 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) ≈ [(𝐵 + 𝐶)] ∼ ) |
124 | | fisseneq 8171 |
. . 3
⊢ (([(𝐵 + 𝐶)] ∼ ∈ Fin ∧
ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) ⊆ [(𝐵 + 𝐶)] ∼ ∧ ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) ≈ [(𝐵 + 𝐶)] ∼ ) → ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) = [(𝐵 + 𝐶)] ∼ ) |
125 | 28, 92, 123, 124 | syl3anc 1326 |
. 2
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) = [(𝐵 + 𝐶)] ∼ ) |
126 | 19, 125 | eqtrd 2656 |
1
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝐵 · [𝐶] ∼ ) = [(𝐵 + 𝐶)] ∼ ) |