Metamath Proof Explorer

Theorem cycpmco2lem1

Description: Lemma for cycpmco2 . (Contributed by Thierry Arnoux, 4-Jan-2024)

Ref Expression
Hypotheses cycpmco2.c ⊢ M = toCyc ⁡ D
cycpmco2.s ⊢ S = SymGrp ⁡ D
cycpmco2.d ⊢ φ → D ∈ V
cycpmco2.w ⊢ φ → W ∈ dom ⁡ M
cycpmco2.i ⊢ φ → I ∈ D ∖ ran ⁡ W
cycpmco2.j ⊢ φ → J ∈ ran ⁡ W
cycpmco2.e ⊢ E = W -1 ⁡ J + 1
cycpmco2.1 ⊢ U = W splice E E ⟨“ I ”⟩
Assertion cycpmco2lem1 ⊢ φ → M ⁡ W ⁡ M ⁡ ⟨“ IJ ”⟩ ⁡ I = M ⁡ W ⁡ J

Proof

Step Hyp Ref Expression
1 cycpmco2.c ⊢ M = toCyc ⁡ D
2 cycpmco2.s ⊢ S = SymGrp ⁡ D
3 cycpmco2.d ⊢ φ → D ∈ V
4 cycpmco2.w ⊢ φ → W ∈ dom ⁡ M
5 cycpmco2.i ⊢ φ → I ∈ D ∖ ran ⁡ W
6 cycpmco2.j ⊢ φ → J ∈ ran ⁡ W
7 cycpmco2.e ⊢ E = W -1 ⁡ J + 1
8 cycpmco2.1 ⊢ U = W splice E E ⟨“ I ”⟩
9 5 eldifad ⊢ φ → I ∈ D
10 ssrab2 ⊢ w ∈ Word D | w : dom ⁡ w ⟶ 1-1 D ⊆ Word D
11 eqid ⊢ Base S = Base S
12 1 2 11 tocycf ⊢ D ∈ V → M : w ∈ Word D | w : dom ⁡ w ⟶ 1-1 D ⟶ Base S
13 3 12 syl ⊢ φ → M : w ∈ Word D | w : dom ⁡ w ⟶ 1-1 D ⟶ Base S
14 13 fdmd ⊢ φ → dom ⁡ M = w ∈ Word D | w : dom ⁡ w ⟶ 1-1 D
15 4 14 eleqtrd ⊢ φ → W ∈ w ∈ Word D | w : dom ⁡ w ⟶ 1-1 D
16 10 15 sselid ⊢ φ → W ∈ Word D
17 id ⊢ w = W → w = W
18 dmeq ⊢ w = W → dom ⁡ w = dom ⁡ W
19 eqidd ⊢ w = W → D = D
20 17 18 19 f1eq123d ⊢ w = W → w : dom ⁡ w ⟶ 1-1 D ↔ W : dom ⁡ W ⟶ 1-1 D
21 20 elrab3 ⊢ W ∈ Word D → W ∈ w ∈ Word D | w : dom ⁡ w ⟶ 1-1 D ↔ W : dom ⁡ W ⟶ 1-1 D
22 21 biimpa ⊢ W ∈ Word D ∧ W ∈ w ∈ Word D | w : dom ⁡ w ⟶ 1-1 D → W : dom ⁡ W ⟶ 1-1 D
23 16 15 22 syl2anc ⊢ φ → W : dom ⁡ W ⟶ 1-1 D
24 f1f ⊢ W : dom ⁡ W ⟶ 1-1 D → W : dom ⁡ W ⟶ D
25 23 24 syl ⊢ φ → W : dom ⁡ W ⟶ D
26 25 frnd ⊢ φ → ran ⁡ W ⊆ D
27 26 6 sseldd ⊢ φ → J ∈ D
28 5 eldifbd ⊢ φ → ¬ I ∈ ran ⁡ W
29 nelne2 ⊢ J ∈ ran ⁡ W ∧ ¬ I ∈ ran ⁡ W → J ≠ I
30 6 28 29 syl2anc ⊢ φ → J ≠ I
31 30 necomd ⊢ φ → I ≠ J
32 1 3 9 27 31 2 cyc2fv1 ⊢ φ → M ⁡ ⟨“ IJ ”⟩ ⁡ I = J
33 32 fveq2d ⊢ φ → M ⁡ W ⁡ M ⁡ ⟨“ IJ ”⟩ ⁡ I = M ⁡ W ⁡ J