| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | frgpup3.k | . . 3
⊢ (𝜑 → 𝐾 ∈ (𝐺 GrpHom 𝐻)) | 
| 2 |  | frgpup.x | . . . 4
⊢ 𝑋 = (Base‘𝐺) | 
| 3 |  | frgpup.b | . . . 4
⊢ 𝐵 = (Base‘𝐻) | 
| 4 | 2, 3 | ghmf 19239 | . . 3
⊢ (𝐾 ∈ (𝐺 GrpHom 𝐻) → 𝐾:𝑋⟶𝐵) | 
| 5 |  | ffn 6735 | . . 3
⊢ (𝐾:𝑋⟶𝐵 → 𝐾 Fn 𝑋) | 
| 6 | 1, 4, 5 | 3syl 18 | . 2
⊢ (𝜑 → 𝐾 Fn 𝑋) | 
| 7 |  | frgpup.n | . . . 4
⊢ 𝑁 = (invg‘𝐻) | 
| 8 |  | frgpup.t | . . . 4
⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦)))) | 
| 9 |  | frgpup.h | . . . 4
⊢ (𝜑 → 𝐻 ∈ Grp) | 
| 10 |  | frgpup.i | . . . 4
⊢ (𝜑 → 𝐼 ∈ 𝑉) | 
| 11 |  | frgpup.a | . . . 4
⊢ (𝜑 → 𝐹:𝐼⟶𝐵) | 
| 12 |  | frgpup.w | . . . 4
⊢ 𝑊 = ( I ‘Word (𝐼 ×
2o)) | 
| 13 |  | frgpup.r | . . . 4
⊢  ∼ = (
~FG ‘𝐼) | 
| 14 |  | frgpup.g | . . . 4
⊢ 𝐺 = (freeGrp‘𝐼) | 
| 15 |  | frgpup.e | . . . 4
⊢ 𝐸 = ran (𝑔 ∈ 𝑊 ↦ 〈[𝑔] ∼ , (𝐻 Σg
(𝑇 ∘ 𝑔))〉) | 
| 16 | 3, 7, 8, 9, 10, 11, 12, 13, 14, 2, 15 | frgpup1 19794 | . . 3
⊢ (𝜑 → 𝐸 ∈ (𝐺 GrpHom 𝐻)) | 
| 17 | 2, 3 | ghmf 19239 | . . 3
⊢ (𝐸 ∈ (𝐺 GrpHom 𝐻) → 𝐸:𝑋⟶𝐵) | 
| 18 |  | ffn 6735 | . . 3
⊢ (𝐸:𝑋⟶𝐵 → 𝐸 Fn 𝑋) | 
| 19 | 16, 17, 18 | 3syl 18 | . 2
⊢ (𝜑 → 𝐸 Fn 𝑋) | 
| 20 |  | eqid 2736 | . . . . . . . . 9
⊢
(freeMnd‘(𝐼
× 2o)) = (freeMnd‘(𝐼 × 2o)) | 
| 21 | 14, 20, 13 | frgpval 19777 | . . . . . . . 8
⊢ (𝐼 ∈ 𝑉 → 𝐺 = ((freeMnd‘(𝐼 × 2o))
/s ∼ )) | 
| 22 | 10, 21 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝐺 = ((freeMnd‘(𝐼 × 2o))
/s ∼ )) | 
| 23 |  | 2on 8521 | . . . . . . . . . . 11
⊢
2o ∈ On | 
| 24 |  | xpexg 7771 | . . . . . . . . . . 11
⊢ ((𝐼 ∈ 𝑉 ∧ 2o ∈ On) →
(𝐼 × 2o)
∈ V) | 
| 25 | 10, 23, 24 | sylancl 586 | . . . . . . . . . 10
⊢ (𝜑 → (𝐼 × 2o) ∈
V) | 
| 26 |  | wrdexg 14563 | . . . . . . . . . 10
⊢ ((𝐼 × 2o) ∈ V
→ Word (𝐼 ×
2o) ∈ V) | 
| 27 |  | fvi 6984 | . . . . . . . . . 10
⊢ (Word
(𝐼 × 2o)
∈ V → ( I ‘Word (𝐼 × 2o)) = Word (𝐼 ×
2o)) | 
| 28 | 25, 26, 27 | 3syl 18 | . . . . . . . . 9
⊢ (𝜑 → ( I ‘Word (𝐼 × 2o)) = Word
(𝐼 ×
2o)) | 
| 29 | 12, 28 | eqtrid 2788 | . . . . . . . 8
⊢ (𝜑 → 𝑊 = Word (𝐼 × 2o)) | 
| 30 |  | eqid 2736 | . . . . . . . . . 10
⊢
(Base‘(freeMnd‘(𝐼 × 2o))) =
(Base‘(freeMnd‘(𝐼 × 2o))) | 
| 31 | 20, 30 | frmdbas 18866 | . . . . . . . . 9
⊢ ((𝐼 × 2o) ∈ V
→ (Base‘(freeMnd‘(𝐼 × 2o))) = Word (𝐼 ×
2o)) | 
| 32 | 25, 31 | syl 17 | . . . . . . . 8
⊢ (𝜑 →
(Base‘(freeMnd‘(𝐼 × 2o))) = Word (𝐼 ×
2o)) | 
| 33 | 29, 32 | eqtr4d 2779 | . . . . . . 7
⊢ (𝜑 → 𝑊 = (Base‘(freeMnd‘(𝐼 ×
2o)))) | 
| 34 | 13 | fvexi 6919 | . . . . . . . 8
⊢  ∼ ∈
V | 
| 35 | 34 | a1i 11 | . . . . . . 7
⊢ (𝜑 → ∼ ∈
V) | 
| 36 |  | fvexd 6920 | . . . . . . 7
⊢ (𝜑 → (freeMnd‘(𝐼 × 2o)) ∈
V) | 
| 37 | 22, 33, 35, 36 | qusbas 17591 | . . . . . 6
⊢ (𝜑 → (𝑊 / ∼ ) =
(Base‘𝐺)) | 
| 38 | 2, 37 | eqtr4id 2795 | . . . . 5
⊢ (𝜑 → 𝑋 = (𝑊 / ∼ )) | 
| 39 |  | eqimss 4041 | . . . . 5
⊢ (𝑋 = (𝑊 / ∼ ) → 𝑋 ⊆ (𝑊 / ∼ )) | 
| 40 | 38, 39 | syl 17 | . . . 4
⊢ (𝜑 → 𝑋 ⊆ (𝑊 / ∼ )) | 
| 41 | 40 | sselda 3982 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑋) → 𝑎 ∈ (𝑊 / ∼ )) | 
| 42 |  | eqid 2736 | . . . 4
⊢ (𝑊 / ∼ ) = (𝑊 / ∼ ) | 
| 43 |  | fveq2 6905 | . . . . 5
⊢ ([𝑡] ∼ = 𝑎 → (𝐾‘[𝑡] ∼ ) = (𝐾‘𝑎)) | 
| 44 |  | fveq2 6905 | . . . . 5
⊢ ([𝑡] ∼ = 𝑎 → (𝐸‘[𝑡] ∼ ) = (𝐸‘𝑎)) | 
| 45 | 43, 44 | eqeq12d 2752 | . . . 4
⊢ ([𝑡] ∼ = 𝑎 → ((𝐾‘[𝑡] ∼ ) = (𝐸‘[𝑡] ∼ ) ↔ (𝐾‘𝑎) = (𝐸‘𝑎))) | 
| 46 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → 𝑡 ∈ 𝑊) | 
| 47 | 29 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → 𝑊 = Word (𝐼 × 2o)) | 
| 48 | 46, 47 | eleqtrd 2842 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → 𝑡 ∈ Word (𝐼 × 2o)) | 
| 49 |  | wrdf 14558 | . . . . . . . . . . . . 13
⊢ (𝑡 ∈ Word (𝐼 × 2o) → 𝑡:(0..^(♯‘𝑡))⟶(𝐼 × 2o)) | 
| 50 | 48, 49 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → 𝑡:(0..^(♯‘𝑡))⟶(𝐼 × 2o)) | 
| 51 | 50 | ffvelcdmda 7103 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → (𝑡‘𝑛) ∈ (𝐼 × 2o)) | 
| 52 |  | elxp2 5708 | . . . . . . . . . . 11
⊢ ((𝑡‘𝑛) ∈ (𝐼 × 2o) ↔ ∃𝑖 ∈ 𝐼 ∃𝑗 ∈ 2o (𝑡‘𝑛) = 〈𝑖, 𝑗〉) | 
| 53 | 51, 52 | sylib 218 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → ∃𝑖 ∈ 𝐼 ∃𝑗 ∈ 2o (𝑡‘𝑛) = 〈𝑖, 𝑗〉) | 
| 54 |  | fveq2 6905 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑖 → (𝐹‘𝑦) = (𝐹‘𝑖)) | 
| 55 | 54 | fveq2d 6909 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑖 → (𝑁‘(𝐹‘𝑦)) = (𝑁‘(𝐹‘𝑖))) | 
| 56 | 54, 55 | ifeq12d 4546 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑖 → if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦))) = if(𝑧 = ∅, (𝐹‘𝑖), (𝑁‘(𝐹‘𝑖)))) | 
| 57 |  | eqeq1 2740 | . . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑗 → (𝑧 = ∅ ↔ 𝑗 = ∅)) | 
| 58 | 57 | ifbid 4548 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑗 → if(𝑧 = ∅, (𝐹‘𝑖), (𝑁‘(𝐹‘𝑖))) = if(𝑗 = ∅, (𝐹‘𝑖), (𝑁‘(𝐹‘𝑖)))) | 
| 59 |  | fvex 6918 | . . . . . . . . . . . . . . . . 17
⊢ (𝐹‘𝑖) ∈ V | 
| 60 |  | fvex 6918 | . . . . . . . . . . . . . . . . 17
⊢ (𝑁‘(𝐹‘𝑖)) ∈ V | 
| 61 | 59, 60 | ifex 4575 | . . . . . . . . . . . . . . . 16
⊢ if(𝑗 = ∅, (𝐹‘𝑖), (𝑁‘(𝐹‘𝑖))) ∈ V | 
| 62 | 56, 58, 8, 61 | ovmpo 7594 | . . . . . . . . . . . . . . 15
⊢ ((𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 2o) → (𝑖𝑇𝑗) = if(𝑗 = ∅, (𝐹‘𝑖), (𝑁‘(𝐹‘𝑖)))) | 
| 63 | 62 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 2o)) → (𝑖𝑇𝑗) = if(𝑗 = ∅, (𝐹‘𝑖), (𝑁‘(𝐹‘𝑖)))) | 
| 64 |  | elpri 4648 | . . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ {∅, 1o}
→ (𝑗 = ∅ ∨
𝑗 =
1o)) | 
| 65 |  | df2o3 8515 | . . . . . . . . . . . . . . . . 17
⊢
2o = {∅, 1o} | 
| 66 | 64, 65 | eleq2s 2858 | . . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ 2o →
(𝑗 = ∅ ∨ 𝑗 =
1o)) | 
| 67 |  | frgpup3.e | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐾 ∘ 𝑈) = 𝐹) | 
| 68 | 67 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝐾 ∘ 𝑈) = 𝐹) | 
| 69 | 68 | fveq1d 6907 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → ((𝐾 ∘ 𝑈)‘𝑖) = (𝐹‘𝑖)) | 
| 70 |  | frgpup.u | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑈 =
(varFGrp‘𝐼) | 
| 71 | 13, 70, 14, 2 | vrgpf 19787 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐼 ∈ 𝑉 → 𝑈:𝐼⟶𝑋) | 
| 72 | 10, 71 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝑈:𝐼⟶𝑋) | 
| 73 |  | fvco3 7007 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑈:𝐼⟶𝑋 ∧ 𝑖 ∈ 𝐼) → ((𝐾 ∘ 𝑈)‘𝑖) = (𝐾‘(𝑈‘𝑖))) | 
| 74 | 72, 73 | sylan 580 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → ((𝐾 ∘ 𝑈)‘𝑖) = (𝐾‘(𝑈‘𝑖))) | 
| 75 | 69, 74 | eqtr3d 2778 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝐹‘𝑖) = (𝐾‘(𝑈‘𝑖))) | 
| 76 | 75 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = ∅) → (𝐹‘𝑖) = (𝐾‘(𝑈‘𝑖))) | 
| 77 |  | iftrue 4530 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 = ∅ → if(𝑗 = ∅, (𝐹‘𝑖), (𝑁‘(𝐹‘𝑖))) = (𝐹‘𝑖)) | 
| 78 | 77 | adantl 481 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = ∅) → if(𝑗 = ∅, (𝐹‘𝑖), (𝑁‘(𝐹‘𝑖))) = (𝐹‘𝑖)) | 
| 79 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = ∅) → 𝑗 = ∅) | 
| 80 | 79 | opeq2d 4879 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = ∅) → 〈𝑖, 𝑗〉 = 〈𝑖, ∅〉) | 
| 81 | 80 | s1eqd 14640 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = ∅) → 〈“〈𝑖, 𝑗〉”〉 =
〈“〈𝑖,
∅〉”〉) | 
| 82 | 81 | eceq1d 8786 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = ∅) → [〈“〈𝑖, 𝑗〉”〉] ∼ =
[〈“〈𝑖,
∅〉”〉] ∼ ) | 
| 83 | 13, 70 | vrgpval 19786 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑖 ∈ 𝐼) → (𝑈‘𝑖) = [〈“〈𝑖, ∅〉”〉] ∼
) | 
| 84 | 10, 83 | sylan 580 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝑈‘𝑖) = [〈“〈𝑖, ∅〉”〉] ∼
) | 
| 85 | 84 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = ∅) → (𝑈‘𝑖) = [〈“〈𝑖, ∅〉”〉] ∼
) | 
| 86 | 82, 85 | eqtr4d 2779 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = ∅) → [〈“〈𝑖, 𝑗〉”〉] ∼ = (𝑈‘𝑖)) | 
| 87 | 86 | fveq2d 6909 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = ∅) → (𝐾‘[〈“〈𝑖, 𝑗〉”〉] ∼ ) = (𝐾‘(𝑈‘𝑖))) | 
| 88 | 76, 78, 87 | 3eqtr4d 2786 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = ∅) → if(𝑗 = ∅, (𝐹‘𝑖), (𝑁‘(𝐹‘𝑖))) = (𝐾‘[〈“〈𝑖, 𝑗〉”〉] ∼ )) | 
| 89 | 75 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝑁‘(𝐹‘𝑖)) = (𝑁‘(𝐾‘(𝑈‘𝑖)))) | 
| 90 | 72 | ffvelcdmda 7103 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝑈‘𝑖) ∈ 𝑋) | 
| 91 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(invg‘𝐺) = (invg‘𝐺) | 
| 92 | 2, 91, 7 | ghminv 19242 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐾 ∈ (𝐺 GrpHom 𝐻) ∧ (𝑈‘𝑖) ∈ 𝑋) → (𝐾‘((invg‘𝐺)‘(𝑈‘𝑖))) = (𝑁‘(𝐾‘(𝑈‘𝑖)))) | 
| 93 | 1, 90, 92 | syl2an2r 685 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝐾‘((invg‘𝐺)‘(𝑈‘𝑖))) = (𝑁‘(𝐾‘(𝑈‘𝑖)))) | 
| 94 | 89, 93 | eqtr4d 2779 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → (𝑁‘(𝐹‘𝑖)) = (𝐾‘((invg‘𝐺)‘(𝑈‘𝑖)))) | 
| 95 | 94 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = 1o) → (𝑁‘(𝐹‘𝑖)) = (𝐾‘((invg‘𝐺)‘(𝑈‘𝑖)))) | 
| 96 |  | 1n0 8527 | . . . . . . . . . . . . . . . . . . . 20
⊢
1o ≠ ∅ | 
| 97 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = 1o) → 𝑗 = 1o) | 
| 98 | 97 | neeq1d 2999 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = 1o) → (𝑗 ≠ ∅ ↔ 1o ≠
∅)) | 
| 99 | 96, 98 | mpbiri 258 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = 1o) → 𝑗 ≠ ∅) | 
| 100 |  | ifnefalse 4536 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ≠ ∅ → if(𝑗 = ∅, (𝐹‘𝑖), (𝑁‘(𝐹‘𝑖))) = (𝑁‘(𝐹‘𝑖))) | 
| 101 | 99, 100 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = 1o) → if(𝑗 = ∅, (𝐹‘𝑖), (𝑁‘(𝐹‘𝑖))) = (𝑁‘(𝐹‘𝑖))) | 
| 102 | 97 | opeq2d 4879 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = 1o) → 〈𝑖, 𝑗〉 = 〈𝑖, 1o〉) | 
| 103 | 102 | s1eqd 14640 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = 1o) →
〈“〈𝑖, 𝑗〉”〉 =
〈“〈𝑖,
1o〉”〉) | 
| 104 | 103 | eceq1d 8786 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = 1o) →
[〈“〈𝑖,
𝑗〉”〉] ∼ =
[〈“〈𝑖,
1o〉”〉] ∼ ) | 
| 105 | 13, 70, 14, 91 | vrgpinv 19788 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑖 ∈ 𝐼) → ((invg‘𝐺)‘(𝑈‘𝑖)) = [〈“〈𝑖, 1o〉”〉] ∼
) | 
| 106 | 10, 105 | sylan 580 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → ((invg‘𝐺)‘(𝑈‘𝑖)) = [〈“〈𝑖, 1o〉”〉] ∼
) | 
| 107 | 106 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = 1o) →
((invg‘𝐺)‘(𝑈‘𝑖)) = [〈“〈𝑖, 1o〉”〉] ∼
) | 
| 108 | 104, 107 | eqtr4d 2779 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = 1o) →
[〈“〈𝑖,
𝑗〉”〉] ∼ =
((invg‘𝐺)‘(𝑈‘𝑖))) | 
| 109 | 108 | fveq2d 6909 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = 1o) → (𝐾‘[〈“〈𝑖, 𝑗〉”〉] ∼ ) = (𝐾‘((invg‘𝐺)‘(𝑈‘𝑖)))) | 
| 110 | 95, 101, 109 | 3eqtr4d 2786 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 = 1o) → if(𝑗 = ∅, (𝐹‘𝑖), (𝑁‘(𝐹‘𝑖))) = (𝐾‘[〈“〈𝑖, 𝑗〉”〉] ∼ )) | 
| 111 | 88, 110 | jaodan 959 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ (𝑗 = ∅ ∨ 𝑗 = 1o)) → if(𝑗 = ∅, (𝐹‘𝑖), (𝑁‘(𝐹‘𝑖))) = (𝐾‘[〈“〈𝑖, 𝑗〉”〉] ∼ )) | 
| 112 | 66, 111 | sylan2 593 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑗 ∈ 2o) → if(𝑗 = ∅, (𝐹‘𝑖), (𝑁‘(𝐹‘𝑖))) = (𝐾‘[〈“〈𝑖, 𝑗〉”〉] ∼ )) | 
| 113 | 112 | anasss 466 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 2o)) → if(𝑗 = ∅, (𝐹‘𝑖), (𝑁‘(𝐹‘𝑖))) = (𝐾‘[〈“〈𝑖, 𝑗〉”〉] ∼ )) | 
| 114 | 63, 113 | eqtrd 2776 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 2o)) → (𝑖𝑇𝑗) = (𝐾‘[〈“〈𝑖, 𝑗〉”〉] ∼ )) | 
| 115 |  | fveq2 6905 | . . . . . . . . . . . . . . 15
⊢ ((𝑡‘𝑛) = 〈𝑖, 𝑗〉 → (𝑇‘(𝑡‘𝑛)) = (𝑇‘〈𝑖, 𝑗〉)) | 
| 116 |  | df-ov 7435 | . . . . . . . . . . . . . . 15
⊢ (𝑖𝑇𝑗) = (𝑇‘〈𝑖, 𝑗〉) | 
| 117 | 115, 116 | eqtr4di 2794 | . . . . . . . . . . . . . 14
⊢ ((𝑡‘𝑛) = 〈𝑖, 𝑗〉 → (𝑇‘(𝑡‘𝑛)) = (𝑖𝑇𝑗)) | 
| 118 |  | s1eq 14639 | . . . . . . . . . . . . . . . 16
⊢ ((𝑡‘𝑛) = 〈𝑖, 𝑗〉 → 〈“(𝑡‘𝑛)”〉 = 〈“〈𝑖, 𝑗〉”〉) | 
| 119 | 118 | eceq1d 8786 | . . . . . . . . . . . . . . 15
⊢ ((𝑡‘𝑛) = 〈𝑖, 𝑗〉 → [〈“(𝑡‘𝑛)”〉] ∼ =
[〈“〈𝑖,
𝑗〉”〉] ∼
) | 
| 120 | 119 | fveq2d 6909 | . . . . . . . . . . . . . 14
⊢ ((𝑡‘𝑛) = 〈𝑖, 𝑗〉 → (𝐾‘[〈“(𝑡‘𝑛)”〉] ∼ ) = (𝐾‘[〈“〈𝑖, 𝑗〉”〉] ∼ )) | 
| 121 | 117, 120 | eqeq12d 2752 | . . . . . . . . . . . . 13
⊢ ((𝑡‘𝑛) = 〈𝑖, 𝑗〉 → ((𝑇‘(𝑡‘𝑛)) = (𝐾‘[〈“(𝑡‘𝑛)”〉] ∼ ) ↔ (𝑖𝑇𝑗) = (𝐾‘[〈“〈𝑖, 𝑗〉”〉] ∼
))) | 
| 122 | 114, 121 | syl5ibrcom 247 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 2o)) → ((𝑡‘𝑛) = 〈𝑖, 𝑗〉 → (𝑇‘(𝑡‘𝑛)) = (𝐾‘[〈“(𝑡‘𝑛)”〉] ∼
))) | 
| 123 | 122 | rexlimdvva 3212 | . . . . . . . . . . 11
⊢ (𝜑 → (∃𝑖 ∈ 𝐼 ∃𝑗 ∈ 2o (𝑡‘𝑛) = 〈𝑖, 𝑗〉 → (𝑇‘(𝑡‘𝑛)) = (𝐾‘[〈“(𝑡‘𝑛)”〉] ∼
))) | 
| 124 | 123 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → (∃𝑖 ∈ 𝐼 ∃𝑗 ∈ 2o (𝑡‘𝑛) = 〈𝑖, 𝑗〉 → (𝑇‘(𝑡‘𝑛)) = (𝐾‘[〈“(𝑡‘𝑛)”〉] ∼
))) | 
| 125 | 53, 124 | mpd 15 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → (𝑇‘(𝑡‘𝑛)) = (𝐾‘[〈“(𝑡‘𝑛)”〉] ∼ )) | 
| 126 | 125 | mpteq2dva 5241 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝑇‘(𝑡‘𝑛))) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝐾‘[〈“(𝑡‘𝑛)”〉] ∼
))) | 
| 127 | 3, 7, 8, 9, 10, 11 | frgpuptf 19789 | . . . . . . . . 9
⊢ (𝜑 → 𝑇:(𝐼 × 2o)⟶𝐵) | 
| 128 |  | fcompt 7152 | . . . . . . . . 9
⊢ ((𝑇:(𝐼 × 2o)⟶𝐵 ∧ 𝑡:(0..^(♯‘𝑡))⟶(𝐼 × 2o)) → (𝑇 ∘ 𝑡) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝑇‘(𝑡‘𝑛)))) | 
| 129 | 127, 50, 128 | syl2an2r 685 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝑇 ∘ 𝑡) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝑇‘(𝑡‘𝑛)))) | 
| 130 | 51 | s1cld 14642 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → 〈“(𝑡‘𝑛)”〉 ∈ Word (𝐼 × 2o)) | 
| 131 | 29 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → 𝑊 = Word (𝐼 × 2o)) | 
| 132 | 130, 131 | eleqtrrd 2843 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → 〈“(𝑡‘𝑛)”〉 ∈ 𝑊) | 
| 133 | 14, 13, 12, 2 | frgpeccl 19780 | . . . . . . . . . 10
⊢
(〈“(𝑡‘𝑛)”〉 ∈ 𝑊 → [〈“(𝑡‘𝑛)”〉] ∼ ∈ 𝑋) | 
| 134 | 132, 133 | syl 17 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑊) ∧ 𝑛 ∈ (0..^(♯‘𝑡))) → [〈“(𝑡‘𝑛)”〉] ∼ ∈ 𝑋) | 
| 135 | 50 | feqmptd 6976 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → 𝑡 = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝑡‘𝑛))) | 
| 136 | 10 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → 𝐼 ∈ 𝑉) | 
| 137 | 136, 23, 24 | sylancl 586 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝐼 × 2o) ∈
V) | 
| 138 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(varFMnd‘(𝐼 × 2o)) =
(varFMnd‘(𝐼 × 2o)) | 
| 139 | 138 | vrmdfval 18870 | . . . . . . . . . . . 12
⊢ ((𝐼 × 2o) ∈ V
→ (varFMnd‘(𝐼 × 2o)) = (𝑤 ∈ (𝐼 × 2o) ↦
〈“𝑤”〉)) | 
| 140 | 137, 139 | syl 17 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) →
(varFMnd‘(𝐼 × 2o)) = (𝑤 ∈ (𝐼 × 2o) ↦
〈“𝑤”〉)) | 
| 141 |  | s1eq 14639 | . . . . . . . . . . 11
⊢ (𝑤 = (𝑡‘𝑛) → 〈“𝑤”〉 = 〈“(𝑡‘𝑛)”〉) | 
| 142 | 51, 135, 140, 141 | fmptco 7148 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) →
((varFMnd‘(𝐼 × 2o)) ∘ 𝑡) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ 〈“(𝑡‘𝑛)”〉)) | 
| 143 |  | eqidd 2737 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) = (𝑤 ∈ 𝑊 ↦ [𝑤] ∼ )) | 
| 144 |  | eceq1 8785 | . . . . . . . . . 10
⊢ (𝑤 = 〈“(𝑡‘𝑛)”〉 → [𝑤] ∼ =
[〈“(𝑡‘𝑛)”〉] ∼ ) | 
| 145 | 132, 142,
143, 144 | fmptco 7148 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∘
((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ [〈“(𝑡‘𝑛)”〉] ∼ )) | 
| 146 | 1 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → 𝐾 ∈ (𝐺 GrpHom 𝐻)) | 
| 147 | 146, 4 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → 𝐾:𝑋⟶𝐵) | 
| 148 | 147 | feqmptd 6976 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → 𝐾 = (𝑤 ∈ 𝑋 ↦ (𝐾‘𝑤))) | 
| 149 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑤 = [〈“(𝑡‘𝑛)”〉] ∼ → (𝐾‘𝑤) = (𝐾‘[〈“(𝑡‘𝑛)”〉] ∼ )) | 
| 150 | 134, 145,
148, 149 | fmptco 7148 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝐾 ∘ ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∘
((varFMnd‘(𝐼 × 2o)) ∘ 𝑡))) = (𝑛 ∈ (0..^(♯‘𝑡)) ↦ (𝐾‘[〈“(𝑡‘𝑛)”〉] ∼
))) | 
| 151 | 126, 129,
150 | 3eqtr4d 2786 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝑇 ∘ 𝑡) = (𝐾 ∘ ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∘
((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)))) | 
| 152 | 151 | oveq2d 7448 | . . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝐻 Σg (𝑇 ∘ 𝑡)) = (𝐻 Σg (𝐾 ∘ ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∘
((varFMnd‘(𝐼 × 2o)) ∘ 𝑡))))) | 
| 153 | 3, 7, 8, 9, 10, 11, 12, 13, 14, 2, 15 | frgpupval 19793 | . . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝐸‘[𝑡] ∼ ) = (𝐻 Σg
(𝑇 ∘ 𝑡))) | 
| 154 |  | ghmmhm 19245 | . . . . . . . 8
⊢ (𝐾 ∈ (𝐺 GrpHom 𝐻) → 𝐾 ∈ (𝐺 MndHom 𝐻)) | 
| 155 | 146, 154 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → 𝐾 ∈ (𝐺 MndHom 𝐻)) | 
| 156 | 138 | vrmdf 18872 | . . . . . . . . . . 11
⊢ ((𝐼 × 2o) ∈ V
→ (varFMnd‘(𝐼 × 2o)):(𝐼 × 2o)⟶Word (𝐼 ×
2o)) | 
| 157 | 137, 156 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) →
(varFMnd‘(𝐼 × 2o)):(𝐼 × 2o)⟶Word (𝐼 ×
2o)) | 
| 158 | 47 | feq3d 6722 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) →
((varFMnd‘(𝐼 × 2o)):(𝐼 × 2o)⟶𝑊 ↔
(varFMnd‘(𝐼 × 2o)):(𝐼 × 2o)⟶Word (𝐼 ×
2o))) | 
| 159 | 157, 158 | mpbird 257 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) →
(varFMnd‘(𝐼 × 2o)):(𝐼 × 2o)⟶𝑊) | 
| 160 |  | wrdco 14871 | . . . . . . . . 9
⊢ ((𝑡 ∈ Word (𝐼 × 2o) ∧
(varFMnd‘(𝐼 × 2o)):(𝐼 × 2o)⟶𝑊) →
((varFMnd‘(𝐼 × 2o)) ∘ 𝑡) ∈ Word 𝑊) | 
| 161 | 48, 159, 160 | syl2anc 584 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) →
((varFMnd‘(𝐼 × 2o)) ∘ 𝑡) ∈ Word 𝑊) | 
| 162 | 33 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → 𝑊 = (Base‘(freeMnd‘(𝐼 ×
2o)))) | 
| 163 | 162 | mpteq1d 5236 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) = (𝑤 ∈
(Base‘(freeMnd‘(𝐼 × 2o))) ↦ [𝑤] ∼ )) | 
| 164 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢ (𝑤 ∈
(Base‘(freeMnd‘(𝐼 × 2o))) ↦ [𝑤] ∼ ) = (𝑤 ∈
(Base‘(freeMnd‘(𝐼 × 2o))) ↦ [𝑤] ∼ ) | 
| 165 | 20, 30, 14, 13, 164 | frgpmhm 19784 | . . . . . . . . . . . 12
⊢ (𝐼 ∈ 𝑉 → (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2o)))
↦ [𝑤] ∼ )
∈ ((freeMnd‘(𝐼
× 2o)) MndHom 𝐺)) | 
| 166 | 136, 165 | syl 17 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝑤 ∈ (Base‘(freeMnd‘(𝐼 × 2o)))
↦ [𝑤] ∼ )
∈ ((freeMnd‘(𝐼
× 2o)) MndHom 𝐺)) | 
| 167 | 163, 166 | eqeltrd 2840 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∈
((freeMnd‘(𝐼 ×
2o)) MndHom 𝐺)) | 
| 168 | 30, 2 | mhmf 18803 | . . . . . . . . . 10
⊢ ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∈
((freeMnd‘(𝐼 ×
2o)) MndHom 𝐺)
→ (𝑤 ∈ 𝑊 ↦ [𝑤] ∼
):(Base‘(freeMnd‘(𝐼 × 2o)))⟶𝑋) | 
| 169 | 167, 168 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝑤 ∈ 𝑊 ↦ [𝑤] ∼
):(Base‘(freeMnd‘(𝐼 × 2o)))⟶𝑋) | 
| 170 | 162 | feq2d 6721 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ):𝑊⟶𝑋 ↔ (𝑤 ∈ 𝑊 ↦ [𝑤] ∼
):(Base‘(freeMnd‘(𝐼 × 2o)))⟶𝑋)) | 
| 171 | 169, 170 | mpbird 257 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ):𝑊⟶𝑋) | 
| 172 |  | wrdco 14871 | . . . . . . . 8
⊢
((((varFMnd‘(𝐼 × 2o)) ∘ 𝑡) ∈ Word 𝑊 ∧ (𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ):𝑊⟶𝑋) → ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∘
((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)) ∈ Word 𝑋) | 
| 173 | 161, 171,
172 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∘
((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)) ∈ Word 𝑋) | 
| 174 | 2 | gsumwmhm 18859 | . . . . . . 7
⊢ ((𝐾 ∈ (𝐺 MndHom 𝐻) ∧ ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∘
((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)) ∈ Word 𝑋) → (𝐾‘(𝐺 Σg ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∘
((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)))) = (𝐻 Σg (𝐾 ∘ ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∘
((varFMnd‘(𝐼 × 2o)) ∘ 𝑡))))) | 
| 175 | 155, 173,
174 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝐾‘(𝐺 Σg ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∘
((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)))) = (𝐻 Σg (𝐾 ∘ ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∘
((varFMnd‘(𝐼 × 2o)) ∘ 𝑡))))) | 
| 176 | 152, 153,
175 | 3eqtr4d 2786 | . . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝐸‘[𝑡] ∼ ) = (𝐾‘(𝐺 Σg ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∘
((varFMnd‘(𝐼 × 2o)) ∘ 𝑡))))) | 
| 177 | 20, 138 | frmdgsum 18876 | . . . . . . . . 9
⊢ (((𝐼 × 2o) ∈ V
∧ 𝑡 ∈ Word (𝐼 × 2o)) →
((freeMnd‘(𝐼 ×
2o)) Σg
((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)) = 𝑡) | 
| 178 | 25, 48, 177 | syl2an2r 685 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → ((freeMnd‘(𝐼 × 2o))
Σg ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)) = 𝑡) | 
| 179 | 178 | fveq2d 6909 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼
)‘((freeMnd‘(𝐼
× 2o)) Σg
((varFMnd‘(𝐼 × 2o)) ∘ 𝑡))) = ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ )‘𝑡)) | 
| 180 |  | wrdco 14871 | . . . . . . . . . 10
⊢ ((𝑡 ∈ Word (𝐼 × 2o) ∧
(varFMnd‘(𝐼 × 2o)):(𝐼 × 2o)⟶Word (𝐼 × 2o)) →
((varFMnd‘(𝐼 × 2o)) ∘ 𝑡) ∈ Word Word (𝐼 ×
2o)) | 
| 181 | 48, 157, 180 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) →
((varFMnd‘(𝐼 × 2o)) ∘ 𝑡) ∈ Word Word (𝐼 ×
2o)) | 
| 182 | 32 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (Base‘(freeMnd‘(𝐼 × 2o))) = Word
(𝐼 ×
2o)) | 
| 183 |  | wrdeq 14575 | . . . . . . . . . 10
⊢
((Base‘(freeMnd‘(𝐼 × 2o))) = Word (𝐼 × 2o) →
Word (Base‘(freeMnd‘(𝐼 × 2o))) = Word Word (𝐼 ×
2o)) | 
| 184 | 182, 183 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → Word
(Base‘(freeMnd‘(𝐼 × 2o))) = Word Word (𝐼 ×
2o)) | 
| 185 | 181, 184 | eleqtrrd 2843 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) →
((varFMnd‘(𝐼 × 2o)) ∘ 𝑡) ∈ Word
(Base‘(freeMnd‘(𝐼 × 2o)))) | 
| 186 | 30 | gsumwmhm 18859 | . . . . . . . 8
⊢ (((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∈
((freeMnd‘(𝐼 ×
2o)) MndHom 𝐺)
∧ ((varFMnd‘(𝐼 × 2o)) ∘ 𝑡) ∈ Word
(Base‘(freeMnd‘(𝐼 × 2o)))) → ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼
)‘((freeMnd‘(𝐼
× 2o)) Σg
((varFMnd‘(𝐼 × 2o)) ∘ 𝑡))) = (𝐺 Σg ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∘
((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)))) | 
| 187 | 167, 185,
186 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼
)‘((freeMnd‘(𝐼
× 2o)) Σg
((varFMnd‘(𝐼 × 2o)) ∘ 𝑡))) = (𝐺 Σg ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∘
((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)))) | 
| 188 | 12, 13 | efger 19737 | . . . . . . . . 9
⊢  ∼ Er
𝑊 | 
| 189 | 188 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → ∼ Er 𝑊) | 
| 190 | 12 | fvexi 6919 | . . . . . . . . 9
⊢ 𝑊 ∈ V | 
| 191 | 190 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → 𝑊 ∈ V) | 
| 192 |  | eqid 2736 | . . . . . . . 8
⊢ (𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) = (𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) | 
| 193 | 189, 191,
192 | divsfval 17593 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ )‘𝑡) = [𝑡] ∼ ) | 
| 194 | 179, 187,
193 | 3eqtr3d 2784 | . . . . . 6
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝐺 Σg ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∘
((varFMnd‘(𝐼 × 2o)) ∘ 𝑡))) = [𝑡] ∼ ) | 
| 195 | 194 | fveq2d 6909 | . . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝐾‘(𝐺 Σg ((𝑤 ∈ 𝑊 ↦ [𝑤] ∼ ) ∘
((varFMnd‘(𝐼 × 2o)) ∘ 𝑡)))) = (𝐾‘[𝑡] ∼ )) | 
| 196 | 176, 195 | eqtr2d 2777 | . . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑊) → (𝐾‘[𝑡] ∼ ) = (𝐸‘[𝑡] ∼ )) | 
| 197 | 42, 45, 196 | ectocld 8825 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ (𝑊 / ∼ )) → (𝐾‘𝑎) = (𝐸‘𝑎)) | 
| 198 | 41, 197 | syldan 591 | . 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝑋) → (𝐾‘𝑎) = (𝐸‘𝑎)) | 
| 199 | 6, 19, 198 | eqfnfvd 7053 | 1
⊢ (𝜑 → 𝐾 = 𝐸) |