vrgpinv

Description: The inverse of a generating element is represented by <. A , 1 >. instead of <. A , 0 >. . (Contributed by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	vrgpfval.r	$⊢ \underset{˙}{\sim} = ~_{FG} (I)$
	vrgpfval.u	$⊢ U = {var}_{FGrp} (I)$
	vrgpf.m	$⊢ G = freeGrp (I)$
	vrgpinv.n	$⊢ N = {inv}_{g} (G)$
Assertion	vrgpinv	$⊢ (I \in V \land A \in I) \to N (U (A)) = [⟨“ ⟨A, 1_{𝑜}⟩ ”⟩] \underset{˙}{\sim}$

Proof

Step	Hyp	Ref	Expression
1		vrgpfval.r	$⊢ \underset{˙}{\sim} = ~_{FG} (I)$
2		vrgpfval.u	$⊢ U = {var}_{FGrp} (I)$
3		vrgpf.m	$⊢ G = freeGrp (I)$
4		vrgpinv.n	$⊢ N = {inv}_{g} (G)$
5	1 2	vrgpval	$⊢ (I \in V \land A \in I) \to U (A) = [⟨“ ⟨A, \emptyset⟩ ”⟩] \underset{˙}{\sim}$
6	5	fveq2d	$⊢ (I \in V \land A \in I) \to N (U (A)) = N ([⟨“ ⟨A, \emptyset⟩ ”⟩] \underset{˙}{\sim})$
7		simpr	$⊢ (I \in V \land A \in I) \to A \in I$
8		0ex	$⊢ \emptyset \in V$
9	8	prid1	$⊢ \emptyset \in \{\emptyset, 1_{𝑜}\}$
10		df2o3	$⊢ 2_{𝑜} = \{\emptyset, 1_{𝑜}\}$
11	9 10	eleqtrri	$⊢ \emptyset \in 2_{𝑜}$
12		opelxpi	$⊢ (A \in I \land \emptyset \in 2_{𝑜}) \to ⟨A, \emptyset⟩ \in (I \times 2_{𝑜})$
13	7 11 12	sylancl	$⊢ (I \in V \land A \in I) \to ⟨A, \emptyset⟩ \in (I \times 2_{𝑜})$
14	13	s1cld	$⊢ (I \in V \land A \in I) \to ⟨“ ⟨A, \emptyset⟩ ”⟩ \in Word (I \times 2_{𝑜})$
15		simpl	$⊢ (I \in V \land A \in I) \to I \in V$
16		2on	$⊢ 2_{𝑜} \in On$
17		xpexg	$⊢ (I \in V \land 2_{𝑜} \in On) \to I \times 2_{𝑜} \in V$
18	15 16 17	sylancl	$⊢ (I \in V \land A \in I) \to I \times 2_{𝑜} \in V$
19		wrdexg	$⊢ I \times 2_{𝑜} \in V \to Word (I \times 2_{𝑜}) \in V$
20		fvi	$⊢ Word (I \times 2_{𝑜}) \in V \to I (Word (I \times 2_{𝑜})) = Word (I \times 2_{𝑜})$
21	18 19 20	3syl	$⊢ (I \in V \land A \in I) \to I (Word (I \times 2_{𝑜})) = Word (I \times 2_{𝑜})$
22	14 21	eleqtrrd	$⊢ (I \in V \land A \in I) \to ⟨“ ⟨A, \emptyset⟩ ”⟩ \in I (Word (I \times 2_{𝑜}))$
23		eqid	$⊢ I (Word (I \times 2_{𝑜})) = I (Word (I \times 2_{𝑜}))$
24		eqid	$⊢ (x \in I, y \in 2_{𝑜} ⟼ ⟨x, 1_{𝑜} ∖ y⟩) = (x \in I, y \in 2_{𝑜} ⟼ ⟨x, 1_{𝑜} ∖ y⟩)$
25	23 3 1 4 24	frgpinv	$⊢ ⟨“ ⟨A, \emptyset⟩ ”⟩ \in I (Word (I \times 2_{𝑜})) \to N ([⟨“ ⟨A, \emptyset⟩ ”⟩] \underset{˙}{\sim}) = [((x \in I, y \in 2_{𝑜} ⟼ ⟨x, 1_{𝑜} ∖ y⟩) \circ reverse (⟨“ ⟨A, \emptyset⟩ ”⟩))] \underset{˙}{\sim}$
26	22 25	syl	$⊢ (I \in V \land A \in I) \to N ([⟨“ ⟨A, \emptyset⟩ ”⟩] \underset{˙}{\sim}) = [((x \in I, y \in 2_{𝑜} ⟼ ⟨x, 1_{𝑜} ∖ y⟩) \circ reverse (⟨“ ⟨A, \emptyset⟩ ”⟩))] \underset{˙}{\sim}$
27		revs1	$⊢ reverse (⟨“ ⟨A, \emptyset⟩ ”⟩) = ⟨“ ⟨A, \emptyset⟩ ”⟩$
28	27	a1i	$⊢ (I \in V \land A \in I) \to reverse (⟨“ ⟨A, \emptyset⟩ ”⟩) = ⟨“ ⟨A, \emptyset⟩ ”⟩$
29	28	coeq2d	$⊢ (I \in V \land A \in I) \to (x \in I, y \in 2_{𝑜} ⟼ ⟨x, 1_{𝑜} ∖ y⟩) \circ reverse (⟨“ ⟨A, \emptyset⟩ ”⟩) = (x \in I, y \in 2_{𝑜} ⟼ ⟨x, 1_{𝑜} ∖ y⟩) \circ ⟨“ ⟨A, \emptyset⟩ ”⟩$
30	24	efgmf	$⊢ (x \in I, y \in 2_{𝑜} ⟼ ⟨x, 1_{𝑜} ∖ y⟩) : I \times 2_{𝑜} ⟶ I \times 2_{𝑜}$
31		s1co	$⊢ (⟨A, \emptyset⟩ \in (I \times 2_{𝑜}) \land (x \in I, y \in 2_{𝑜} ⟼ ⟨x, 1_{𝑜} ∖ y⟩) : I \times 2_{𝑜} ⟶ I \times 2_{𝑜}) \to (x \in I, y \in 2_{𝑜} ⟼ ⟨x, 1_{𝑜} ∖ y⟩) \circ ⟨“ ⟨A, \emptyset⟩ ”⟩ = ⟨“ (x \in I, y \in 2_{𝑜} ⟼ ⟨x, 1_{𝑜} ∖ y⟩) (⟨A, \emptyset⟩) ”⟩$
32	13 30 31	sylancl	$⊢ (I \in V \land A \in I) \to (x \in I, y \in 2_{𝑜} ⟼ ⟨x, 1_{𝑜} ∖ y⟩) \circ ⟨“ ⟨A, \emptyset⟩ ”⟩ = ⟨“ (x \in I, y \in 2_{𝑜} ⟼ ⟨x, 1_{𝑜} ∖ y⟩) (⟨A, \emptyset⟩) ”⟩$
33	24	efgmval	$⊢ (A \in I \land \emptyset \in 2_{𝑜}) \to A (x \in I, y \in 2_{𝑜} ⟼ ⟨x, 1_{𝑜} ∖ y⟩) \emptyset = ⟨A, 1_{𝑜} ∖ \emptyset⟩$
34	7 11 33	sylancl	$⊢ (I \in V \land A \in I) \to A (x \in I, y \in 2_{𝑜} ⟼ ⟨x, 1_{𝑜} ∖ y⟩) \emptyset = ⟨A, 1_{𝑜} ∖ \emptyset⟩$
35		df-ov	$⊢ A (x \in I, y \in 2_{𝑜} ⟼ ⟨x, 1_{𝑜} ∖ y⟩) \emptyset = (x \in I, y \in 2_{𝑜} ⟼ ⟨x, 1_{𝑜} ∖ y⟩) (⟨A, \emptyset⟩)$
36		dif0	$⊢ 1_{𝑜} ∖ \emptyset = 1_{𝑜}$
37	36	opeq2i	$⊢ ⟨A, 1_{𝑜} ∖ \emptyset⟩ = ⟨A, 1_{𝑜}⟩$
38	34 35 37	3eqtr3g	$⊢ (I \in V \land A \in I) \to (x \in I, y \in 2_{𝑜} ⟼ ⟨x, 1_{𝑜} ∖ y⟩) (⟨A, \emptyset⟩) = ⟨A, 1_{𝑜}⟩$
39	38	s1eqd	$⊢ (I \in V \land A \in I) \to ⟨“ (x \in I, y \in 2_{𝑜} ⟼ ⟨x, 1_{𝑜} ∖ y⟩) (⟨A, \emptyset⟩) ”⟩ = ⟨“ ⟨A, 1_{𝑜}⟩ ”⟩$
40	29 32 39	3eqtrd	$⊢ (I \in V \land A \in I) \to (x \in I, y \in 2_{𝑜} ⟼ ⟨x, 1_{𝑜} ∖ y⟩) \circ reverse (⟨“ ⟨A, \emptyset⟩ ”⟩) = ⟨“ ⟨A, 1_{𝑜}⟩ ”⟩$
41	40	eceq1d	$⊢ (I \in V \land A \in I) \to [((x \in I, y \in 2_{𝑜} ⟼ ⟨x, 1_{𝑜} ∖ y⟩) \circ reverse (⟨“ ⟨A, \emptyset⟩ ”⟩))] \underset{˙}{\sim} = [⟨“ ⟨A, 1_{𝑜}⟩ ”⟩] \underset{˙}{\sim}$
42	6 26 41	3eqtrd	$⊢ (I \in V \land A \in I) \to N (U (A)) = [⟨“ ⟨A, 1_{𝑜}⟩ ”⟩] \underset{˙}{\sim}$

Metamath Proof Explorer

Theorem vrgpinv

Proof