Metamath Proof Explorer

Theorem sylow2blem1

Description: Lemma for sylow2b . Evaluate the group action on a left coset. (Contributed by Mario Carneiro, 17-Jan-2015)

Ref Expression
Hypotheses sylow2b.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
sylow2b.xf ⊢ ( 𝜑 → 𝑋 ∈ Fin )
sylow2b.h ⊢ ( 𝜑 → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) )
sylow2b.k ⊢ ( 𝜑 → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) )
sylow2b.a ⊢ + = ( +g ‘ 𝐺 )
sylow2b.r ⊢ ∼ = ( 𝐺 ~QG 𝐾 )
sylow2b.m ⊢ · = ( 𝑥 ∈ 𝐻 , 𝑦 ∈ ( 𝑋 / ∼ ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) )
Assertion sylow2blem1 ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 · [ 𝐶 ] ∼ ) = [ ( 𝐵 + 𝐶 ) ] ∼ )

Proof

Step Hyp Ref Expression
1 sylow2b.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 sylow2b.xf ⊢ ( 𝜑 → 𝑋 ∈ Fin )
3 sylow2b.h ⊢ ( 𝜑 → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) )
4 sylow2b.k ⊢ ( 𝜑 → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) )
5 sylow2b.a ⊢ + = ( +g ‘ 𝐺 )
6 sylow2b.r ⊢ ∼ = ( 𝐺 ~QG 𝐾 )
7 sylow2b.m ⊢ · = ( 𝑥 ∈ 𝐻 , 𝑦 ∈ ( 𝑋 / ∼ ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) )
8 simp2 ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → 𝐵 ∈ 𝐻 )
9 6 ovexi ⊢ ∼ ∈ V
10 simp3 ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → 𝐶 ∈ 𝑋 )
11 ecelqsg ⊢ ( ( ∼ ∈ V ∧ 𝐶 ∈ 𝑋 ) → [ 𝐶 ] ∼ ∈ ( 𝑋 / ∼ ) )
12 9 10 11 sylancr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → [ 𝐶 ] ∼ ∈ ( 𝑋 / ∼ ) )
13 simpr ⊢ ( ( 𝑥 = 𝐵 ∧ 𝑦 = [ 𝐶 ] ∼ ) → 𝑦 = [ 𝐶 ] ∼ )
14 simpl ⊢ ( ( 𝑥 = 𝐵 ∧ 𝑦 = [ 𝐶 ] ∼ ) → 𝑥 = 𝐵 )
15 14 oveq1d ⊢ ( ( 𝑥 = 𝐵 ∧ 𝑦 = [ 𝐶 ] ∼ ) → ( 𝑥 + 𝑧 ) = ( 𝐵 + 𝑧 ) )
16 13 15 mpteq12dv ⊢ ( ( 𝑥 = 𝐵 ∧ 𝑦 = [ 𝐶 ] ∼ ) → ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) = ( 𝑧 ∈ [ 𝐶 ] ∼ ↦ ( 𝐵 + 𝑧 ) ) )
17 16 rneqd ⊢ ( ( 𝑥 = 𝐵 ∧ 𝑦 = [ 𝐶 ] ∼ ) → ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) = ran ( 𝑧 ∈ [ 𝐶 ] ∼ ↦ ( 𝐵 + 𝑧 ) ) )
18 ecexg ⊢ ( ∼ ∈ V → [ 𝐶 ] ∼ ∈ V )
19 9 18 ax-mp ⊢ [ 𝐶 ] ∼ ∈ V
20 19 mptex ⊢ ( 𝑧 ∈ [ 𝐶 ] ∼ ↦ ( 𝐵 + 𝑧 ) ) ∈ V
21 20 rnex ⊢ ran ( 𝑧 ∈ [ 𝐶 ] ∼ ↦ ( 𝐵 + 𝑧 ) ) ∈ V
22 17 7 21 ovmpoa ⊢ ( ( 𝐵 ∈ 𝐻 ∧ [ 𝐶 ] ∼ ∈ ( 𝑋 / ∼ ) ) → ( 𝐵 · [ 𝐶 ] ∼ ) = ran ( 𝑧 ∈ [ 𝐶 ] ∼ ↦ ( 𝐵 + 𝑧 ) ) )
23 8 12 22 syl2anc ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 · [ 𝐶 ] ∼ ) = ran ( 𝑧 ∈ [ 𝐶 ] ∼ ↦ ( 𝐵 + 𝑧 ) ) )
24 1 6 eqger ⊢ ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) → ∼ Er 𝑋 )
25 4 24 syl ⊢ ( 𝜑 → ∼ Er 𝑋 )
26 25 ecss ⊢ ( 𝜑 → [ ( 𝐵 + 𝐶 ) ] ∼ ⊆ 𝑋 )
27 2 26 ssfid ⊢ ( 𝜑 → [ ( 𝐵 + 𝐶 ) ] ∼ ∈ Fin )
28 27 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → [ ( 𝐵 + 𝐶 ) ] ∼ ∈ Fin )
29 vex ⊢ 𝑧 ∈ V
30 elecg ⊢ ( ( 𝑧 ∈ V ∧ 𝐶 ∈ 𝑋 ) → ( 𝑧 ∈ [ 𝐶 ] ∼ ↔ 𝐶 ∼ 𝑧 ) )
31 29 10 30 sylancr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → ( 𝑧 ∈ [ 𝐶 ] ∼ ↔ 𝐶 ∼ 𝑧 ) )
32 31 biimpa ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝑧 ∈ [ 𝐶 ] ∼ ) → 𝐶 ∼ 𝑧 )
33 subgrcl ⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
34 3 33 syl ⊢ ( 𝜑 → 𝐺 ∈ Grp )
35 34 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → 𝐺 ∈ Grp )
36 1 subgss ⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → 𝐻 ⊆ 𝑋 )
37 3 36 syl ⊢ ( 𝜑 → 𝐻 ⊆ 𝑋 )
38 37 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → 𝐻 ⊆ 𝑋 )
39 38 8 sseldd ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → 𝐵 ∈ 𝑋 )
40 1 5 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 + 𝐶 ) ∈ 𝑋 )
41 35 39 10 40 syl3anc ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 + 𝐶 ) ∈ 𝑋 )
42 41 adantr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝐶 ∼ 𝑧 ) → ( 𝐵 + 𝐶 ) ∈ 𝑋 )
43 35 adantr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝐶 ∼ 𝑧 ) → 𝐺 ∈ Grp )
44 39 adantr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝐶 ∼ 𝑧 ) → 𝐵 ∈ 𝑋 )
45 1 subgss ⊢ ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) → 𝐾 ⊆ 𝑋 )
46 4 45 syl ⊢ ( 𝜑 → 𝐾 ⊆ 𝑋 )
47 eqid ⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
48 1 47 5 6 eqgval ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐾 ⊆ 𝑋 ) → ( 𝐶 ∼ 𝑧 ↔ ( 𝐶 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) + 𝑧 ) ∈ 𝐾 ) ) )
49 34 46 48 syl2anc ⊢ ( 𝜑 → ( 𝐶 ∼ 𝑧 ↔ ( 𝐶 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) + 𝑧 ) ∈ 𝐾 ) ) )
50 49 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐶 ∼ 𝑧 ↔ ( 𝐶 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) + 𝑧 ) ∈ 𝐾 ) ) )
51 50 biimpa ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝐶 ∼ 𝑧 ) → ( 𝐶 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) + 𝑧 ) ∈ 𝐾 ) )
52 51 simp2d ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝐶 ∼ 𝑧 ) → 𝑧 ∈ 𝑋 )
53 1 5 grpcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( 𝐵 + 𝑧 ) ∈ 𝑋 )
54 43 44 52 53 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝐶 ∼ 𝑧 ) → ( 𝐵 + 𝑧 ) ∈ 𝑋 )
55 1 47 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝐵 + 𝐶 ) ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ ( 𝐵 + 𝐶 ) ) ∈ 𝑋 )
56 35 41 55 syl2anc ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ ( 𝐵 + 𝐶 ) ) ∈ 𝑋 )
57 56 adantr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝐶 ∼ 𝑧 ) → ( ( invg ‘ 𝐺 ) ‘ ( 𝐵 + 𝐶 ) ) ∈ 𝑋 )
58 1 5 grpass ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( ( invg ‘ 𝐺 ) ‘ ( 𝐵 + 𝐶 ) ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( ( ( invg ‘ 𝐺 ) ‘ ( 𝐵 + 𝐶 ) ) + 𝐵 ) + 𝑧 ) = ( ( ( invg ‘ 𝐺 ) ‘ ( 𝐵 + 𝐶 ) ) + ( 𝐵 + 𝑧 ) ) )
59 43 57 44 52 58 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝐶 ∼ 𝑧 ) → ( ( ( ( invg ‘ 𝐺 ) ‘ ( 𝐵 + 𝐶 ) ) + 𝐵 ) + 𝑧 ) = ( ( ( invg ‘ 𝐺 ) ‘ ( 𝐵 + 𝐶 ) ) + ( 𝐵 + 𝑧 ) ) )
60 1 5 47 grpinvadd ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ ( 𝐵 + 𝐶 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) + ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ) )
61 35 39 10 60 syl3anc ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ ( 𝐵 + 𝐶 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) + ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ) )
62 1 47 grpinvcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐶 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) ∈ 𝑋 )
63 35 10 62 syl2anc ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) ∈ 𝑋 )
64 eqid ⊢ ( -g ‘ 𝐺 ) = ( -g ‘ 𝐺 )
65 1 5 47 64 grpsubval ⊢ ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) ( -g ‘ 𝐺 ) 𝐵 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) + ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ) )
66 63 39 65 syl2anc ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) ( -g ‘ 𝐺 ) 𝐵 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) + ( ( invg ‘ 𝐺 ) ‘ 𝐵 ) ) )
67 61 66 eqtr4d ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → ( ( invg ‘ 𝐺 ) ‘ ( 𝐵 + 𝐶 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) ( -g ‘ 𝐺 ) 𝐵 ) )
68 67 oveq1d ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ ( 𝐵 + 𝐶 ) ) + 𝐵 ) = ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) ( -g ‘ 𝐺 ) 𝐵 ) + 𝐵 ) )
69 1 5 64 grpnpcan ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) ( -g ‘ 𝐺 ) 𝐵 ) + 𝐵 ) = ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) )
70 35 63 39 69 syl3anc ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → ( ( ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) ( -g ‘ 𝐺 ) 𝐵 ) + 𝐵 ) = ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) )
71 68 70 eqtrd ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → ( ( ( invg ‘ 𝐺 ) ‘ ( 𝐵 + 𝐶 ) ) + 𝐵 ) = ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) )
72 71 oveq1d ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → ( ( ( ( invg ‘ 𝐺 ) ‘ ( 𝐵 + 𝐶 ) ) + 𝐵 ) + 𝑧 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) + 𝑧 ) )
73 72 adantr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝐶 ∼ 𝑧 ) → ( ( ( ( invg ‘ 𝐺 ) ‘ ( 𝐵 + 𝐶 ) ) + 𝐵 ) + 𝑧 ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) + 𝑧 ) )
74 59 73 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝐶 ∼ 𝑧 ) → ( ( ( invg ‘ 𝐺 ) ‘ ( 𝐵 + 𝐶 ) ) + ( 𝐵 + 𝑧 ) ) = ( ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) + 𝑧 ) )
75 51 simp3d ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝐶 ∼ 𝑧 ) → ( ( ( invg ‘ 𝐺 ) ‘ 𝐶 ) + 𝑧 ) ∈ 𝐾 )
76 74 75 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝐶 ∼ 𝑧 ) → ( ( ( invg ‘ 𝐺 ) ‘ ( 𝐵 + 𝐶 ) ) + ( 𝐵 + 𝑧 ) ) ∈ 𝐾 )
77 1 47 5 6 eqgval ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐾 ⊆ 𝑋 ) → ( ( 𝐵 + 𝐶 ) ∼ ( 𝐵 + 𝑧 ) ↔ ( ( 𝐵 + 𝐶 ) ∈ 𝑋 ∧ ( 𝐵 + 𝑧 ) ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ ( 𝐵 + 𝐶 ) ) + ( 𝐵 + 𝑧 ) ) ∈ 𝐾 ) ) )
78 34 46 77 syl2anc ⊢ ( 𝜑 → ( ( 𝐵 + 𝐶 ) ∼ ( 𝐵 + 𝑧 ) ↔ ( ( 𝐵 + 𝐶 ) ∈ 𝑋 ∧ ( 𝐵 + 𝑧 ) ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ ( 𝐵 + 𝐶 ) ) + ( 𝐵 + 𝑧 ) ) ∈ 𝐾 ) ) )
79 78 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐵 + 𝐶 ) ∼ ( 𝐵 + 𝑧 ) ↔ ( ( 𝐵 + 𝐶 ) ∈ 𝑋 ∧ ( 𝐵 + 𝑧 ) ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ ( 𝐵 + 𝐶 ) ) + ( 𝐵 + 𝑧 ) ) ∈ 𝐾 ) ) )
80 79 adantr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝐶 ∼ 𝑧 ) → ( ( 𝐵 + 𝐶 ) ∼ ( 𝐵 + 𝑧 ) ↔ ( ( 𝐵 + 𝐶 ) ∈ 𝑋 ∧ ( 𝐵 + 𝑧 ) ∈ 𝑋 ∧ ( ( ( invg ‘ 𝐺 ) ‘ ( 𝐵 + 𝐶 ) ) + ( 𝐵 + 𝑧 ) ) ∈ 𝐾 ) ) )
81 42 54 76 80 mpbir3and ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝐶 ∼ 𝑧 ) → ( 𝐵 + 𝐶 ) ∼ ( 𝐵 + 𝑧 ) )
82 ovex ⊢ ( 𝐵 + 𝑧 ) ∈ V
83 ovex ⊢ ( 𝐵 + 𝐶 ) ∈ V
84 82 83 elec ⊢ ( ( 𝐵 + 𝑧 ) ∈ [ ( 𝐵 + 𝐶 ) ] ∼ ↔ ( 𝐵 + 𝐶 ) ∼ ( 𝐵 + 𝑧 ) )
85 81 84 sylibr ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝐶 ∼ 𝑧 ) → ( 𝐵 + 𝑧 ) ∈ [ ( 𝐵 + 𝐶 ) ] ∼ )
86 32 85 syldan ⊢ ( ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) ∧ 𝑧 ∈ [ 𝐶 ] ∼ ) → ( 𝐵 + 𝑧 ) ∈ [ ( 𝐵 + 𝐶 ) ] ∼ )
87 86 fmpttd ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → ( 𝑧 ∈ [ 𝐶 ] ∼ ↦ ( 𝐵 + 𝑧 ) ) : [ 𝐶 ] ∼ ⟶ [ ( 𝐵 + 𝐶 ) ] ∼ )
88 87 frnd ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → ran ( 𝑧 ∈ [ 𝐶 ] ∼ ↦ ( 𝐵 + 𝑧 ) ) ⊆ [ ( 𝐵 + 𝐶 ) ] ∼ )
89 eqid ⊢ ( 𝑧 ∈ 𝑋 ↦ ( 𝐵 + 𝑧 ) ) = ( 𝑧 ∈ 𝑋 ↦ ( 𝐵 + 𝑧 ) )
90 1 5 89 grplmulf1o ⊢ ( ( 𝐺 ∈ Grp ∧ 𝐵 ∈ 𝑋 ) → ( 𝑧 ∈ 𝑋 ↦ ( 𝐵 + 𝑧 ) ) : 𝑋 –1-1-onto→ 𝑋 )
91 35 39 90 syl2anc ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → ( 𝑧 ∈ 𝑋 ↦ ( 𝐵 + 𝑧 ) ) : 𝑋 –1-1-onto→ 𝑋 )
92 f1of1 ⊢ ( ( 𝑧 ∈ 𝑋 ↦ ( 𝐵 + 𝑧 ) ) : 𝑋 –1-1-onto→ 𝑋 → ( 𝑧 ∈ 𝑋 ↦ ( 𝐵 + 𝑧 ) ) : 𝑋 –1-1→ 𝑋 )
93 91 92 syl ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → ( 𝑧 ∈ 𝑋 ↦ ( 𝐵 + 𝑧 ) ) : 𝑋 –1-1→ 𝑋 )
94 25 ecss ⊢ ( 𝜑 → [ 𝐶 ] ∼ ⊆ 𝑋 )
95 94 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → [ 𝐶 ] ∼ ⊆ 𝑋 )
96 f1ssres ⊢ ( ( ( 𝑧 ∈ 𝑋 ↦ ( 𝐵 + 𝑧 ) ) : 𝑋 –1-1→ 𝑋 ∧ [ 𝐶 ] ∼ ⊆ 𝑋 ) → ( ( 𝑧 ∈ 𝑋 ↦ ( 𝐵 + 𝑧 ) ) ↾ [ 𝐶 ] ∼ ) : [ 𝐶 ] ∼ –1-1→ 𝑋 )
97 93 95 96 syl2anc ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝑧 ∈ 𝑋 ↦ ( 𝐵 + 𝑧 ) ) ↾ [ 𝐶 ] ∼ ) : [ 𝐶 ] ∼ –1-1→ 𝑋 )
98 resmpt ⊢ ( [ 𝐶 ] ∼ ⊆ 𝑋 → ( ( 𝑧 ∈ 𝑋 ↦ ( 𝐵 + 𝑧 ) ) ↾ [ 𝐶 ] ∼ ) = ( 𝑧 ∈ [ 𝐶 ] ∼ ↦ ( 𝐵 + 𝑧 ) ) )
99 f1eq1 ⊢ ( ( ( 𝑧 ∈ 𝑋 ↦ ( 𝐵 + 𝑧 ) ) ↾ [ 𝐶 ] ∼ ) = ( 𝑧 ∈ [ 𝐶 ] ∼ ↦ ( 𝐵 + 𝑧 ) ) → ( ( ( 𝑧 ∈ 𝑋 ↦ ( 𝐵 + 𝑧 ) ) ↾ [ 𝐶 ] ∼ ) : [ 𝐶 ] ∼ –1-1→ 𝑋 ↔ ( 𝑧 ∈ [ 𝐶 ] ∼ ↦ ( 𝐵 + 𝑧 ) ) : [ 𝐶 ] ∼ –1-1→ 𝑋 ) )
100 95 98 99 3syl ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → ( ( ( 𝑧 ∈ 𝑋 ↦ ( 𝐵 + 𝑧 ) ) ↾ [ 𝐶 ] ∼ ) : [ 𝐶 ] ∼ –1-1→ 𝑋 ↔ ( 𝑧 ∈ [ 𝐶 ] ∼ ↦ ( 𝐵 + 𝑧 ) ) : [ 𝐶 ] ∼ –1-1→ 𝑋 ) )
101 97 100 mpbid ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → ( 𝑧 ∈ [ 𝐶 ] ∼ ↦ ( 𝐵 + 𝑧 ) ) : [ 𝐶 ] ∼ –1-1→ 𝑋 )
102 f1f1orn ⊢ ( ( 𝑧 ∈ [ 𝐶 ] ∼ ↦ ( 𝐵 + 𝑧 ) ) : [ 𝐶 ] ∼ –1-1→ 𝑋 → ( 𝑧 ∈ [ 𝐶 ] ∼ ↦ ( 𝐵 + 𝑧 ) ) : [ 𝐶 ] ∼ –1-1-onto→ ran ( 𝑧 ∈ [ 𝐶 ] ∼ ↦ ( 𝐵 + 𝑧 ) ) )
103 101 102 syl ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → ( 𝑧 ∈ [ 𝐶 ] ∼ ↦ ( 𝐵 + 𝑧 ) ) : [ 𝐶 ] ∼ –1-1-onto→ ran ( 𝑧 ∈ [ 𝐶 ] ∼ ↦ ( 𝐵 + 𝑧 ) ) )
104 19 f1oen ⊢ ( ( 𝑧 ∈ [ 𝐶 ] ∼ ↦ ( 𝐵 + 𝑧 ) ) : [ 𝐶 ] ∼ –1-1-onto→ ran ( 𝑧 ∈ [ 𝐶 ] ∼ ↦ ( 𝐵 + 𝑧 ) ) → [ 𝐶 ] ∼ ≈ ran ( 𝑧 ∈ [ 𝐶 ] ∼ ↦ ( 𝐵 + 𝑧 ) ) )
105 ensym ⊢ ( [ 𝐶 ] ∼ ≈ ran ( 𝑧 ∈ [ 𝐶 ] ∼ ↦ ( 𝐵 + 𝑧 ) ) → ran ( 𝑧 ∈ [ 𝐶 ] ∼ ↦ ( 𝐵 + 𝑧 ) ) ≈ [ 𝐶 ] ∼ )
106 103 104 105 3syl ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → ran ( 𝑧 ∈ [ 𝐶 ] ∼ ↦ ( 𝐵 + 𝑧 ) ) ≈ [ 𝐶 ] ∼ )
107 4 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) )
108 1 6 eqgen ⊢ ( ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ [ 𝐶 ] ∼ ∈ ( 𝑋 / ∼ ) ) → 𝐾 ≈ [ 𝐶 ] ∼ )
109 107 12 108 syl2anc ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → 𝐾 ≈ [ 𝐶 ] ∼ )
110 ensym ⊢ ( 𝐾 ≈ [ 𝐶 ] ∼ → [ 𝐶 ] ∼ ≈ 𝐾 )
111 109 110 syl ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → [ 𝐶 ] ∼ ≈ 𝐾 )
112 ecelqsg ⊢ ( ( ∼ ∈ V ∧ ( 𝐵 + 𝐶 ) ∈ 𝑋 ) → [ ( 𝐵 + 𝐶 ) ] ∼ ∈ ( 𝑋 / ∼ ) )
113 9 41 112 sylancr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → [ ( 𝐵 + 𝐶 ) ] ∼ ∈ ( 𝑋 / ∼ ) )
114 1 6 eqgen ⊢ ( ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ∧ [ ( 𝐵 + 𝐶 ) ] ∼ ∈ ( 𝑋 / ∼ ) ) → 𝐾 ≈ [ ( 𝐵 + 𝐶 ) ] ∼ )
115 107 113 114 syl2anc ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → 𝐾 ≈ [ ( 𝐵 + 𝐶 ) ] ∼ )
116 entr ⊢ ( ( [ 𝐶 ] ∼ ≈ 𝐾 ∧ 𝐾 ≈ [ ( 𝐵 + 𝐶 ) ] ∼ ) → [ 𝐶 ] ∼ ≈ [ ( 𝐵 + 𝐶 ) ] ∼ )
117 111 115 116 syl2anc ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → [ 𝐶 ] ∼ ≈ [ ( 𝐵 + 𝐶 ) ] ∼ )
118 entr ⊢ ( ( ran ( 𝑧 ∈ [ 𝐶 ] ∼ ↦ ( 𝐵 + 𝑧 ) ) ≈ [ 𝐶 ] ∼ ∧ [ 𝐶 ] ∼ ≈ [ ( 𝐵 + 𝐶 ) ] ∼ ) → ran ( 𝑧 ∈ [ 𝐶 ] ∼ ↦ ( 𝐵 + 𝑧 ) ) ≈ [ ( 𝐵 + 𝐶 ) ] ∼ )
119 106 117 118 syl2anc ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → ran ( 𝑧 ∈ [ 𝐶 ] ∼ ↦ ( 𝐵 + 𝑧 ) ) ≈ [ ( 𝐵 + 𝐶 ) ] ∼ )
120 fisseneq ⊢ ( ( [ ( 𝐵 + 𝐶 ) ] ∼ ∈ Fin ∧ ran ( 𝑧 ∈ [ 𝐶 ] ∼ ↦ ( 𝐵 + 𝑧 ) ) ⊆ [ ( 𝐵 + 𝐶 ) ] ∼ ∧ ran ( 𝑧 ∈ [ 𝐶 ] ∼ ↦ ( 𝐵 + 𝑧 ) ) ≈ [ ( 𝐵 + 𝐶 ) ] ∼ ) → ran ( 𝑧 ∈ [ 𝐶 ] ∼ ↦ ( 𝐵 + 𝑧 ) ) = [ ( 𝐵 + 𝐶 ) ] ∼ )
121 28 88 119 120 syl3anc ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → ran ( 𝑧 ∈ [ 𝐶 ] ∼ ↦ ( 𝐵 + 𝑧 ) ) = [ ( 𝐵 + 𝐶 ) ] ∼ )
122 23 121 eqtrd ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 · [ 𝐶 ] ∼ ) = [ ( 𝐵 + 𝐶 ) ] ∼ )