Proof of Theorem sylow2blem1
| Step | Hyp | Ref
| Expression |
| 1 | | simp2 1138 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → 𝐵 ∈ 𝐻) |
| 2 | | sylow2b.r |
. . . . 5
⊢ ∼ =
(𝐺 ~QG
𝐾) |
| 3 | 2 | ovexi 7465 |
. . . 4
⊢ ∼ ∈
V |
| 4 | | simp3 1139 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → 𝐶 ∈ 𝑋) |
| 5 | | ecelqsg 8812 |
. . . 4
⊢ (( ∼ ∈
V ∧ 𝐶 ∈ 𝑋) → [𝐶] ∼ ∈ (𝑋 / ∼ )) |
| 6 | 3, 4, 5 | sylancr 587 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → [𝐶] ∼ ∈ (𝑋 / ∼ )) |
| 7 | | simpr 484 |
. . . . . 6
⊢ ((𝑥 = 𝐵 ∧ 𝑦 = [𝐶] ∼ ) → 𝑦 = [𝐶] ∼ ) |
| 8 | | simpl 482 |
. . . . . . 7
⊢ ((𝑥 = 𝐵 ∧ 𝑦 = [𝐶] ∼ ) → 𝑥 = 𝐵) |
| 9 | 8 | oveq1d 7446 |
. . . . . 6
⊢ ((𝑥 = 𝐵 ∧ 𝑦 = [𝐶] ∼ ) → (𝑥 + 𝑧) = (𝐵 + 𝑧)) |
| 10 | 7, 9 | mpteq12dv 5233 |
. . . . 5
⊢ ((𝑥 = 𝐵 ∧ 𝑦 = [𝐶] ∼ ) → (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) = (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧))) |
| 11 | 10 | rneqd 5949 |
. . . 4
⊢ ((𝑥 = 𝐵 ∧ 𝑦 = [𝐶] ∼ ) → ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧))) |
| 12 | | sylow2b.m |
. . . 4
⊢ · =
(𝑥 ∈ 𝐻, 𝑦 ∈ (𝑋 / ∼ ) ↦ ran
(𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) |
| 13 | | ecexg 8749 |
. . . . . . 7
⊢ ( ∼ ∈
V → [𝐶] ∼ ∈
V) |
| 14 | 3, 13 | ax-mp 5 |
. . . . . 6
⊢ [𝐶] ∼ ∈
V |
| 15 | 14 | mptex 7243 |
. . . . 5
⊢ (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) ∈ V |
| 16 | 15 | rnex 7932 |
. . . 4
⊢ ran
(𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) ∈ V |
| 17 | 11, 12, 16 | ovmpoa 7588 |
. . 3
⊢ ((𝐵 ∈ 𝐻 ∧ [𝐶] ∼ ∈ (𝑋 / ∼ )) → (𝐵 · [𝐶] ∼ ) = ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧))) |
| 18 | 1, 6, 17 | syl2anc 584 |
. 2
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝐵 · [𝐶] ∼ ) = ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧))) |
| 19 | | sylow2b.xf |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ Fin) |
| 20 | | sylow2b.k |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺)) |
| 21 | | sylow2b.x |
. . . . . . . 8
⊢ 𝑋 = (Base‘𝐺) |
| 22 | 21, 2 | eqger 19196 |
. . . . . . 7
⊢ (𝐾 ∈ (SubGrp‘𝐺) → ∼ Er 𝑋) |
| 23 | 20, 22 | syl 17 |
. . . . . 6
⊢ (𝜑 → ∼ Er 𝑋) |
| 24 | 23 | ecss 8793 |
. . . . 5
⊢ (𝜑 → [(𝐵 + 𝐶)] ∼ ⊆ 𝑋) |
| 25 | 19, 24 | ssfid 9301 |
. . . 4
⊢ (𝜑 → [(𝐵 + 𝐶)] ∼ ∈
Fin) |
| 26 | 25 | 3ad2ant1 1134 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → [(𝐵 + 𝐶)] ∼ ∈
Fin) |
| 27 | | vex 3484 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
| 28 | | elecg 8789 |
. . . . . . . 8
⊢ ((𝑧 ∈ V ∧ 𝐶 ∈ 𝑋) → (𝑧 ∈ [𝐶] ∼ ↔ 𝐶 ∼ 𝑧)) |
| 29 | 27, 4, 28 | sylancr 587 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝑧 ∈ [𝐶] ∼ ↔ 𝐶 ∼ 𝑧)) |
| 30 | 29 | biimpa 476 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝑧 ∈ [𝐶] ∼ ) → 𝐶 ∼ 𝑧) |
| 31 | | sylow2b.h |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐻 ∈ (SubGrp‘𝐺)) |
| 32 | | subgrcl 19149 |
. . . . . . . . . . . 12
⊢ (𝐻 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp) |
| 33 | 31, 32 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ Grp) |
| 34 | 33 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → 𝐺 ∈ Grp) |
| 35 | 21 | subgss 19145 |
. . . . . . . . . . . . 13
⊢ (𝐻 ∈ (SubGrp‘𝐺) → 𝐻 ⊆ 𝑋) |
| 36 | 31, 35 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐻 ⊆ 𝑋) |
| 37 | 36 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → 𝐻 ⊆ 𝑋) |
| 38 | 37, 1 | sseldd 3984 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → 𝐵 ∈ 𝑋) |
| 39 | | sylow2b.a |
. . . . . . . . . . 11
⊢ + =
(+g‘𝐺) |
| 40 | 21, 39 | grpcl 18959 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐵 + 𝐶) ∈ 𝑋) |
| 41 | 34, 38, 4, 40 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝐵 + 𝐶) ∈ 𝑋) |
| 42 | 41 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → (𝐵 + 𝐶) ∈ 𝑋) |
| 43 | 34 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → 𝐺 ∈ Grp) |
| 44 | 38 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → 𝐵 ∈ 𝑋) |
| 45 | 21 | subgss 19145 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ (SubGrp‘𝐺) → 𝐾 ⊆ 𝑋) |
| 46 | 20, 45 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ⊆ 𝑋) |
| 47 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(invg‘𝐺) = (invg‘𝐺) |
| 48 | 21, 47, 39, 2 | eqgval 19195 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Grp ∧ 𝐾 ⊆ 𝑋) → (𝐶 ∼ 𝑧 ↔ (𝐶 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐶) + 𝑧) ∈ 𝐾))) |
| 49 | 33, 46, 48 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶 ∼ 𝑧 ↔ (𝐶 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐶) + 𝑧) ∈ 𝐾))) |
| 50 | 49 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝐶 ∼ 𝑧 ↔ (𝐶 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐶) + 𝑧) ∈ 𝐾))) |
| 51 | 50 | biimpa 476 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → (𝐶 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ (((invg‘𝐺)‘𝐶) + 𝑧) ∈ 𝐾)) |
| 52 | 51 | simp2d 1144 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → 𝑧 ∈ 𝑋) |
| 53 | 21, 39 | grpcl 18959 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → (𝐵 + 𝑧) ∈ 𝑋) |
| 54 | 43, 44, 52, 53 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → (𝐵 + 𝑧) ∈ 𝑋) |
| 55 | 21, 47 | grpinvcl 19005 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Grp ∧ (𝐵 + 𝐶) ∈ 𝑋) → ((invg‘𝐺)‘(𝐵 + 𝐶)) ∈ 𝑋) |
| 56 | 34, 41, 55 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ((invg‘𝐺)‘(𝐵 + 𝐶)) ∈ 𝑋) |
| 57 | 56 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → ((invg‘𝐺)‘(𝐵 + 𝐶)) ∈ 𝑋) |
| 58 | 21, 39 | grpass 18960 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧
(((invg‘𝐺)‘(𝐵 + 𝐶)) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → ((((invg‘𝐺)‘(𝐵 + 𝐶)) + 𝐵) + 𝑧) = (((invg‘𝐺)‘(𝐵 + 𝐶)) + (𝐵 + 𝑧))) |
| 59 | 43, 57, 44, 52, 58 | syl13anc 1374 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → ((((invg‘𝐺)‘(𝐵 + 𝐶)) + 𝐵) + 𝑧) = (((invg‘𝐺)‘(𝐵 + 𝐶)) + (𝐵 + 𝑧))) |
| 60 | 21, 39, 47 | grpinvadd 19036 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((invg‘𝐺)‘(𝐵 + 𝐶)) = (((invg‘𝐺)‘𝐶) +
((invg‘𝐺)‘𝐵))) |
| 61 | 34, 38, 4, 60 | syl3anc 1373 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ((invg‘𝐺)‘(𝐵 + 𝐶)) = (((invg‘𝐺)‘𝐶) +
((invg‘𝐺)‘𝐵))) |
| 62 | 21, 47 | grpinvcl 19005 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 ∈ Grp ∧ 𝐶 ∈ 𝑋) → ((invg‘𝐺)‘𝐶) ∈ 𝑋) |
| 63 | 34, 4, 62 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ((invg‘𝐺)‘𝐶) ∈ 𝑋) |
| 64 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢
(-g‘𝐺) = (-g‘𝐺) |
| 65 | 21, 39, 47, 64 | grpsubval 19003 |
. . . . . . . . . . . . . . . 16
⊢
((((invg‘𝐺)‘𝐶) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((invg‘𝐺)‘𝐶)(-g‘𝐺)𝐵) = (((invg‘𝐺)‘𝐶) +
((invg‘𝐺)‘𝐵))) |
| 66 | 63, 38, 65 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (((invg‘𝐺)‘𝐶)(-g‘𝐺)𝐵) = (((invg‘𝐺)‘𝐶) +
((invg‘𝐺)‘𝐵))) |
| 67 | 61, 66 | eqtr4d 2780 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ((invg‘𝐺)‘(𝐵 + 𝐶)) = (((invg‘𝐺)‘𝐶)(-g‘𝐺)𝐵)) |
| 68 | 67 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (((invg‘𝐺)‘(𝐵 + 𝐶)) + 𝐵) = ((((invg‘𝐺)‘𝐶)(-g‘𝐺)𝐵) + 𝐵)) |
| 69 | 21, 39, 64 | grpnpcan 19050 |
. . . . . . . . . . . . . 14
⊢ ((𝐺 ∈ Grp ∧
((invg‘𝐺)‘𝐶) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((((invg‘𝐺)‘𝐶)(-g‘𝐺)𝐵) + 𝐵) = ((invg‘𝐺)‘𝐶)) |
| 70 | 34, 63, 38, 69 | syl3anc 1373 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ((((invg‘𝐺)‘𝐶)(-g‘𝐺)𝐵) + 𝐵) = ((invg‘𝐺)‘𝐶)) |
| 71 | 68, 70 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (((invg‘𝐺)‘(𝐵 + 𝐶)) + 𝐵) = ((invg‘𝐺)‘𝐶)) |
| 72 | 71 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ((((invg‘𝐺)‘(𝐵 + 𝐶)) + 𝐵) + 𝑧) = (((invg‘𝐺)‘𝐶) + 𝑧)) |
| 73 | 72 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → ((((invg‘𝐺)‘(𝐵 + 𝐶)) + 𝐵) + 𝑧) = (((invg‘𝐺)‘𝐶) + 𝑧)) |
| 74 | 59, 73 | eqtr3d 2779 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → (((invg‘𝐺)‘(𝐵 + 𝐶)) + (𝐵 + 𝑧)) = (((invg‘𝐺)‘𝐶) + 𝑧)) |
| 75 | 51 | simp3d 1145 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → (((invg‘𝐺)‘𝐶) + 𝑧) ∈ 𝐾) |
| 76 | 74, 75 | eqeltrd 2841 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → (((invg‘𝐺)‘(𝐵 + 𝐶)) + (𝐵 + 𝑧)) ∈ 𝐾) |
| 77 | 21, 47, 39, 2 | eqgval 19195 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝐾 ⊆ 𝑋) → ((𝐵 + 𝐶) ∼ (𝐵 + 𝑧) ↔ ((𝐵 + 𝐶) ∈ 𝑋 ∧ (𝐵 + 𝑧) ∈ 𝑋 ∧ (((invg‘𝐺)‘(𝐵 + 𝐶)) + (𝐵 + 𝑧)) ∈ 𝐾))) |
| 78 | 33, 46, 77 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐵 + 𝐶) ∼ (𝐵 + 𝑧) ↔ ((𝐵 + 𝐶) ∈ 𝑋 ∧ (𝐵 + 𝑧) ∈ 𝑋 ∧ (((invg‘𝐺)‘(𝐵 + 𝐶)) + (𝐵 + 𝑧)) ∈ 𝐾))) |
| 79 | 78 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ((𝐵 + 𝐶) ∼ (𝐵 + 𝑧) ↔ ((𝐵 + 𝐶) ∈ 𝑋 ∧ (𝐵 + 𝑧) ∈ 𝑋 ∧ (((invg‘𝐺)‘(𝐵 + 𝐶)) + (𝐵 + 𝑧)) ∈ 𝐾))) |
| 80 | 79 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → ((𝐵 + 𝐶) ∼ (𝐵 + 𝑧) ↔ ((𝐵 + 𝐶) ∈ 𝑋 ∧ (𝐵 + 𝑧) ∈ 𝑋 ∧ (((invg‘𝐺)‘(𝐵 + 𝐶)) + (𝐵 + 𝑧)) ∈ 𝐾))) |
| 81 | 42, 54, 76, 80 | mpbir3and 1343 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → (𝐵 + 𝐶) ∼ (𝐵 + 𝑧)) |
| 82 | | ovex 7464 |
. . . . . . . 8
⊢ (𝐵 + 𝑧) ∈ V |
| 83 | | ovex 7464 |
. . . . . . . 8
⊢ (𝐵 + 𝐶) ∈ V |
| 84 | 82, 83 | elec 8791 |
. . . . . . 7
⊢ ((𝐵 + 𝑧) ∈ [(𝐵 + 𝐶)] ∼ ↔ (𝐵 + 𝐶) ∼ (𝐵 + 𝑧)) |
| 85 | 81, 84 | sylibr 234 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝐶 ∼ 𝑧) → (𝐵 + 𝑧) ∈ [(𝐵 + 𝐶)] ∼ ) |
| 86 | 30, 85 | syldan 591 |
. . . . 5
⊢ (((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) ∧ 𝑧 ∈ [𝐶] ∼ ) → (𝐵 + 𝑧) ∈ [(𝐵 + 𝐶)] ∼ ) |
| 87 | 86 | fmpttd 7135 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)):[𝐶] ∼ ⟶[(𝐵 + 𝐶)] ∼ ) |
| 88 | 87 | frnd 6744 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) ⊆ [(𝐵 + 𝐶)] ∼ ) |
| 89 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)) = (𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)) |
| 90 | 21, 39, 89 | grplmulf1o 19031 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)):𝑋–1-1-onto→𝑋) |
| 91 | 34, 38, 90 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)):𝑋–1-1-onto→𝑋) |
| 92 | | f1of1 6847 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)):𝑋–1-1-onto→𝑋 → (𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)):𝑋–1-1→𝑋) |
| 93 | 91, 92 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)):𝑋–1-1→𝑋) |
| 94 | 23 | ecss 8793 |
. . . . . . . . 9
⊢ (𝜑 → [𝐶] ∼ ⊆ 𝑋) |
| 95 | 94 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → [𝐶] ∼ ⊆ 𝑋) |
| 96 | | f1ssres 6811 |
. . . . . . . 8
⊢ (((𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)):𝑋–1-1→𝑋 ∧ [𝐶] ∼ ⊆ 𝑋) → ((𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)) ↾ [𝐶] ∼ ):[𝐶] ∼ –1-1→𝑋) |
| 97 | 93, 95, 96 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ((𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)) ↾ [𝐶] ∼ ):[𝐶] ∼ –1-1→𝑋) |
| 98 | | resmpt 6055 |
. . . . . . . 8
⊢ ([𝐶] ∼ ⊆ 𝑋 → ((𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)) ↾ [𝐶] ∼ ) = (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧))) |
| 99 | | f1eq1 6799 |
. . . . . . . 8
⊢ (((𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)) ↾ [𝐶] ∼ ) = (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) → (((𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)) ↾ [𝐶] ∼ ):[𝐶] ∼ –1-1→𝑋 ↔ (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)):[𝐶] ∼ –1-1→𝑋)) |
| 100 | 95, 98, 99 | 3syl 18 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (((𝑧 ∈ 𝑋 ↦ (𝐵 + 𝑧)) ↾ [𝐶] ∼ ):[𝐶] ∼ –1-1→𝑋 ↔ (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)):[𝐶] ∼ –1-1→𝑋)) |
| 101 | 97, 100 | mpbid 232 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)):[𝐶] ∼ –1-1→𝑋) |
| 102 | | f1f1orn 6859 |
. . . . . 6
⊢ ((𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)):[𝐶] ∼ –1-1→𝑋 → (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)):[𝐶] ∼ –1-1-onto→ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧))) |
| 103 | 101, 102 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)):[𝐶] ∼ –1-1-onto→ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧))) |
| 104 | 14 | f1oen 9013 |
. . . . 5
⊢ ((𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)):[𝐶] ∼ –1-1-onto→ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) → [𝐶] ∼ ≈ ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧))) |
| 105 | | ensym 9043 |
. . . . 5
⊢ ([𝐶] ∼ ≈ ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) → ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) ≈ [𝐶] ∼ ) |
| 106 | 103, 104,
105 | 3syl 18 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) ≈ [𝐶] ∼ ) |
| 107 | 20 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → 𝐾 ∈ (SubGrp‘𝐺)) |
| 108 | 21, 2 | eqgen 19199 |
. . . . . . 7
⊢ ((𝐾 ∈ (SubGrp‘𝐺) ∧ [𝐶] ∼ ∈ (𝑋 / ∼ )) → 𝐾 ≈ [𝐶] ∼ ) |
| 109 | 107, 6, 108 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → 𝐾 ≈ [𝐶] ∼ ) |
| 110 | | ensym 9043 |
. . . . . 6
⊢ (𝐾 ≈ [𝐶] ∼ → [𝐶] ∼ ≈ 𝐾) |
| 111 | 109, 110 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → [𝐶] ∼ ≈ 𝐾) |
| 112 | | ecelqsg 8812 |
. . . . . . 7
⊢ (( ∼ ∈
V ∧ (𝐵 + 𝐶) ∈ 𝑋) → [(𝐵 + 𝐶)] ∼ ∈ (𝑋 / ∼ )) |
| 113 | 3, 41, 112 | sylancr 587 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → [(𝐵 + 𝐶)] ∼ ∈ (𝑋 / ∼ )) |
| 114 | 21, 2 | eqgen 19199 |
. . . . . 6
⊢ ((𝐾 ∈ (SubGrp‘𝐺) ∧ [(𝐵 + 𝐶)] ∼ ∈ (𝑋 / ∼ )) → 𝐾 ≈ [(𝐵 + 𝐶)] ∼ ) |
| 115 | 107, 113,
114 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → 𝐾 ≈ [(𝐵 + 𝐶)] ∼ ) |
| 116 | | entr 9046 |
. . . . 5
⊢ (([𝐶] ∼ ≈ 𝐾 ∧ 𝐾 ≈ [(𝐵 + 𝐶)] ∼ ) → [𝐶] ∼ ≈ [(𝐵 + 𝐶)] ∼ ) |
| 117 | 111, 115,
116 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → [𝐶] ∼ ≈ [(𝐵 + 𝐶)] ∼ ) |
| 118 | | entr 9046 |
. . . 4
⊢ ((ran
(𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) ≈ [𝐶] ∼ ∧ [𝐶] ∼ ≈ [(𝐵 + 𝐶)] ∼ ) → ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) ≈ [(𝐵 + 𝐶)] ∼ ) |
| 119 | 106, 117,
118 | syl2anc 584 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) ≈ [(𝐵 + 𝐶)] ∼ ) |
| 120 | | fisseneq 9293 |
. . 3
⊢ (([(𝐵 + 𝐶)] ∼ ∈ Fin ∧
ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) ⊆ [(𝐵 + 𝐶)] ∼ ∧ ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) ≈ [(𝐵 + 𝐶)] ∼ ) → ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) = [(𝐵 + 𝐶)] ∼ ) |
| 121 | 26, 88, 119, 120 | syl3anc 1373 |
. 2
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → ran (𝑧 ∈ [𝐶] ∼ ↦ (𝐵 + 𝑧)) = [(𝐵 + 𝐶)] ∼ ) |
| 122 | 18, 121 | eqtrd 2777 |
1
⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝐵 · [𝐶] ∼ ) = [(𝐵 + 𝐶)] ∼ ) |