pi1grplem

	Ref	Expression
Hypotheses	pi1fval.g	$⊢ G = J π_{1} Y$
	pi1fval.b	$⊢ B = {Base}_{G}$
	pi1fval.3	$⊢ φ \to J \in TopOn (X)$
	pi1fval.4	$⊢ φ \to Y \in X$
	pi1grplem.z	$⊢ \underset{˙}{0} = [0, 1] \times \{Y\}$
Assertion	pi1grplem	$⊢ φ \to (G \in Grp \land [\underset{˙}{0}] ≃_{ph} (J) = 0_{G})$

Proof

Step	Hyp	Ref	Expression
1		pi1fval.g	$⊢ G = J π_{1} Y$
2		pi1fval.b	$⊢ B = {Base}_{G}$
3		pi1fval.3	$⊢ φ \to J \in TopOn (X)$
4		pi1fval.4	$⊢ φ \to Y \in X$
5		pi1grplem.z	$⊢ \underset{˙}{0} = [0, 1] \times \{Y\}$
6		eqid	$⊢ J Ω_{1} Y = J Ω_{1} Y$
7	1 3 4 6	pi1val	$⊢ φ \to G = (J Ω_{1} Y) /_{𝑠} ≃_{ph} (J)$
8	2	a1i	$⊢ φ \to B = {Base}_{G}$
9		eqidd	$⊢ φ \to {Base}_{(J Ω_{1} Y)} = {Base}_{(J Ω_{1} Y)}$
10	1 3 4 6 8 9	pi1buni	$⊢ φ \to ⋃ B = {Base}_{(J Ω_{1} Y)}$
11		fvexd	$⊢ φ \to ≃_{ph} (J) \in V$
12		ovexd	$⊢ φ \to J Ω_{1} Y \in V$
13	1 3 4 6 8 10	pi1blem	$⊢ φ \to (≃_{ph} (J) [⋃ B] \subseteq ⋃ B \land ⋃ B \subseteq II Cn J)$
14	13	simpld	$⊢ φ \to ≃_{ph} (J) [⋃ B] \subseteq ⋃ B$
15	7 10 11 12 14	qusin	$⊢ φ \to G = (J Ω_{1} Y) /_{𝑠} (≃_{ph} (J) \cap (⋃ B \times ⋃ B))$
16	6 3 4	om1plusg	$⊢ φ \to *_{𝑝} (J) = +_{(J Ω_{1} Y)}$
17		phtpcer	$⊢ ≃_{ph} (J) Er (II Cn J)$
18	17	a1i	$⊢ φ \to ≃_{ph} (J) Er (II Cn J)$
19	13	simprd	$⊢ φ \to ⋃ B \subseteq II Cn J$
20	18 19	erinxp	$⊢ φ \to (≃_{ph} (J) \cap (⋃ B \times ⋃ B)) Er ⋃ B$
21		eqid	$⊢ ≃_{ph} (J) \cap (⋃ B \times ⋃ B) = ≃_{ph} (J) \cap (⋃ B \times ⋃ B)$
22		eqid	$⊢ +_{(J Ω_{1} Y)} = +_{(J Ω_{1} Y)}$
23	1 3 4 8 21 6 22	pi1cpbl	$⊢ φ \to ((a (≃_{ph} (J) \cap (⋃ B \times ⋃ B)) c \land b (≃_{ph} (J) \cap (⋃ B \times ⋃ B)) d) \to (a +_{(J Ω_{1} Y)} b) (≃_{ph} (J) \cap (⋃ B \times ⋃ B)) (c +_{(J Ω_{1} Y)} d))$
24	16	oveqd	$⊢ φ \to a *_{𝑝} (J) b = a +_{(J Ω_{1} Y)} b$
25	16	oveqd	$⊢ φ \to c *_{𝑝} (J) d = c +_{(J Ω_{1} Y)} d$
26	24 25	breq12d	$⊢ φ \to ((a _{𝑝} (J) b) (≃_{ph} (J) \cap (⋃ B \times ⋃ B)) (c _{𝑝} (J) d) \leftrightarrow (a +_{(J Ω_{1} Y)} b) (≃_{ph} (J) \cap (⋃ B \times ⋃ B)) (c +_{(J Ω_{1} Y)} d))$
27	23 26	sylibrd	$⊢ φ \to ((a (≃_{ph} (J) \cap (⋃ B \times ⋃ B)) c \land b (≃_{ph} (J) \cap (⋃ B \times ⋃ B)) d) \to (a _{𝑝} (J) b) (≃_{ph} (J) \cap (⋃ B \times ⋃ B)) (c _{𝑝} (J) d))$
28	3	3ad2ant1	$⊢ (φ \land x \in ⋃ B \land y \in ⋃ B) \to J \in TopOn (X)$
29	4	3ad2ant1	$⊢ (φ \land x \in ⋃ B \land y \in ⋃ B) \to Y \in X$
30	10	3ad2ant1	$⊢ (φ \land x \in ⋃ B \land y \in ⋃ B) \to ⋃ B = {Base}_{(J Ω_{1} Y)}$
31		simp2	$⊢ (φ \land x \in ⋃ B \land y \in ⋃ B) \to x \in ⋃ B$
32		simp3	$⊢ (φ \land x \in ⋃ B \land y \in ⋃ B) \to y \in ⋃ B$
33	6 28 29 30 31 32	om1addcl	$⊢ (φ \land x \in ⋃ B \land y \in ⋃ B) \to x *_{𝑝} (J) y \in ⋃ B$
34	3	adantr	$⊢ (φ \land (x \in ⋃ B \land y \in ⋃ B \land z \in ⋃ B)) \to J \in TopOn (X)$
35	4	adantr	$⊢ (φ \land (x \in ⋃ B \land y \in ⋃ B \land z \in ⋃ B)) \to Y \in X$
36	10	adantr	$⊢ (φ \land (x \in ⋃ B \land y \in ⋃ B \land z \in ⋃ B)) \to ⋃ B = {Base}_{(J Ω_{1} Y)}$
37	33	3adant3r3	$⊢ (φ \land (x \in ⋃ B \land y \in ⋃ B \land z \in ⋃ B)) \to x *_{𝑝} (J) y \in ⋃ B$
38		simpr3	$⊢ (φ \land (x \in ⋃ B \land y \in ⋃ B \land z \in ⋃ B)) \to z \in ⋃ B$
39	6 34 35 36 37 38	om1addcl	$⊢ (φ \land (x \in ⋃ B \land y \in ⋃ B \land z \in ⋃ B)) \to (x _{𝑝} (J) y) _{𝑝} (J) z \in ⋃ B$
40		simpr1	$⊢ (φ \land (x \in ⋃ B \land y \in ⋃ B \land z \in ⋃ B)) \to x \in ⋃ B$
41		simpr2	$⊢ (φ \land (x \in ⋃ B \land y \in ⋃ B \land z \in ⋃ B)) \to y \in ⋃ B$
42	6 34 35 36 41 38	om1addcl	$⊢ (φ \land (x \in ⋃ B \land y \in ⋃ B \land z \in ⋃ B)) \to y *_{𝑝} (J) z \in ⋃ B$
43	6 34 35 36 40 42	om1addcl	$⊢ (φ \land (x \in ⋃ B \land y \in ⋃ B \land z \in ⋃ B)) \to x _{𝑝} (J) (y _{𝑝} (J) z) \in ⋃ B$
44	1 3 4 8	pi1eluni	$⊢ φ \to (x \in ⋃ B \leftrightarrow (x \in (II Cn J) \land x (0) = Y \land x (1) = Y))$
45	44	biimpa	$⊢ (φ \land x \in ⋃ B) \to (x \in (II Cn J) \land x (0) = Y \land x (1) = Y)$
46	45	3ad2antr1	$⊢ (φ \land (x \in ⋃ B \land y \in ⋃ B \land z \in ⋃ B)) \to (x \in (II Cn J) \land x (0) = Y \land x (1) = Y)$
47	46	simp1d	$⊢ (φ \land (x \in ⋃ B \land y \in ⋃ B \land z \in ⋃ B)) \to x \in (II Cn J)$
48	2	a1i	$⊢ (φ \land (x \in ⋃ B \land y \in ⋃ B \land z \in ⋃ B)) \to B = {Base}_{G}$
49	1 34 35 48	pi1eluni	$⊢ (φ \land (x \in ⋃ B \land y \in ⋃ B \land z \in ⋃ B)) \to (y \in ⋃ B \leftrightarrow (y \in (II Cn J) \land y (0) = Y \land y (1) = Y))$
50	41 49	mpbid	$⊢ (φ \land (x \in ⋃ B \land y \in ⋃ B \land z \in ⋃ B)) \to (y \in (II Cn J) \land y (0) = Y \land y (1) = Y)$
51	50	simp1d	$⊢ (φ \land (x \in ⋃ B \land y \in ⋃ B \land z \in ⋃ B)) \to y \in (II Cn J)$
52	1 34 35 48	pi1eluni	$⊢ (φ \land (x \in ⋃ B \land y \in ⋃ B \land z \in ⋃ B)) \to (z \in ⋃ B \leftrightarrow (z \in (II Cn J) \land z (0) = Y \land z (1) = Y))$
53	38 52	mpbid	$⊢ (φ \land (x \in ⋃ B \land y \in ⋃ B \land z \in ⋃ B)) \to (z \in (II Cn J) \land z (0) = Y \land z (1) = Y)$
54	53	simp1d	$⊢ (φ \land (x \in ⋃ B \land y \in ⋃ B \land z \in ⋃ B)) \to z \in (II Cn J)$
55	46	simp3d	$⊢ (φ \land (x \in ⋃ B \land y \in ⋃ B \land z \in ⋃ B)) \to x (1) = Y$
56	50	simp2d	$⊢ (φ \land (x \in ⋃ B \land y \in ⋃ B \land z \in ⋃ B)) \to y (0) = Y$
57	55 56	eqtr4d	$⊢ (φ \land (x \in ⋃ B \land y \in ⋃ B \land z \in ⋃ B)) \to x (1) = y (0)$
58	50	simp3d	$⊢ (φ \land (x \in ⋃ B \land y \in ⋃ B \land z \in ⋃ B)) \to y (1) = Y$
59	53	simp2d	$⊢ (φ \land (x \in ⋃ B \land y \in ⋃ B \land z \in ⋃ B)) \to z (0) = Y$
60	58 59	eqtr4d	$⊢ (φ \land (x \in ⋃ B \land y \in ⋃ B \land z \in ⋃ B)) \to y (1) = z (0)$
61		eqid	$⊢ (u \in [0, 1] ⟼ if (u \leq \frac{1}{2}, if (u \leq \frac{1}{4}, 2 u, u + (\frac{1}{4})), (\frac{u}{2}) + (\frac{1}{2}))) = (u \in [0, 1] ⟼ if (u \leq \frac{1}{2}, if (u \leq \frac{1}{4}, 2 u, u + (\frac{1}{4})), (\frac{u}{2}) + (\frac{1}{2})))$
62	47 51 54 57 60 61	pcoass	$⊢ (φ \land (x \in ⋃ B \land y \in ⋃ B \land z \in ⋃ B)) \to ((x _{𝑝} (J) y) _{𝑝} (J) z) ≃_{ph} (J) (x _{𝑝} (J) (y _{𝑝} (J) z))$
63		brinxp2	$⊢ ((x _{𝑝} (J) y) _{𝑝} (J) z) (≃_{ph} (J) \cap (⋃ B \times ⋃ B)) (x _{𝑝} (J) (y _{𝑝} (J) z)) \leftrightarrow (((x _{𝑝} (J) y) _{𝑝} (J) z \in ⋃ B \land x _{𝑝} (J) (y _{𝑝} (J) z) \in ⋃ B) \land ((x _{𝑝} (J) y) _{𝑝} (J) z) ≃_{ph} (J) (x _{𝑝} (J) (y _{𝑝} (J) z)))$
64	39 43 62 63	syl21anbrc	$⊢ (φ \land (x \in ⋃ B \land y \in ⋃ B \land z \in ⋃ B)) \to ((x _{𝑝} (J) y) _{𝑝} (J) z) (≃_{ph} (J) \cap (⋃ B \times ⋃ B)) (x _{𝑝} (J) (y _{𝑝} (J) z))$
65	5	pcoptcl	$⊢ (J \in TopOn (X) \land Y \in X) \to (\underset{˙}{0} \in (II Cn J) \land \underset{˙}{0} (0) = Y \land \underset{˙}{0} (1) = Y)$
66	3 4 65	syl2anc	$⊢ φ \to (\underset{˙}{0} \in (II Cn J) \land \underset{˙}{0} (0) = Y \land \underset{˙}{0} (1) = Y)$
67	1 3 4 8	pi1eluni	$⊢ φ \to (\underset{˙}{0} \in ⋃ B \leftrightarrow (\underset{˙}{0} \in (II Cn J) \land \underset{˙}{0} (0) = Y \land \underset{˙}{0} (1) = Y))$
68	66 67	mpbird	$⊢ φ \to \underset{˙}{0} \in ⋃ B$
69	3	adantr	$⊢ (φ \land x \in ⋃ B) \to J \in TopOn (X)$
70	4	adantr	$⊢ (φ \land x \in ⋃ B) \to Y \in X$
71	10	adantr	$⊢ (φ \land x \in ⋃ B) \to ⋃ B = {Base}_{(J Ω_{1} Y)}$
72	68	adantr	$⊢ (φ \land x \in ⋃ B) \to \underset{˙}{0} \in ⋃ B$
73		simpr	$⊢ (φ \land x \in ⋃ B) \to x \in ⋃ B$
74	6 69 70 71 72 73	om1addcl	$⊢ (φ \land x \in ⋃ B) \to \underset{˙}{0} *_{𝑝} (J) x \in ⋃ B$
75	19	sselda	$⊢ (φ \land x \in ⋃ B) \to x \in (II Cn J)$
76	45	simp2d	$⊢ (φ \land x \in ⋃ B) \to x (0) = Y$
77	5	pcopt	$⊢ (x \in (II Cn J) \land x (0) = Y) \to (\underset{˙}{0} *_{𝑝} (J) x) ≃_{ph} (J) x$
78	75 76 77	syl2anc	$⊢ (φ \land x \in ⋃ B) \to (\underset{˙}{0} *_{𝑝} (J) x) ≃_{ph} (J) x$
79		brinxp2	$⊢ (\underset{˙}{0} _{𝑝} (J) x) (≃_{ph} (J) \cap (⋃ B \times ⋃ B)) x \leftrightarrow ((\underset{˙}{0} _{𝑝} (J) x \in ⋃ B \land x \in ⋃ B) \land (\underset{˙}{0} *_{𝑝} (J) x) ≃_{ph} (J) x)$
80	74 73 78 79	syl21anbrc	$⊢ (φ \land x \in ⋃ B) \to (\underset{˙}{0} *_{𝑝} (J) x) (≃_{ph} (J) \cap (⋃ B \times ⋃ B)) x$
81		eqid	$⊢ (a \in [0, 1] ⟼ x (1 - a)) = (a \in [0, 1] ⟼ x (1 - a))$
82	81	pcorevcl	$⊢ x \in (II Cn J) \to ((a \in [0, 1] ⟼ x (1 - a)) \in (II Cn J) \land (a \in [0, 1] ⟼ x (1 - a)) (0) = x (1) \land (a \in [0, 1] ⟼ x (1 - a)) (1) = x (0))$
83	75 82	syl	$⊢ (φ \land x \in ⋃ B) \to ((a \in [0, 1] ⟼ x (1 - a)) \in (II Cn J) \land (a \in [0, 1] ⟼ x (1 - a)) (0) = x (1) \land (a \in [0, 1] ⟼ x (1 - a)) (1) = x (0))$
84	83	simp1d	$⊢ (φ \land x \in ⋃ B) \to (a \in [0, 1] ⟼ x (1 - a)) \in (II Cn J)$
85	83	simp2d	$⊢ (φ \land x \in ⋃ B) \to (a \in [0, 1] ⟼ x (1 - a)) (0) = x (1)$
86	45	simp3d	$⊢ (φ \land x \in ⋃ B) \to x (1) = Y$
87	85 86	eqtrd	$⊢ (φ \land x \in ⋃ B) \to (a \in [0, 1] ⟼ x (1 - a)) (0) = Y$
88	83	simp3d	$⊢ (φ \land x \in ⋃ B) \to (a \in [0, 1] ⟼ x (1 - a)) (1) = x (0)$
89	88 76	eqtrd	$⊢ (φ \land x \in ⋃ B) \to (a \in [0, 1] ⟼ x (1 - a)) (1) = Y$
90	1 3 4 8	pi1eluni	$⊢ φ \to ((a \in [0, 1] ⟼ x (1 - a)) \in ⋃ B \leftrightarrow ((a \in [0, 1] ⟼ x (1 - a)) \in (II Cn J) \land (a \in [0, 1] ⟼ x (1 - a)) (0) = Y \land (a \in [0, 1] ⟼ x (1 - a)) (1) = Y))$
91	90	adantr	$⊢ (φ \land x \in ⋃ B) \to ((a \in [0, 1] ⟼ x (1 - a)) \in ⋃ B \leftrightarrow ((a \in [0, 1] ⟼ x (1 - a)) \in (II Cn J) \land (a \in [0, 1] ⟼ x (1 - a)) (0) = Y \land (a \in [0, 1] ⟼ x (1 - a)) (1) = Y))$
92	84 87 89 91	mpbir3and	$⊢ (φ \land x \in ⋃ B) \to (a \in [0, 1] ⟼ x (1 - a)) \in ⋃ B$
93	6 69 70 71 92 73	om1addcl	$⊢ (φ \land x \in ⋃ B) \to (a \in [0, 1] ⟼ x (1 - a)) *_{𝑝} (J) x \in ⋃ B$
94		eqid	$⊢ [0, 1] \times \{x (1)\} = [0, 1] \times \{x (1)\}$
95	81 94	pcorev	$⊢ x \in (II Cn J) \to ((a \in [0, 1] ⟼ x (1 - a)) *_{𝑝} (J) x) ≃_{ph} (J) ([0, 1] \times \{x (1)\})$
96	75 95	syl	$⊢ (φ \land x \in ⋃ B) \to ((a \in [0, 1] ⟼ x (1 - a)) *_{𝑝} (J) x) ≃_{ph} (J) ([0, 1] \times \{x (1)\})$
97	86	sneqd	$⊢ (φ \land x \in ⋃ B) \to \{x (1)\} = \{Y\}$
98	97	xpeq2d	$⊢ (φ \land x \in ⋃ B) \to [0, 1] \times \{x (1)\} = [0, 1] \times \{Y\}$
99	5 98	eqtr4id	$⊢ (φ \land x \in ⋃ B) \to \underset{˙}{0} = [0, 1] \times \{x (1)\}$
100	96 99	breqtrrd	$⊢ (φ \land x \in ⋃ B) \to ((a \in [0, 1] ⟼ x (1 - a)) *_{𝑝} (J) x) ≃_{ph} (J) \underset{˙}{0}$
101		brinxp2	$⊢ ((a \in [0, 1] ⟼ x (1 - a)) _{𝑝} (J) x) (≃_{ph} (J) \cap (⋃ B \times ⋃ B)) \underset{˙}{0} \leftrightarrow (((a \in [0, 1] ⟼ x (1 - a)) _{𝑝} (J) x \in ⋃ B \land \underset{˙}{0} \in ⋃ B) \land ((a \in [0, 1] ⟼ x (1 - a)) *_{𝑝} (J) x) ≃_{ph} (J) \underset{˙}{0})$
102	93 72 100 101	syl21anbrc	$⊢ (φ \land x \in ⋃ B) \to ((a \in [0, 1] ⟼ x (1 - a)) *_{𝑝} (J) x) (≃_{ph} (J) \cap (⋃ B \times ⋃ B)) \underset{˙}{0}$
103	15 10 16 20 12 27 33 64 68 80 92 102	qusgrp2	$⊢ φ \to (G \in Grp \land [\underset{˙}{0}] (≃_{ph} (J) \cap (⋃ B \times ⋃ B)) = 0_{G})$
104		ecinxp	$⊢ (≃_{ph} (J) [⋃ B] \subseteq ⋃ B \land \underset{˙}{0} \in ⋃ B) \to [\underset{˙}{0}] ≃_{ph} (J) = [\underset{˙}{0}] (≃_{ph} (J) \cap (⋃ B \times ⋃ B))$
105	14 68 104	syl2anc	$⊢ φ \to [\underset{˙}{0}] ≃_{ph} (J) = [\underset{˙}{0}] (≃_{ph} (J) \cap (⋃ B \times ⋃ B))$
106	105	eqeq1d	$⊢ φ \to ([\underset{˙}{0}] ≃_{ph} (J) = 0_{G} \leftrightarrow [\underset{˙}{0}] (≃_{ph} (J) \cap (⋃ B \times ⋃ B)) = 0_{G})$
107	106	anbi2d	$⊢ φ \to ((G \in Grp \land [\underset{˙}{0}] ≃_{ph} (J) = 0_{G}) \leftrightarrow (G \in Grp \land [\underset{˙}{0}] (≃_{ph} (J) \cap (⋃ B \times ⋃ B)) = 0_{G}))$
108	103 107	mpbird	$⊢ φ \to (G \in Grp \land [\underset{˙}{0}] ≃_{ph} (J) = 0_{G})$

Metamath Proof Explorer

Theorem pi1grplem

Proof