Step |
Hyp |
Ref |
Expression |
1 |
|
shftfval.1 |
⊢ 𝐹 ∈ V |
2 |
1
|
shftfval |
⊢ ( 𝐴 ∈ ℂ → ( 𝐹 shift 𝐴 ) = { 〈 𝑧 , 𝑤 〉 ∣ ( 𝑧 ∈ ℂ ∧ ( 𝑧 − 𝐴 ) 𝐹 𝑤 ) } ) |
3 |
2
|
breqd |
⊢ ( 𝐴 ∈ ℂ → ( ( 𝑥 − 𝐵 ) ( 𝐹 shift 𝐴 ) 𝑦 ↔ ( 𝑥 − 𝐵 ) { 〈 𝑧 , 𝑤 〉 ∣ ( 𝑧 ∈ ℂ ∧ ( 𝑧 − 𝐴 ) 𝐹 𝑤 ) } 𝑦 ) ) |
4 |
|
ovex |
⊢ ( 𝑥 − 𝐵 ) ∈ V |
5 |
|
vex |
⊢ 𝑦 ∈ V |
6 |
|
eleq1 |
⊢ ( 𝑧 = ( 𝑥 − 𝐵 ) → ( 𝑧 ∈ ℂ ↔ ( 𝑥 − 𝐵 ) ∈ ℂ ) ) |
7 |
|
oveq1 |
⊢ ( 𝑧 = ( 𝑥 − 𝐵 ) → ( 𝑧 − 𝐴 ) = ( ( 𝑥 − 𝐵 ) − 𝐴 ) ) |
8 |
7
|
breq1d |
⊢ ( 𝑧 = ( 𝑥 − 𝐵 ) → ( ( 𝑧 − 𝐴 ) 𝐹 𝑤 ↔ ( ( 𝑥 − 𝐵 ) − 𝐴 ) 𝐹 𝑤 ) ) |
9 |
6 8
|
anbi12d |
⊢ ( 𝑧 = ( 𝑥 − 𝐵 ) → ( ( 𝑧 ∈ ℂ ∧ ( 𝑧 − 𝐴 ) 𝐹 𝑤 ) ↔ ( ( 𝑥 − 𝐵 ) ∈ ℂ ∧ ( ( 𝑥 − 𝐵 ) − 𝐴 ) 𝐹 𝑤 ) ) ) |
10 |
|
breq2 |
⊢ ( 𝑤 = 𝑦 → ( ( ( 𝑥 − 𝐵 ) − 𝐴 ) 𝐹 𝑤 ↔ ( ( 𝑥 − 𝐵 ) − 𝐴 ) 𝐹 𝑦 ) ) |
11 |
10
|
anbi2d |
⊢ ( 𝑤 = 𝑦 → ( ( ( 𝑥 − 𝐵 ) ∈ ℂ ∧ ( ( 𝑥 − 𝐵 ) − 𝐴 ) 𝐹 𝑤 ) ↔ ( ( 𝑥 − 𝐵 ) ∈ ℂ ∧ ( ( 𝑥 − 𝐵 ) − 𝐴 ) 𝐹 𝑦 ) ) ) |
12 |
|
eqid |
⊢ { 〈 𝑧 , 𝑤 〉 ∣ ( 𝑧 ∈ ℂ ∧ ( 𝑧 − 𝐴 ) 𝐹 𝑤 ) } = { 〈 𝑧 , 𝑤 〉 ∣ ( 𝑧 ∈ ℂ ∧ ( 𝑧 − 𝐴 ) 𝐹 𝑤 ) } |
13 |
4 5 9 11 12
|
brab |
⊢ ( ( 𝑥 − 𝐵 ) { 〈 𝑧 , 𝑤 〉 ∣ ( 𝑧 ∈ ℂ ∧ ( 𝑧 − 𝐴 ) 𝐹 𝑤 ) } 𝑦 ↔ ( ( 𝑥 − 𝐵 ) ∈ ℂ ∧ ( ( 𝑥 − 𝐵 ) − 𝐴 ) 𝐹 𝑦 ) ) |
14 |
3 13
|
bitrdi |
⊢ ( 𝐴 ∈ ℂ → ( ( 𝑥 − 𝐵 ) ( 𝐹 shift 𝐴 ) 𝑦 ↔ ( ( 𝑥 − 𝐵 ) ∈ ℂ ∧ ( ( 𝑥 − 𝐵 ) − 𝐴 ) 𝐹 𝑦 ) ) ) |
15 |
14
|
ad2antrr |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑥 ∈ ℂ ) → ( ( 𝑥 − 𝐵 ) ( 𝐹 shift 𝐴 ) 𝑦 ↔ ( ( 𝑥 − 𝐵 ) ∈ ℂ ∧ ( ( 𝑥 − 𝐵 ) − 𝐴 ) 𝐹 𝑦 ) ) ) |
16 |
|
subcl |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝑥 − 𝐵 ) ∈ ℂ ) |
17 |
16
|
biantrurd |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝑥 − 𝐵 ) − 𝐴 ) 𝐹 𝑦 ↔ ( ( 𝑥 − 𝐵 ) ∈ ℂ ∧ ( ( 𝑥 − 𝐵 ) − 𝐴 ) 𝐹 𝑦 ) ) ) |
18 |
17
|
ancoms |
⊢ ( ( 𝐵 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( ( ( 𝑥 − 𝐵 ) − 𝐴 ) 𝐹 𝑦 ↔ ( ( 𝑥 − 𝐵 ) ∈ ℂ ∧ ( ( 𝑥 − 𝐵 ) − 𝐴 ) 𝐹 𝑦 ) ) ) |
19 |
18
|
adantll |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑥 ∈ ℂ ) → ( ( ( 𝑥 − 𝐵 ) − 𝐴 ) 𝐹 𝑦 ↔ ( ( 𝑥 − 𝐵 ) ∈ ℂ ∧ ( ( 𝑥 − 𝐵 ) − 𝐴 ) 𝐹 𝑦 ) ) ) |
20 |
|
sub32 |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝑥 − 𝐴 ) − 𝐵 ) = ( ( 𝑥 − 𝐵 ) − 𝐴 ) ) |
21 |
|
subsub4 |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝑥 − 𝐴 ) − 𝐵 ) = ( 𝑥 − ( 𝐴 + 𝐵 ) ) ) |
22 |
20 21
|
eqtr3d |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝑥 − 𝐵 ) − 𝐴 ) = ( 𝑥 − ( 𝐴 + 𝐵 ) ) ) |
23 |
22
|
3expb |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ) → ( ( 𝑥 − 𝐵 ) − 𝐴 ) = ( 𝑥 − ( 𝐴 + 𝐵 ) ) ) |
24 |
23
|
ancoms |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑥 ∈ ℂ ) → ( ( 𝑥 − 𝐵 ) − 𝐴 ) = ( 𝑥 − ( 𝐴 + 𝐵 ) ) ) |
25 |
24
|
breq1d |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑥 ∈ ℂ ) → ( ( ( 𝑥 − 𝐵 ) − 𝐴 ) 𝐹 𝑦 ↔ ( 𝑥 − ( 𝐴 + 𝐵 ) ) 𝐹 𝑦 ) ) |
26 |
15 19 25
|
3bitr2d |
⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑥 ∈ ℂ ) → ( ( 𝑥 − 𝐵 ) ( 𝐹 shift 𝐴 ) 𝑦 ↔ ( 𝑥 − ( 𝐴 + 𝐵 ) ) 𝐹 𝑦 ) ) |
27 |
26
|
pm5.32da |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐵 ) ( 𝐹 shift 𝐴 ) 𝑦 ) ↔ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − ( 𝐴 + 𝐵 ) ) 𝐹 𝑦 ) ) ) |
28 |
27
|
opabbidv |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐵 ) ( 𝐹 shift 𝐴 ) 𝑦 ) } = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − ( 𝐴 + 𝐵 ) ) 𝐹 𝑦 ) } ) |
29 |
|
ovex |
⊢ ( 𝐹 shift 𝐴 ) ∈ V |
30 |
29
|
shftfval |
⊢ ( 𝐵 ∈ ℂ → ( ( 𝐹 shift 𝐴 ) shift 𝐵 ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐵 ) ( 𝐹 shift 𝐴 ) 𝑦 ) } ) |
31 |
30
|
adantl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐹 shift 𝐴 ) shift 𝐵 ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − 𝐵 ) ( 𝐹 shift 𝐴 ) 𝑦 ) } ) |
32 |
|
addcl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 𝐵 ) ∈ ℂ ) |
33 |
1
|
shftfval |
⊢ ( ( 𝐴 + 𝐵 ) ∈ ℂ → ( 𝐹 shift ( 𝐴 + 𝐵 ) ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − ( 𝐴 + 𝐵 ) ) 𝐹 𝑦 ) } ) |
34 |
32 33
|
syl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐹 shift ( 𝐴 + 𝐵 ) ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ ℂ ∧ ( 𝑥 − ( 𝐴 + 𝐵 ) ) 𝐹 𝑦 ) } ) |
35 |
28 31 34
|
3eqtr4d |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐹 shift 𝐴 ) shift 𝐵 ) = ( 𝐹 shift ( 𝐴 + 𝐵 ) ) ) |