Step |
Hyp |
Ref |
Expression |
1 |
|
shftfval.1 |
⊢ 𝐹 ∈ V |
2 |
1
|
shftfval |
⊢ ( 𝐴 ∈ ℂ → ( 𝐹 shift 𝐴 ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } ) |
3 |
2
|
breqd |
⊢ ( 𝐴 ∈ ℂ → ( 𝐵 ( 𝐹 shift 𝐴 ) 𝑧 ↔ 𝐵 { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } 𝑧 ) ) |
4 |
|
eleq1 |
⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∈ ℂ ↔ 𝐵 ∈ ℂ ) ) |
5 |
|
oveq1 |
⊢ ( 𝑥 = 𝐵 → ( 𝑥 − 𝐴 ) = ( 𝐵 − 𝐴 ) ) |
6 |
5
|
breq1d |
⊢ ( 𝑥 = 𝐵 → ( ( 𝑥 − 𝐴 ) 𝐹 𝑦 ↔ ( 𝐵 − 𝐴 ) 𝐹 𝑦 ) ) |
7 |
4 6
|
anbi12d |
⊢ ( 𝑥 = 𝐵 → ( ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) ↔ ( 𝐵 ∈ ℂ ∧ ( 𝐵 − 𝐴 ) 𝐹 𝑦 ) ) ) |
8 |
|
breq2 |
⊢ ( 𝑦 = 𝑧 → ( ( 𝐵 − 𝐴 ) 𝐹 𝑦 ↔ ( 𝐵 − 𝐴 ) 𝐹 𝑧 ) ) |
9 |
8
|
anbi2d |
⊢ ( 𝑦 = 𝑧 → ( ( 𝐵 ∈ ℂ ∧ ( 𝐵 − 𝐴 ) 𝐹 𝑦 ) ↔ ( 𝐵 ∈ ℂ ∧ ( 𝐵 − 𝐴 ) 𝐹 𝑧 ) ) ) |
10 |
|
eqid |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } |
11 |
7 9 10
|
brabg |
⊢ ( ( 𝐵 ∈ ℂ ∧ 𝑧 ∈ V ) → ( 𝐵 { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } 𝑧 ↔ ( 𝐵 ∈ ℂ ∧ ( 𝐵 − 𝐴 ) 𝐹 𝑧 ) ) ) |
12 |
11
|
elvd |
⊢ ( 𝐵 ∈ ℂ → ( 𝐵 { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐴 ) 𝐹 𝑦 ) } 𝑧 ↔ ( 𝐵 ∈ ℂ ∧ ( 𝐵 − 𝐴 ) 𝐹 𝑧 ) ) ) |
13 |
3 12
|
sylan9bb |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 ( 𝐹 shift 𝐴 ) 𝑧 ↔ ( 𝐵 ∈ ℂ ∧ ( 𝐵 − 𝐴 ) 𝐹 𝑧 ) ) ) |
14 |
|
ibar |
⊢ ( 𝐵 ∈ ℂ → ( ( 𝐵 − 𝐴 ) 𝐹 𝑧 ↔ ( 𝐵 ∈ ℂ ∧ ( 𝐵 − 𝐴 ) 𝐹 𝑧 ) ) ) |
15 |
14
|
adantl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐵 − 𝐴 ) 𝐹 𝑧 ↔ ( 𝐵 ∈ ℂ ∧ ( 𝐵 − 𝐴 ) 𝐹 𝑧 ) ) ) |
16 |
13 15
|
bitr4d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐵 ( 𝐹 shift 𝐴 ) 𝑧 ↔ ( 𝐵 − 𝐴 ) 𝐹 𝑧 ) ) |
17 |
16
|
abbidv |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → { 𝑧 ∣ 𝐵 ( 𝐹 shift 𝐴 ) 𝑧 } = { 𝑧 ∣ ( 𝐵 − 𝐴 ) 𝐹 𝑧 } ) |
18 |
|
imasng |
⊢ ( 𝐵 ∈ ℂ → ( ( 𝐹 shift 𝐴 ) “ { 𝐵 } ) = { 𝑧 ∣ 𝐵 ( 𝐹 shift 𝐴 ) 𝑧 } ) |
19 |
18
|
adantl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐹 shift 𝐴 ) “ { 𝐵 } ) = { 𝑧 ∣ 𝐵 ( 𝐹 shift 𝐴 ) 𝑧 } ) |
20 |
|
ovex |
⊢ ( 𝐵 − 𝐴 ) ∈ V |
21 |
|
imasng |
⊢ ( ( 𝐵 − 𝐴 ) ∈ V → ( 𝐹 “ { ( 𝐵 − 𝐴 ) } ) = { 𝑧 ∣ ( 𝐵 − 𝐴 ) 𝐹 𝑧 } ) |
22 |
20 21
|
mp1i |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐹 “ { ( 𝐵 − 𝐴 ) } ) = { 𝑧 ∣ ( 𝐵 − 𝐴 ) 𝐹 𝑧 } ) |
23 |
17 19 22
|
3eqtr4d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐹 shift 𝐴 ) “ { 𝐵 } ) = ( 𝐹 “ { ( 𝐵 − 𝐴 ) } ) ) |