This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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