Metamath Proof Explorer


Theorem 2shfti

Description: Composite shift operations. (Contributed by NM, 19-Aug-2005) (Revised by Mario Carneiro, 5-Nov-2013)

Ref Expression
Hypothesis shftfval.1 𝐹 ∈ V
Assertion 2shfti ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐹 shift 𝐴 ) shift 𝐵 ) = ( 𝐹 shift ( 𝐴 + 𝐵 ) ) )

Proof

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 ( 𝐴 + 𝐵 ) ) )