sylow2blem2

Description: Lemma for sylow2b . Left multiplication in a subgroup H is a group action on the set of all left cosets of K . (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	sylow2blem2	$⊢ φ \to \underset{˙}{\cdot} \in ((G ↾_{𝑠} H) GrpAct (X / \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		eqid	$⊢ G ↾_{𝑠} H = G ↾_{𝑠} H$
9	8	subggrp	$⊢ H \in SubGrp (G) \to G ↾_{𝑠} H \in Grp$
10	3 9	syl	$⊢ φ \to G ↾_{𝑠} H \in Grp$
11		pwfi	$⊢ X \in Fin \leftrightarrow 𝒫 X \in Fin$
12	2 11	sylib	$⊢ φ \to 𝒫 X \in Fin$
13	1 6	eqger	$⊢ K \in SubGrp (G) \to \underset{˙}{\sim} Er X$
14	4 13	syl	$⊢ φ \to \underset{˙}{\sim} Er X$
15	14	qsss	$⊢ φ \to X / \underset{˙}{\sim} \subseteq 𝒫 X$
16	12 15	ssexd	$⊢ φ \to X / \underset{˙}{\sim} \in V$
17	10 16	jca	$⊢ φ \to (G ↾_{𝑠} H \in Grp \land X / \underset{˙}{\sim} \in V)$
18		vex	$⊢ y \in V$
19	18	mptex	$⊢ (z \in y ⟼ x \underset{˙}{+} z) \in V$
20	19	rnex	$⊢ ran (z \in y ⟼ x \underset{˙}{+} z) \in V$
21	7 20	fnmpoi	$⊢ \underset{˙}{\cdot} Fn (H \times (X / \underset{˙}{\sim}))$
22	21	a1i	$⊢ φ \to \underset{˙}{\cdot} Fn (H \times (X / \underset{˙}{\sim}))$
23		eqid	$⊢ X / \underset{˙}{\sim} = X / \underset{˙}{\sim}$
24		oveq2	$⊢ [s] \underset{˙}{\sim} = v \to u \underset{˙}{\cdot} [s] \underset{˙}{\sim} = u \underset{˙}{\cdot} v$
25	24	eleq1d	$⊢ [s] \underset{˙}{\sim} = v \to (u \underset{˙}{\cdot} [s] \underset{˙}{\sim} \in (X / \underset{˙}{\sim}) \leftrightarrow u \underset{˙}{\cdot} v \in (X / \underset{˙}{\sim}))$
26	1 2 3 4 5 6 7	sylow2blem1	$⊢ (φ \land u \in H \land s \in X) \to u \underset{˙}{\cdot} [s] \underset{˙}{\sim} = [(u \underset{˙}{+} s)] \underset{˙}{\sim}$
27	6	ovexi	$⊢ \underset{˙}{\sim} \in V$
28		subgrcl	$⊢ H \in SubGrp (G) \to G \in Grp$
29	3 28	syl	$⊢ φ \to G \in Grp$
30	29	3ad2ant1	$⊢ (φ \land u \in H \land s \in X) \to G \in Grp$
31	1	subgss	$⊢ H \in SubGrp (G) \to H \subseteq X$
32	3 31	syl	$⊢ φ \to H \subseteq X$
33	32	sselda	$⊢ (φ \land u \in H) \to u \in X$
34	33	3adant3	$⊢ (φ \land u \in H \land s \in X) \to u \in X$
35		simp3	$⊢ (φ \land u \in H \land s \in X) \to s \in X$
36	1 5	grpcl	$⊢ (G \in Grp \land u \in X \land s \in X) \to u \underset{˙}{+} s \in X$
37	30 34 35 36	syl3anc	$⊢ (φ \land u \in H \land s \in X) \to u \underset{˙}{+} s \in X$
38		ecelqsw	$⊢ (\underset{˙}{\sim} \in V \land u \underset{˙}{+} s \in X) \to [(u \underset{˙}{+} s)] \underset{˙}{\sim} \in (X / \underset{˙}{\sim})$
39	27 37 38	sylancr	$⊢ (φ \land u \in H \land s \in X) \to [(u \underset{˙}{+} s)] \underset{˙}{\sim} \in (X / \underset{˙}{\sim})$
40	26 39	eqeltrd	$⊢ (φ \land u \in H \land s \in X) \to u \underset{˙}{\cdot} [s] \underset{˙}{\sim} \in (X / \underset{˙}{\sim})$
41	40	3expa	$⊢ ((φ \land u \in H) \land s \in X) \to u \underset{˙}{\cdot} [s] \underset{˙}{\sim} \in (X / \underset{˙}{\sim})$
42	23 25 41	ectocld	$⊢ ((φ \land u \in H) \land v \in (X / \underset{˙}{\sim})) \to u \underset{˙}{\cdot} v \in (X / \underset{˙}{\sim})$
43	42	ralrimiva	$⊢ (φ \land u \in H) \to \forall v \in (X / \underset{˙}{\sim}) u \underset{˙}{\cdot} v \in (X / \underset{˙}{\sim})$
44	43	ralrimiva	$⊢ φ \to \forall u \in H \forall v \in (X / \underset{˙}{\sim}) u \underset{˙}{\cdot} v \in (X / \underset{˙}{\sim})$
45		ffnov	$⊢ \underset{˙}{\cdot} : H \times (X / \underset{˙}{\sim}) ⟶ X / \underset{˙}{\sim} \leftrightarrow (\underset{˙}{\cdot} Fn (H \times (X / \underset{˙}{\sim})) \land \forall u \in H \forall v \in (X / \underset{˙}{\sim}) u \underset{˙}{\cdot} v \in (X / \underset{˙}{\sim}))$
46	22 44 45	sylanbrc	$⊢ φ \to \underset{˙}{\cdot} : H \times (X / \underset{˙}{\sim}) ⟶ X / \underset{˙}{\sim}$
47	8	subgbas	$⊢ H \in SubGrp (G) \to H = {Base}_{(G ↾_{𝑠} H)}$
48	3 47	syl	$⊢ φ \to H = {Base}_{(G ↾_{𝑠} H)}$
49	48	xpeq1d	$⊢ φ \to H \times (X / \underset{˙}{\sim}) = {Base}_{(G ↾_{𝑠} H)} \times (X / \underset{˙}{\sim})$
50	49	feq2d	$⊢ φ \to (\underset{˙}{\cdot} : H \times (X / \underset{˙}{\sim}) ⟶ X / \underset{˙}{\sim} \leftrightarrow \underset{˙}{\cdot} : {Base}_{(G ↾_{𝑠} H)} \times (X / \underset{˙}{\sim}) ⟶ X / \underset{˙}{\sim})$
51	46 50	mpbid	$⊢ φ \to \underset{˙}{\cdot} : {Base}_{(G ↾_{𝑠} H)} \times (X / \underset{˙}{\sim}) ⟶ X / \underset{˙}{\sim}$
52		oveq2	$⊢ [s] \underset{˙}{\sim} = u \to 0_{(G ↾_{𝑠} H)} \underset{˙}{\cdot} [s] \underset{˙}{\sim} = 0_{(G ↾_{𝑠} H)} \underset{˙}{\cdot} u$
53		id	$⊢ [s] \underset{˙}{\sim} = u \to [s] \underset{˙}{\sim} = u$
54	52 53	eqeq12d	$⊢ [s] \underset{˙}{\sim} = u \to (0_{(G ↾_{𝑠} H)} \underset{˙}{\cdot} [s] \underset{˙}{\sim} = [s] \underset{˙}{\sim} \leftrightarrow 0_{(G ↾_{𝑠} H)} \underset{˙}{\cdot} u = u)$
55		oveq2	$⊢ [s] \underset{˙}{\sim} = u \to (a +_{(G ↾_{𝑠} H)} b) \underset{˙}{\cdot} [s] \underset{˙}{\sim} = (a +_{(G ↾_{𝑠} H)} b) \underset{˙}{\cdot} u$
56		oveq2	$⊢ [s] \underset{˙}{\sim} = u \to b \underset{˙}{\cdot} [s] \underset{˙}{\sim} = b \underset{˙}{\cdot} u$
57	56	oveq2d	$⊢ [s] \underset{˙}{\sim} = u \to a \underset{˙}{\cdot} (b \underset{˙}{\cdot} [s] \underset{˙}{\sim}) = a \underset{˙}{\cdot} (b \underset{˙}{\cdot} u)$
58	55 57	eqeq12d	$⊢ [s] \underset{˙}{\sim} = u \to ((a +_{(G ↾_{𝑠} H)} b) \underset{˙}{\cdot} [s] \underset{˙}{\sim} = a \underset{˙}{\cdot} (b \underset{˙}{\cdot} [s] \underset{˙}{\sim}) \leftrightarrow (a +_{(G ↾_{𝑠} H)} b) \underset{˙}{\cdot} u = a \underset{˙}{\cdot} (b \underset{˙}{\cdot} u))$
59	58	2ralbidv	$⊢ [s] \underset{˙}{\sim} = u \to (\forall a \in {Base}_{(G ↾_{𝑠} H)} \forall b \in {Base}_{(G ↾_{𝑠} H)} (a +_{(G ↾_{𝑠} H)} b) \underset{˙}{\cdot} [s] \underset{˙}{\sim} = a \underset{˙}{\cdot} (b \underset{˙}{\cdot} [s] \underset{˙}{\sim}) \leftrightarrow \forall a \in {Base}_{(G ↾_{𝑠} H)} \forall b \in {Base}_{(G ↾_{𝑠} H)} (a +_{(G ↾_{𝑠} H)} b) \underset{˙}{\cdot} u = a \underset{˙}{\cdot} (b \underset{˙}{\cdot} u))$
60	54 59	anbi12d	$⊢ [s] \underset{˙}{\sim} = u \to ((0_{(G ↾_{𝑠} H)} \underset{˙}{\cdot} [s] \underset{˙}{\sim} = [s] \underset{˙}{\sim} \land \forall a \in {Base}_{(G ↾_{𝑠} H)} \forall b \in {Base}_{(G ↾_{𝑠} H)} (a +_{(G ↾_{𝑠} H)} b) \underset{˙}{\cdot} [s] \underset{˙}{\sim} = a \underset{˙}{\cdot} (b \underset{˙}{\cdot} [s] \underset{˙}{\sim})) \leftrightarrow (0_{(G ↾_{𝑠} H)} \underset{˙}{\cdot} u = u \land \forall a \in {Base}_{(G ↾_{𝑠} H)} \forall b \in {Base}_{(G ↾_{𝑠} H)} (a +_{(G ↾_{𝑠} H)} b) \underset{˙}{\cdot} u = a \underset{˙}{\cdot} (b \underset{˙}{\cdot} u)))$
61		simpl	$⊢ (φ \land s \in X) \to φ$
62	3	adantr	$⊢ (φ \land s \in X) \to H \in SubGrp (G)$
63		eqid	$⊢ 0_{G} = 0_{G}$
64	63	subg0cl	$⊢ H \in SubGrp (G) \to 0_{G} \in H$
65	62 64	syl	$⊢ (φ \land s \in X) \to 0_{G} \in H$
66		simpr	$⊢ (φ \land s \in X) \to s \in X$
67	1 2 3 4 5 6 7	sylow2blem1	$⊢ (φ \land 0_{G} \in H \land s \in X) \to 0_{G} \underset{˙}{\cdot} [s] \underset{˙}{\sim} = [(0_{G} \underset{˙}{+} s)] \underset{˙}{\sim}$
68	61 65 66 67	syl3anc	$⊢ (φ \land s \in X) \to 0_{G} \underset{˙}{\cdot} [s] \underset{˙}{\sim} = [(0_{G} \underset{˙}{+} s)] \underset{˙}{\sim}$
69	8 63	subg0	$⊢ H \in SubGrp (G) \to 0_{G} = 0_{(G ↾_{𝑠} H)}$
70	62 69	syl	$⊢ (φ \land s \in X) \to 0_{G} = 0_{(G ↾_{𝑠} H)}$
71	70	oveq1d	$⊢ (φ \land s \in X) \to 0_{G} \underset{˙}{\cdot} [s] \underset{˙}{\sim} = 0_{(G ↾_{𝑠} H)} \underset{˙}{\cdot} [s] \underset{˙}{\sim}$
72	1 5 63	grplid	$⊢ (G \in Grp \land s \in X) \to 0_{G} \underset{˙}{+} s = s$
73	29 72	sylan	$⊢ (φ \land s \in X) \to 0_{G} \underset{˙}{+} s = s$
74	73	eceq1d	$⊢ (φ \land s \in X) \to [(0_{G} \underset{˙}{+} s)] \underset{˙}{\sim} = [s] \underset{˙}{\sim}$
75	68 71 74	3eqtr3d	$⊢ (φ \land s \in X) \to 0_{(G ↾_{𝑠} H)} \underset{˙}{\cdot} [s] \underset{˙}{\sim} = [s] \underset{˙}{\sim}$
76	62	adantr	$⊢ ((φ \land s \in X) \land (a \in H \land b \in H)) \to H \in SubGrp (G)$
77	76 28	syl	$⊢ ((φ \land s \in X) \land (a \in H \land b \in H)) \to G \in Grp$
78	76 31	syl	$⊢ ((φ \land s \in X) \land (a \in H \land b \in H)) \to H \subseteq X$
79		simprl	$⊢ ((φ \land s \in X) \land (a \in H \land b \in H)) \to a \in H$
80	78 79	sseldd	$⊢ ((φ \land s \in X) \land (a \in H \land b \in H)) \to a \in X$
81		simprr	$⊢ ((φ \land s \in X) \land (a \in H \land b \in H)) \to b \in H$
82	78 81	sseldd	$⊢ ((φ \land s \in X) \land (a \in H \land b \in H)) \to b \in X$
83	66	adantr	$⊢ ((φ \land s \in X) \land (a \in H \land b \in H)) \to s \in X$
84	1 5	grpass	$⊢ (G \in Grp \land (a \in X \land b \in X \land s \in X)) \to (a \underset{˙}{+} b) \underset{˙}{+} s = a \underset{˙}{+} (b \underset{˙}{+} s)$
85	77 80 82 83 84	syl13anc	$⊢ ((φ \land s \in X) \land (a \in H \land b \in H)) \to (a \underset{˙}{+} b) \underset{˙}{+} s = a \underset{˙}{+} (b \underset{˙}{+} s)$
86	85	eceq1d	$⊢ ((φ \land s \in X) \land (a \in H \land b \in H)) \to [((a \underset{˙}{+} b) \underset{˙}{+} s)] \underset{˙}{\sim} = [(a \underset{˙}{+} (b \underset{˙}{+} s))] \underset{˙}{\sim}$
87	61	adantr	$⊢ ((φ \land s \in X) \land (a \in H \land b \in H)) \to φ$
88	1 5	grpcl	$⊢ (G \in Grp \land b \in X \land s \in X) \to b \underset{˙}{+} s \in X$
89	77 82 83 88	syl3anc	$⊢ ((φ \land s \in X) \land (a \in H \land b \in H)) \to b \underset{˙}{+} s \in X$
90	1 2 3 4 5 6 7	sylow2blem1	$⊢ (φ \land a \in H \land b \underset{˙}{+} s \in X) \to a \underset{˙}{\cdot} [(b \underset{˙}{+} s)] \underset{˙}{\sim} = [(a \underset{˙}{+} (b \underset{˙}{+} s))] \underset{˙}{\sim}$
91	87 79 89 90	syl3anc	$⊢ ((φ \land s \in X) \land (a \in H \land b \in H)) \to a \underset{˙}{\cdot} [(b \underset{˙}{+} s)] \underset{˙}{\sim} = [(a \underset{˙}{+} (b \underset{˙}{+} s))] \underset{˙}{\sim}$
92	86 91	eqtr4d	$⊢ ((φ \land s \in X) \land (a \in H \land b \in H)) \to [((a \underset{˙}{+} b) \underset{˙}{+} s)] \underset{˙}{\sim} = a \underset{˙}{\cdot} [(b \underset{˙}{+} s)] \underset{˙}{\sim}$
93	5	subgcl	$⊢ (H \in SubGrp (G) \land a \in H \land b \in H) \to a \underset{˙}{+} b \in H$
94	76 79 81 93	syl3anc	$⊢ ((φ \land s \in X) \land (a \in H \land b \in H)) \to a \underset{˙}{+} b \in H$
95	1 2 3 4 5 6 7	sylow2blem1	$⊢ (φ \land a \underset{˙}{+} b \in H \land s \in X) \to (a \underset{˙}{+} b) \underset{˙}{\cdot} [s] \underset{˙}{\sim} = [((a \underset{˙}{+} b) \underset{˙}{+} s)] \underset{˙}{\sim}$
96	87 94 83 95	syl3anc	$⊢ ((φ \land s \in X) \land (a \in H \land b \in H)) \to (a \underset{˙}{+} b) \underset{˙}{\cdot} [s] \underset{˙}{\sim} = [((a \underset{˙}{+} b) \underset{˙}{+} s)] \underset{˙}{\sim}$
97	1 2 3 4 5 6 7	sylow2blem1	$⊢ (φ \land b \in H \land s \in X) \to b \underset{˙}{\cdot} [s] \underset{˙}{\sim} = [(b \underset{˙}{+} s)] \underset{˙}{\sim}$
98	87 81 83 97	syl3anc	$⊢ ((φ \land s \in X) \land (a \in H \land b \in H)) \to b \underset{˙}{\cdot} [s] \underset{˙}{\sim} = [(b \underset{˙}{+} s)] \underset{˙}{\sim}$
99	98	oveq2d	$⊢ ((φ \land s \in X) \land (a \in H \land b \in H)) \to a \underset{˙}{\cdot} (b \underset{˙}{\cdot} [s] \underset{˙}{\sim}) = a \underset{˙}{\cdot} [(b \underset{˙}{+} s)] \underset{˙}{\sim}$
100	92 96 99	3eqtr4d	$⊢ ((φ \land s \in X) \land (a \in H \land b \in H)) \to (a \underset{˙}{+} b) \underset{˙}{\cdot} [s] \underset{˙}{\sim} = a \underset{˙}{\cdot} (b \underset{˙}{\cdot} [s] \underset{˙}{\sim})$
101	100	ralrimivva	$⊢ (φ \land s \in X) \to \forall a \in H \forall b \in H (a \underset{˙}{+} b) \underset{˙}{\cdot} [s] \underset{˙}{\sim} = a \underset{˙}{\cdot} (b \underset{˙}{\cdot} [s] \underset{˙}{\sim})$
102	62 47	syl	$⊢ (φ \land s \in X) \to H = {Base}_{(G ↾_{𝑠} H)}$
103	8 5	ressplusg	$⊢ H \in SubGrp (G) \to \underset{˙}{+} = +_{(G ↾_{𝑠} H)}$
104	3 103	syl	$⊢ φ \to \underset{˙}{+} = +_{(G ↾_{𝑠} H)}$
105	104	oveqdr	$⊢ (φ \land s \in X) \to a \underset{˙}{+} b = a +_{(G ↾_{𝑠} H)} b$
106	105	oveq1d	$⊢ (φ \land s \in X) \to (a \underset{˙}{+} b) \underset{˙}{\cdot} [s] \underset{˙}{\sim} = (a +_{(G ↾_{𝑠} H)} b) \underset{˙}{\cdot} [s] \underset{˙}{\sim}$
107	106	eqeq1d	$⊢ (φ \land s \in X) \to ((a \underset{˙}{+} b) \underset{˙}{\cdot} [s] \underset{˙}{\sim} = a \underset{˙}{\cdot} (b \underset{˙}{\cdot} [s] \underset{˙}{\sim}) \leftrightarrow (a +_{(G ↾_{𝑠} H)} b) \underset{˙}{\cdot} [s] \underset{˙}{\sim} = a \underset{˙}{\cdot} (b \underset{˙}{\cdot} [s] \underset{˙}{\sim}))$
108	102 107	raleqbidv	$⊢ (φ \land s \in X) \to (\forall b \in H (a \underset{˙}{+} b) \underset{˙}{\cdot} [s] \underset{˙}{\sim} = a \underset{˙}{\cdot} (b \underset{˙}{\cdot} [s] \underset{˙}{\sim}) \leftrightarrow \forall b \in {Base}_{(G ↾_{𝑠} H)} (a +_{(G ↾_{𝑠} H)} b) \underset{˙}{\cdot} [s] \underset{˙}{\sim} = a \underset{˙}{\cdot} (b \underset{˙}{\cdot} [s] \underset{˙}{\sim}))$
109	102 108	raleqbidv	$⊢ (φ \land s \in X) \to (\forall a \in H \forall b \in H (a \underset{˙}{+} b) \underset{˙}{\cdot} [s] \underset{˙}{\sim} = a \underset{˙}{\cdot} (b \underset{˙}{\cdot} [s] \underset{˙}{\sim}) \leftrightarrow \forall a \in {Base}_{(G ↾_{𝑠} H)} \forall b \in {Base}_{(G ↾_{𝑠} H)} (a +_{(G ↾_{𝑠} H)} b) \underset{˙}{\cdot} [s] \underset{˙}{\sim} = a \underset{˙}{\cdot} (b \underset{˙}{\cdot} [s] \underset{˙}{\sim}))$
110	101 109	mpbid	$⊢ (φ \land s \in X) \to \forall a \in {Base}_{(G ↾_{𝑠} H)} \forall b \in {Base}_{(G ↾_{𝑠} H)} (a +_{(G ↾_{𝑠} H)} b) \underset{˙}{\cdot} [s] \underset{˙}{\sim} = a \underset{˙}{\cdot} (b \underset{˙}{\cdot} [s] \underset{˙}{\sim})$
111	75 110	jca	$⊢ (φ \land s \in X) \to (0_{(G ↾_{𝑠} H)} \underset{˙}{\cdot} [s] \underset{˙}{\sim} = [s] \underset{˙}{\sim} \land \forall a \in {Base}_{(G ↾_{𝑠} H)} \forall b \in {Base}_{(G ↾_{𝑠} H)} (a +_{(G ↾_{𝑠} H)} b) \underset{˙}{\cdot} [s] \underset{˙}{\sim} = a \underset{˙}{\cdot} (b \underset{˙}{\cdot} [s] \underset{˙}{\sim}))$
112	23 60 111	ectocld	$⊢ (φ \land u \in (X / \underset{˙}{\sim})) \to (0_{(G ↾_{𝑠} H)} \underset{˙}{\cdot} u = u \land \forall a \in {Base}_{(G ↾_{𝑠} H)} \forall b \in {Base}_{(G ↾_{𝑠} H)} (a +_{(G ↾_{𝑠} H)} b) \underset{˙}{\cdot} u = a \underset{˙}{\cdot} (b \underset{˙}{\cdot} u))$
113	112	ralrimiva	$⊢ φ \to \forall u \in (X / \underset{˙}{\sim}) (0_{(G ↾_{𝑠} H)} \underset{˙}{\cdot} u = u \land \forall a \in {Base}_{(G ↾_{𝑠} H)} \forall b \in {Base}_{(G ↾_{𝑠} H)} (a +_{(G ↾_{𝑠} H)} b) \underset{˙}{\cdot} u = a \underset{˙}{\cdot} (b \underset{˙}{\cdot} u))$
114	51 113	jca	$⊢ φ \to (\underset{˙}{\cdot} : {Base}_{(G ↾_{𝑠} H)} \times (X / \underset{˙}{\sim}) ⟶ X / \underset{˙}{\sim} \land \forall u \in (X / \underset{˙}{\sim}) (0_{(G ↾_{𝑠} H)} \underset{˙}{\cdot} u = u \land \forall a \in {Base}_{(G ↾_{𝑠} H)} \forall b \in {Base}_{(G ↾_{𝑠} H)} (a +_{(G ↾_{𝑠} H)} b) \underset{˙}{\cdot} u = a \underset{˙}{\cdot} (b \underset{˙}{\cdot} u)))$
115		eqid	$⊢ {Base}_{(G ↾_{𝑠} H)} = {Base}_{(G ↾_{𝑠} H)}$
116		eqid	$⊢ +_{(G ↾_{𝑠} H)} = +_{(G ↾_{𝑠} H)}$
117		eqid	$⊢ 0_{(G ↾_{𝑠} H)} = 0_{(G ↾_{𝑠} H)}$
118	115 116 117	isga	$⊢ \underset{˙}{\cdot} \in ((G ↾_{𝑠} H) GrpAct (X / \underset{˙}{\sim})) \leftrightarrow ((G ↾_{𝑠} H \in Grp \land X / \underset{˙}{\sim} \in V) \land (\underset{˙}{\cdot} : {Base}_{(G ↾_{𝑠} H)} \times (X / \underset{˙}{\sim}) ⟶ X / \underset{˙}{\sim} \land \forall u \in (X / \underset{˙}{\sim}) (0_{(G ↾_{𝑠} H)} \underset{˙}{\cdot} u = u \land \forall a \in {Base}_{(G ↾_{𝑠} H)} \forall b \in {Base}_{(G ↾_{𝑠} H)} (a +_{(G ↾_{𝑠} H)} b) \underset{˙}{\cdot} u = a \underset{˙}{\cdot} (b \underset{˙}{\cdot} u))))$
119	17 114 118	sylanbrc	$⊢ φ \to \underset{˙}{\cdot} \in ((G ↾_{𝑠} H) GrpAct (X / \underset{˙}{\sim}))$

Metamath Proof Explorer

Theorem sylow2blem2

Proof