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	⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 · [ 𝐶 ] ∼ ) = [ ( 𝐵 + 𝐶 ) ] ∼ )