efgmnvl

Description: The inversion function on the generators is an involution. (Contributed by Mario Carneiro, 1-Oct-2015)

		Ref	Expression
	Hypothesis	efgmval.m	$⊢ M = (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩)$
	Assertion	efgmnvl	$⊢ A \in (I \times 2_{𝑜}) \to M (M (A)) = A$

Proof

Step	Hyp	Ref	Expression
1		efgmval.m	$⊢ M = (y \in I, z \in 2_{𝑜} ⟼ ⟨y, 1_{𝑜} ∖ z⟩)$
2		elxp2	$⊢ A \in (I \times 2_{𝑜}) \leftrightarrow \exists a \in I \exists b \in 2_{𝑜} A = ⟨a, b⟩$
3	1	efgmval	$⊢ (a \in I \land b \in 2_{𝑜}) \to a M b = ⟨a, 1_{𝑜} ∖ b⟩$
4	3	fveq2d	$⊢ (a \in I \land b \in 2_{𝑜}) \to M (a M b) = M (⟨a, 1_{𝑜} ∖ b⟩)$
5		df-ov	$⊢ a M (1_{𝑜} ∖ b) = M (⟨a, 1_{𝑜} ∖ b⟩)$
6	4 5	eqtr4di	$⊢ (a \in I \land b \in 2_{𝑜}) \to M (a M b) = a M (1_{𝑜} ∖ b)$
7		2oconcl	$⊢ b \in 2_{𝑜} \to 1_{𝑜} ∖ b \in 2_{𝑜}$
8	1	efgmval	$⊢ (a \in I \land 1_{𝑜} ∖ b \in 2_{𝑜}) \to a M (1_{𝑜} ∖ b) = ⟨a, 1_{𝑜} ∖ (1_{𝑜} ∖ b)⟩$
9	7 8	sylan2	$⊢ (a \in I \land b \in 2_{𝑜}) \to a M (1_{𝑜} ∖ b) = ⟨a, 1_{𝑜} ∖ (1_{𝑜} ∖ b)⟩$
10		1on	$⊢ 1_{𝑜} \in On$
11	10	onordi	$⊢ Ord 1_{𝑜}$
12		ordtr	$⊢ Ord 1_{𝑜} \to Tr 1_{𝑜}$
13		trsucss	$⊢ Tr 1_{𝑜} \to (b \in suc 1_{𝑜} \to b \subseteq 1_{𝑜})$
14	11 12 13	mp2b	$⊢ b \in suc 1_{𝑜} \to b \subseteq 1_{𝑜}$
15		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
16	14 15	eleq2s	$⊢ b \in 2_{𝑜} \to b \subseteq 1_{𝑜}$
17	16	adantl	$⊢ (a \in I \land b \in 2_{𝑜}) \to b \subseteq 1_{𝑜}$
18		dfss4	$⊢ b \subseteq 1_{𝑜} \leftrightarrow 1_{𝑜} ∖ (1_{𝑜} ∖ b) = b$
19	17 18	sylib	$⊢ (a \in I \land b \in 2_{𝑜}) \to 1_{𝑜} ∖ (1_{𝑜} ∖ b) = b$
20	19	opeq2d	$⊢ (a \in I \land b \in 2_{𝑜}) \to ⟨a, 1_{𝑜} ∖ (1_{𝑜} ∖ b)⟩ = ⟨a, b⟩$
21	6 9 20	3eqtrd	$⊢ (a \in I \land b \in 2_{𝑜}) \to M (a M b) = ⟨a, b⟩$
22		fveq2	$⊢ A = ⟨a, b⟩ \to M (A) = M (⟨a, b⟩)$
23		df-ov	$⊢ a M b = M (⟨a, b⟩)$
24	22 23	eqtr4di	$⊢ A = ⟨a, b⟩ \to M (A) = a M b$
25	24	fveq2d	$⊢ A = ⟨a, b⟩ \to M (M (A)) = M (a M b)$
26		id	$⊢ A = ⟨a, b⟩ \to A = ⟨a, b⟩$
27	25 26	eqeq12d	$⊢ A = ⟨a, b⟩ \to (M (M (A)) = A \leftrightarrow M (a M b) = ⟨a, b⟩)$
28	21 27	syl5ibrcom	$⊢ (a \in I \land b \in 2_{𝑜}) \to (A = ⟨a, b⟩ \to M (M (A)) = A)$
29	28	rexlimivv	$⊢ \exists a \in I \exists b \in 2_{𝑜} A = ⟨a, b⟩ \to M (M (A)) = A$
30	2 29	sylbi	$⊢ A \in (I \times 2_{𝑜}) \to M (M (A)) = A$

Metamath Proof Explorer

Theorem efgmnvl

Proof