frgpnabllem2

Description: Lemma for frgpnabl . (Contributed by Mario Carneiro, 21-Apr-2016) (Revised by AV, 25-Apr-2024)

	Ref	Expression
Hypotheses	frgpnabl.g	$⊢ G = freeGrp (I)$
	frgpnabl.w	$⊢ W = I (Word (I \times 2_{𝑜}))$
	frgpnabl.r	$⊢ \underset{˙}{\sim} = ~_{FG} (I)$
	frgpnabl.p	$⊢ \underset{˙}{+} = +_{G}$
	frgpnabl.m	$⊢ M = (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩)$
	frgpnabl.t	$⊢ T = (v \in W ⟼ (n \in (0 \dots \|v\|), w \in (I \times 2_{𝑜}) ⟼ v splice ⟨n, n, ⟨“ w M (w) ”⟩⟩))$
	frgpnabl.d	$⊢ D = W ∖ ⋃_{x \in W} ran T (x)$
	frgpnabl.u	$⊢ U = {var}_{FGrp} (I)$
	frgpnabl.i	$⊢ φ \to I \in V$
	frgpnabl.a	$⊢ φ \to A \in I$
	frgpnabl.b	$⊢ φ \to B \in I$
	frgpnabl.n	$⊢ φ \to U (A) \underset{˙}{+} U (B) = U (B) \underset{˙}{+} U (A)$
Assertion	frgpnabllem2	$⊢ φ \to A = B$

Proof

Step	Hyp	Ref	Expression
1		frgpnabl.g	$⊢ G = freeGrp (I)$
2		frgpnabl.w	$⊢ W = I (Word (I \times 2_{𝑜}))$
3		frgpnabl.r	$⊢ \underset{˙}{\sim} = ~_{FG} (I)$
4		frgpnabl.p	$⊢ \underset{˙}{+} = +_{G}$
5		frgpnabl.m	$⊢ M = (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩)$
6		frgpnabl.t	$⊢ T = (v \in W ⟼ (n \in (0 \dots \|v\|), w \in (I \times 2_{𝑜}) ⟼ v splice ⟨n, n, ⟨“ w M (w) ”⟩⟩))$
7		frgpnabl.d	$⊢ D = W ∖ ⋃_{x \in W} ran T (x)$
8		frgpnabl.u	$⊢ U = {var}_{FGrp} (I)$
9		frgpnabl.i	$⊢ φ \to I \in V$
10		frgpnabl.a	$⊢ φ \to A \in I$
11		frgpnabl.b	$⊢ φ \to B \in I$
12		frgpnabl.n	$⊢ φ \to U (A) \underset{˙}{+} U (B) = U (B) \underset{˙}{+} U (A)$
13		0ex	$⊢ \emptyset \in V$
14	13	a1i	$⊢ φ \to \emptyset \in V$
15		difss	$⊢ W ∖ ⋃_{x \in W} ran T (x) \subseteq W$
16	7 15	eqsstri	$⊢ D \subseteq W$
17	1 2 3 4 5 6 7 8 9 11 10	frgpnabllem1	$⊢ φ \to ⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩ \in (D \cap (U (B) \underset{˙}{+} U (A)))$
18	17	elin1d	$⊢ φ \to ⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩ \in D$
19	16 18	sselid	$⊢ φ \to ⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩ \in W$
20		eqid	$⊢ (m \in \{t \in (Word W ∖ \{\emptyset\}) \| (t (0) \in D \land \forall k \in (1 ..^\|t\|) t (k) \in ran T (t (k - 1)))\} ⟼ m (\|m\| - 1)) = (m \in \{t \in (Word W ∖ \{\emptyset\}) \| (t (0) \in D \land \forall k \in (1 ..^\|t\|) t (k) \in ran T (t (k - 1)))\} ⟼ m (\|m\| - 1))$
21	2 3 5 6 7 20	efgredeu	$⊢ ⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩ \in W \to \exists! d \in D d \underset{˙}{\sim} ⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩$
22		reurmo	$⊢ \exists! d \in D d \underset{˙}{\sim} ⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩ \to \exists^{*} d \in D d \underset{˙}{\sim} ⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩$
23	19 21 22	3syl	$⊢ φ \to \exists^{*} d \in D d \underset{˙}{\sim} ⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩$
24	1 2 3 4 5 6 7 8 9 10 11	frgpnabllem1	$⊢ φ \to ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in (D \cap (U (A) \underset{˙}{+} U (B)))$
25	24	elin1d	$⊢ φ \to ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in D$
26	2 3	efger	$⊢ \underset{˙}{\sim} Er W$
27	26	a1i	$⊢ φ \to \underset{˙}{\sim} Er W$
28	1	frgpgrp	$⊢ I \in V \to G \in Grp$
29	9 28	syl	$⊢ φ \to G \in Grp$
30		eqid	$⊢ {Base}_{G} = {Base}_{G}$
31	3 8 1 30	vrgpf	$⊢ I \in V \to U : I ⟶ {Base}_{G}$
32	9 31	syl	$⊢ φ \to U : I ⟶ {Base}_{G}$
33	32 10	ffvelcdmd	$⊢ φ \to U (A) \in {Base}_{G}$
34	32 11	ffvelcdmd	$⊢ φ \to U (B) \in {Base}_{G}$
35	30 4	grpcl	$⊢ (G \in Grp \land U (A) \in {Base}_{G} \land U (B) \in {Base}_{G}) \to U (A) \underset{˙}{+} U (B) \in {Base}_{G}$
36	29 33 34 35	syl3anc	$⊢ φ \to U (A) \underset{˙}{+} U (B) \in {Base}_{G}$
37		eqid	$⊢ freeMnd (I \times 2_{𝑜}) = freeMnd (I \times 2_{𝑜})$
38	1 37 3	frgpval	$⊢ I \in V \to G = freeMnd (I \times 2_{𝑜}) /_{𝑠} \underset{˙}{\sim}$
39	9 38	syl	$⊢ φ \to G = freeMnd (I \times 2_{𝑜}) /_{𝑠} \underset{˙}{\sim}$
40		2on	$⊢ 2_{𝑜} \in On$
41		xpexg	$⊢ (I \in V \land 2_{𝑜} \in On) \to I \times 2_{𝑜} \in V$
42	9 40 41	sylancl	$⊢ φ \to I \times 2_{𝑜} \in V$
43		wrdexg	$⊢ I \times 2_{𝑜} \in V \to Word (I \times 2_{𝑜}) \in V$
44		fvi	$⊢ Word (I \times 2_{𝑜}) \in V \to I (Word (I \times 2_{𝑜})) = Word (I \times 2_{𝑜})$
45	42 43 44	3syl	$⊢ φ \to I (Word (I \times 2_{𝑜})) = Word (I \times 2_{𝑜})$
46	2 45	eqtrid	$⊢ φ \to W = Word (I \times 2_{𝑜})$
47		eqid	$⊢ {Base}_{freeMnd (I \times 2_{𝑜})} = {Base}_{freeMnd (I \times 2_{𝑜})}$
48	37 47	frmdbas	$⊢ I \times 2_{𝑜} \in V \to {Base}_{freeMnd (I \times 2_{𝑜})} = Word (I \times 2_{𝑜})$
49	42 48	syl	$⊢ φ \to {Base}_{freeMnd (I \times 2_{𝑜})} = Word (I \times 2_{𝑜})$
50	46 49	eqtr4d	$⊢ φ \to W = {Base}_{freeMnd (I \times 2_{𝑜})}$
51	3	fvexi	$⊢ \underset{˙}{\sim} \in V$
52	51	a1i	$⊢ φ \to \underset{˙}{\sim} \in V$
53		fvexd	$⊢ φ \to freeMnd (I \times 2_{𝑜}) \in V$
54	39 50 52 53	qusbas	$⊢ φ \to W / \underset{˙}{\sim} = {Base}_{G}$
55	36 54	eleqtrrd	$⊢ φ \to U (A) \underset{˙}{+} U (B) \in (W / \underset{˙}{\sim})$
56	24	elin2d	$⊢ φ \to ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in (U (A) \underset{˙}{+} U (B))$
57		qsel	$⊢ (\underset{˙}{\sim} Er W \land U (A) \underset{˙}{+} U (B) \in (W / \underset{˙}{\sim}) \land ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in (U (A) \underset{˙}{+} U (B))) \to U (A) \underset{˙}{+} U (B) = [⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩] \underset{˙}{\sim}$
58	27 55 56 57	syl3anc	$⊢ φ \to U (A) \underset{˙}{+} U (B) = [⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩] \underset{˙}{\sim}$
59	17	elin2d	$⊢ φ \to ⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩ \in (U (B) \underset{˙}{+} U (A))$
60	59 12	eleqtrrd	$⊢ φ \to ⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩ \in (U (A) \underset{˙}{+} U (B))$
61		qsel	$⊢ (\underset{˙}{\sim} Er W \land U (A) \underset{˙}{+} U (B) \in (W / \underset{˙}{\sim}) \land ⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩ \in (U (A) \underset{˙}{+} U (B))) \to U (A) \underset{˙}{+} U (B) = [⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩] \underset{˙}{\sim}$
62	27 55 60 61	syl3anc	$⊢ φ \to U (A) \underset{˙}{+} U (B) = [⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩] \underset{˙}{\sim}$
63	58 62	eqtr3d	$⊢ φ \to [⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩] \underset{˙}{\sim} = [⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩] \underset{˙}{\sim}$
64	16 25	sselid	$⊢ φ \to ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in W$
65	27 64	erth	$⊢ φ \to (⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \underset{˙}{\sim} ⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩ \leftrightarrow [⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩] \underset{˙}{\sim} = [⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩] \underset{˙}{\sim})$
66	63 65	mpbird	$⊢ φ \to ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \underset{˙}{\sim} ⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩$
67	27 19	erref	$⊢ φ \to ⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩ \underset{˙}{\sim} ⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩$
68		breq1	$⊢ d = ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \to (d \underset{˙}{\sim} ⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩ \leftrightarrow ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \underset{˙}{\sim} ⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩)$
69		breq1	$⊢ d = ⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩ \to (d \underset{˙}{\sim} ⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩ \leftrightarrow ⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩ \underset{˙}{\sim} ⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩)$
70	68 69	rmoi	$⊢ (\exists^{*} d \in D d \underset{˙}{\sim} ⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩ \land (⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \in D \land ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ \underset{˙}{\sim} ⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩) \land (⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩ \in D \land ⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩ \underset{˙}{\sim} ⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩)) \to ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ = ⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩$
71	23 25 66 18 67 70	syl122anc	$⊢ φ \to ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ = ⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩$
72	71	fveq1d	$⊢ φ \to ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ (0) = ⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩ (0)$
73		opex	$⊢ ⟨A, \emptyset⟩ \in V$
74		s2fv0	$⊢ ⟨A, \emptyset⟩ \in V \to ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ (0) = ⟨A, \emptyset⟩$
75	73 74	ax-mp	$⊢ ⟨“ ⟨A, \emptyset⟩ ⟨B, \emptyset⟩ ”⟩ (0) = ⟨A, \emptyset⟩$
76		opex	$⊢ ⟨B, \emptyset⟩ \in V$
77		s2fv0	$⊢ ⟨B, \emptyset⟩ \in V \to ⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩ (0) = ⟨B, \emptyset⟩$
78	76 77	ax-mp	$⊢ ⟨“ ⟨B, \emptyset⟩ ⟨A, \emptyset⟩ ”⟩ (0) = ⟨B, \emptyset⟩$
79	72 75 78	3eqtr3g	$⊢ φ \to ⟨A, \emptyset⟩ = ⟨B, \emptyset⟩$
80		opthg	$⊢ (A \in I \land \emptyset \in V) \to (⟨A, \emptyset⟩ = ⟨B, \emptyset⟩ \leftrightarrow (A = B \land \emptyset = \emptyset))$
81	80	simprbda	$⊢ ((A \in I \land \emptyset \in V) \land ⟨A, \emptyset⟩ = ⟨B, \emptyset⟩) \to A = B$
82	10 14 79 81	syl21anc	$⊢ φ \to A = B$

Metamath Proof Explorer

Theorem frgpnabllem2

Proof