![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > symgextfve | Structured version Visualization version GIF version |
Description: The function value of the extension of a permutation, fixing the additional element, for the additional element. (Contributed by AV, 6-Jan-2019.) |
Ref | Expression |
---|---|
symgext.s | ⊢ 𝑆 = (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) |
symgext.e | ⊢ 𝐸 = (𝑥 ∈ 𝑁 ↦ if(𝑥 = 𝐾, 𝐾, (𝑍‘𝑥))) |
Ref | Expression |
---|---|
symgextfve | ⊢ (𝐾 ∈ 𝑁 → (𝑋 = 𝐾 → (𝐸‘𝑋) = 𝐾)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fveq2 6409 | . . 3 ⊢ (𝑋 = 𝐾 → (𝐸‘𝑋) = (𝐸‘𝐾)) | |
2 | iftrue 4281 | . . . . 5 ⊢ (𝑥 = 𝐾 → if(𝑥 = 𝐾, 𝐾, (𝑍‘𝑥)) = 𝐾) | |
3 | symgext.e | . . . . 5 ⊢ 𝐸 = (𝑥 ∈ 𝑁 ↦ if(𝑥 = 𝐾, 𝐾, (𝑍‘𝑥))) | |
4 | 2, 3 | fvmptg 6503 | . . . 4 ⊢ ((𝐾 ∈ 𝑁 ∧ 𝐾 ∈ 𝑁) → (𝐸‘𝐾) = 𝐾) |
5 | 4 | anidms 563 | . . 3 ⊢ (𝐾 ∈ 𝑁 → (𝐸‘𝐾) = 𝐾) |
6 | 1, 5 | sylan9eqr 2853 | . 2 ⊢ ((𝐾 ∈ 𝑁 ∧ 𝑋 = 𝐾) → (𝐸‘𝑋) = 𝐾) |
7 | 6 | ex 402 | 1 ⊢ (𝐾 ∈ 𝑁 → (𝑋 = 𝐾 → (𝐸‘𝑋) = 𝐾)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1653 ∈ wcel 2157 ∖ cdif 3764 ifcif 4275 {csn 4366 ↦ cmpt 4920 ‘cfv 6099 Basecbs 16181 SymGrpcsymg 18106 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2354 ax-ext 2775 ax-sep 4973 ax-nul 4981 ax-pr 5095 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2590 df-eu 2607 df-clab 2784 df-cleq 2790 df-clel 2793 df-nfc 2928 df-ral 3092 df-rex 3093 df-rab 3096 df-v 3385 df-sbc 3632 df-dif 3770 df-un 3772 df-in 3774 df-ss 3781 df-nul 4114 df-if 4276 df-sn 4367 df-pr 4369 df-op 4373 df-uni 4627 df-br 4842 df-opab 4904 df-mpt 4921 df-id 5218 df-xp 5316 df-rel 5317 df-cnv 5318 df-co 5319 df-dm 5320 df-iota 6062 df-fun 6101 df-fv 6107 |
This theorem is referenced by: symgextf1lem 18149 symgextfo 18151 |
Copyright terms: Public domain | W3C validator |