Step |
Hyp |
Ref |
Expression |
1 |
|
symgext.s |
⊢ 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) ) |
2 |
|
symgext.e |
⊢ 𝐸 = ( 𝑥 ∈ 𝑁 ↦ if ( 𝑥 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑥 ) ) ) |
3 |
|
eldifi |
⊢ ( 𝑋 ∈ ( 𝑁 ∖ { 𝐾 } ) → 𝑋 ∈ 𝑁 ) |
4 |
|
fvexd |
⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ( 𝑍 ‘ 𝑋 ) ∈ V ) |
5 |
|
ifexg |
⊢ ( ( 𝐾 ∈ 𝑁 ∧ ( 𝑍 ‘ 𝑋 ) ∈ V ) → if ( 𝑋 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑋 ) ) ∈ V ) |
6 |
4 5
|
syldan |
⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → if ( 𝑋 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑋 ) ) ∈ V ) |
7 |
|
eqeq1 |
⊢ ( 𝑥 = 𝑋 → ( 𝑥 = 𝐾 ↔ 𝑋 = 𝐾 ) ) |
8 |
|
fveq2 |
⊢ ( 𝑥 = 𝑋 → ( 𝑍 ‘ 𝑥 ) = ( 𝑍 ‘ 𝑋 ) ) |
9 |
7 8
|
ifbieq2d |
⊢ ( 𝑥 = 𝑋 → if ( 𝑥 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑥 ) ) = if ( 𝑋 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑋 ) ) ) |
10 |
9 2
|
fvmptg |
⊢ ( ( 𝑋 ∈ 𝑁 ∧ if ( 𝑋 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑋 ) ) ∈ V ) → ( 𝐸 ‘ 𝑋 ) = if ( 𝑋 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑋 ) ) ) |
11 |
3 6 10
|
syl2anr |
⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝐸 ‘ 𝑋 ) = if ( 𝑋 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑋 ) ) ) |
12 |
|
eldifsnneq |
⊢ ( 𝑋 ∈ ( 𝑁 ∖ { 𝐾 } ) → ¬ 𝑋 = 𝐾 ) |
13 |
12
|
adantl |
⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ¬ 𝑋 = 𝐾 ) |
14 |
13
|
iffalsed |
⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → if ( 𝑋 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑋 ) ) = ( 𝑍 ‘ 𝑋 ) ) |
15 |
11 14
|
eqtrd |
⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝐸 ‘ 𝑋 ) = ( 𝑍 ‘ 𝑋 ) ) |
16 |
15
|
ex |
⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ( 𝑋 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( 𝐸 ‘ 𝑋 ) = ( 𝑍 ‘ 𝑋 ) ) ) |