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