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	$⊢ X = {Base}_{G}$
	sylow2b.xf	$⊢ φ \to X \in Fin$
	sylow2b.h	$⊢ φ \to H \in SubGrp (G)$
	sylow2b.k	$⊢ φ \to K \in SubGrp (G)$
	sylow2b.a	$⊢ \underset{˙}{+} = +_{G}$
	sylow2b.r	$⊢ \underset{˙}{\sim} = G ~_{QG} K$
	sylow2b.m	$⊢ \underset{˙}{\cdot} = (x \in H, y \in (X / \underset{˙}{\sim}) ⟼ ran (z \in y ⟼ x \underset{˙}{+} z))$
Assertion	sylow2blem1	$⊢ (φ \land B \in H \land C \in X) \to B \underset{˙}{\cdot} [C] \underset{˙}{\sim} = [(B \underset{˙}{+} C)] \underset{˙}{\sim}$

Proof

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

Metamath Proof Explorer

Theorem sylow2blem1

Proof