cycpmco2lem1

	Ref	Expression
Hypotheses	cycpmco2.c	$⊢ M = toCyc (D)$
	cycpmco2.s	$⊢ S = SymGrp (D)$
	cycpmco2.d	$⊢ φ \to D \in V$
	cycpmco2.w	$⊢ φ \to W \in dom M$
	cycpmco2.i	$⊢ φ \to I \in (D ∖ ran W)$
	cycpmco2.j	$⊢ φ \to J \in ran W$
	cycpmco2.e	$⊢ E = W^{-1} (J) + 1$
	cycpmco2.1	$⊢ U = W splice ⟨E, E, ⟨“ I ”⟩⟩$
Assertion	cycpmco2lem1	$⊢ φ \to M (W) (M (⟨“ I J ”⟩) (I)) = M (W) (J)$

Proof

Step	Hyp	Ref	Expression
1		cycpmco2.c	$⊢ M = toCyc (D)$
2		cycpmco2.s	$⊢ S = SymGrp (D)$
3		cycpmco2.d	$⊢ φ \to D \in V$
4		cycpmco2.w	$⊢ φ \to W \in dom M$
5		cycpmco2.i	$⊢ φ \to I \in (D ∖ ran W)$
6		cycpmco2.j	$⊢ φ \to J \in ran W$
7		cycpmco2.e	$⊢ E = W^{-1} (J) + 1$
8		cycpmco2.1	$⊢ U = W splice ⟨E, E, ⟨“ I ”⟩⟩$
9	5	eldifad	$⊢ φ \to I \in D$
10		ssrab2	$⊢ \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \subseteq Word D$
11		eqid	$⊢ {Base}_{S} = {Base}_{S}$
12	1 2 11	tocycf	$⊢ D \in V \to M : \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} ⟶ {Base}_{S}$
13	3 12	syl	$⊢ φ \to M : \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} ⟶ {Base}_{S}$
14	13	fdmd	$⊢ φ \to dom M = \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
15	4 14	eleqtrd	$⊢ φ \to W \in \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}$
16	10 15	sselid	$⊢ φ \to W \in Word D$
17		id	$⊢ w = W \to w = W$
18		dmeq	$⊢ w = W \to dom w = dom W$
19		eqidd	$⊢ w = W \to D = D$
20	17 18 19	f1eq123d	$⊢ w = W \to (w : dom w \underset{1-1}{⟶} D \leftrightarrow W : dom W \underset{1-1}{⟶} D)$
21	20	elrab3	$⊢ W \in Word D \to (W \in \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\} \leftrightarrow W : dom W \underset{1-1}{⟶} D)$
22	21	biimpa	$⊢ (W \in Word D \land W \in \{w \in Word D \| w : dom w \underset{1-1}{⟶} D\}) \to W : dom W \underset{1-1}{⟶} D$
23	16 15 22	syl2anc	$⊢ φ \to W : dom W \underset{1-1}{⟶} D$
24		f1f	$⊢ W : dom W \underset{1-1}{⟶} D \to W : dom W ⟶ D$
25	23 24	syl	$⊢ φ \to W : dom W ⟶ D$
26	25	frnd	$⊢ φ \to ran W \subseteq D$
27	26 6	sseldd	$⊢ φ \to J \in D$
28	5	eldifbd	$⊢ φ \to \neg I \in ran W$
29		nelne2	$⊢ (J \in ran W \land \neg I \in ran W) \to J \neq I$
30	6 28 29	syl2anc	$⊢ φ \to J \neq I$
31	30	necomd	$⊢ φ \to I \neq J$
32	1 3 9 27 31 2	cyc2fv1	$⊢ φ \to M (⟨“ I J ”⟩) (I) = J$
33	32	fveq2d	$⊢ φ \to M (W) (M (⟨“ I J ”⟩) (I)) = M (W) (J)$

Metamath Proof Explorer

Theorem cycpmco2lem1

Proof