Theorem vcdir

Description: Distributive law for the scalar product of a complex vector space. (Contributed by NM, 3-Nov-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	vciOLD.1	⊢ 𝐺 = ( 1st ‘ 𝑊 )
	vciOLD.2	⊢ 𝑆 = ( 2nd ‘ 𝑊 )
	vciOLD.3	⊢ 𝑋 = ran 𝐺
Assertion	vcdir	⊢ ( ( 𝑊 ∈ CVecOLD ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 + 𝐵 ) 𝑆 𝐶 ) = ( ( 𝐴 𝑆 𝐶 ) 𝐺 ( 𝐵 𝑆 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		vciOLD.1	⊢ 𝐺 = ( 1st ‘ 𝑊 )
2		vciOLD.2	⊢ 𝑆 = ( 2nd ‘ 𝑊 )
3		vciOLD.3	⊢ 𝑋 = ran 𝐺
4	1 2 3	vciOLD	⊢ ( 𝑊 ∈ CVecOLD → ( 𝐺 ∈ AbelOp ∧ 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( ( 1 𝑆 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑆 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑦 𝑆 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) ) ) ) ) )
5		simpl	⊢ ( ( ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) ) → ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) )
6	5	ralimi	⊢ ( ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) ) → ∀ 𝑧 ∈ ℂ ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) )
7	6	adantl	⊢ ( ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑆 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑦 𝑆 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) ) ) → ∀ 𝑧 ∈ ℂ ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) )
8	7	ralimi	⊢ ( ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑆 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑦 𝑆 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) ) ) → ∀ 𝑦 ∈ ℂ ∀ 𝑧 ∈ ℂ ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) )
9	8	adantl	⊢ ( ( ( 1 𝑆 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑆 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑦 𝑆 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) ) ) ) → ∀ 𝑦 ∈ ℂ ∀ 𝑧 ∈ ℂ ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) )
10	9	ralimi	⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( 1 𝑆 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑆 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑦 𝑆 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) ) ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ ℂ ∀ 𝑧 ∈ ℂ ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) )
11	10	3ad2ant3	⊢ ( ( 𝐺 ∈ AbelOp ∧ 𝑆 : ( ℂ × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( ( 1 𝑆 𝑥 ) = 𝑥 ∧ ∀ 𝑦 ∈ ℂ ( ∀ 𝑧 ∈ 𝑋 ( 𝑦 𝑆 ( 𝑥 𝐺 𝑧 ) ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑦 𝑆 𝑧 ) ) ∧ ∀ 𝑧 ∈ ℂ ( ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ∧ ( ( 𝑦 · 𝑧 ) 𝑆 𝑥 ) = ( 𝑦 𝑆 ( 𝑧 𝑆 𝑥 ) ) ) ) ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ ℂ ∀ 𝑧 ∈ ℂ ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) )
12	4 11	syl	⊢ ( 𝑊 ∈ CVecOLD → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ ℂ ∀ 𝑧 ∈ ℂ ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) )
13		oveq2	⊢ ( 𝑥 = 𝐶 → ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 + 𝑧 ) 𝑆 𝐶 ) )
14		oveq2	⊢ ( 𝑥 = 𝐶 → ( 𝑦 𝑆 𝑥 ) = ( 𝑦 𝑆 𝐶 ) )
15		oveq2	⊢ ( 𝑥 = 𝐶 → ( 𝑧 𝑆 𝑥 ) = ( 𝑧 𝑆 𝐶 ) )
16	14 15	oveq12d	⊢ ( 𝑥 = 𝐶 → ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) = ( ( 𝑦 𝑆 𝐶 ) 𝐺 ( 𝑧 𝑆 𝐶 ) ) )
17	13 16	eqeq12d	⊢ ( 𝑥 = 𝐶 → ( ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) ↔ ( ( 𝑦 + 𝑧 ) 𝑆 𝐶 ) = ( ( 𝑦 𝑆 𝐶 ) 𝐺 ( 𝑧 𝑆 𝐶 ) ) ) )
18		oveq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 + 𝑧 ) = ( 𝐴 + 𝑧 ) )
19	18	oveq1d	⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 + 𝑧 ) 𝑆 𝐶 ) = ( ( 𝐴 + 𝑧 ) 𝑆 𝐶 ) )
20		oveq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 𝑆 𝐶 ) = ( 𝐴 𝑆 𝐶 ) )
21	20	oveq1d	⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 𝑆 𝐶 ) 𝐺 ( 𝑧 𝑆 𝐶 ) ) = ( ( 𝐴 𝑆 𝐶 ) 𝐺 ( 𝑧 𝑆 𝐶 ) ) )
22	19 21	eqeq12d	⊢ ( 𝑦 = 𝐴 → ( ( ( 𝑦 + 𝑧 ) 𝑆 𝐶 ) = ( ( 𝑦 𝑆 𝐶 ) 𝐺 ( 𝑧 𝑆 𝐶 ) ) ↔ ( ( 𝐴 + 𝑧 ) 𝑆 𝐶 ) = ( ( 𝐴 𝑆 𝐶 ) 𝐺 ( 𝑧 𝑆 𝐶 ) ) ) )
23		oveq2	⊢ ( 𝑧 = 𝐵 → ( 𝐴 + 𝑧 ) = ( 𝐴 + 𝐵 ) )
24	23	oveq1d	⊢ ( 𝑧 = 𝐵 → ( ( 𝐴 + 𝑧 ) 𝑆 𝐶 ) = ( ( 𝐴 + 𝐵 ) 𝑆 𝐶 ) )
25		oveq1	⊢ ( 𝑧 = 𝐵 → ( 𝑧 𝑆 𝐶 ) = ( 𝐵 𝑆 𝐶 ) )
26	25	oveq2d	⊢ ( 𝑧 = 𝐵 → ( ( 𝐴 𝑆 𝐶 ) 𝐺 ( 𝑧 𝑆 𝐶 ) ) = ( ( 𝐴 𝑆 𝐶 ) 𝐺 ( 𝐵 𝑆 𝐶 ) ) )
27	24 26	eqeq12d	⊢ ( 𝑧 = 𝐵 → ( ( ( 𝐴 + 𝑧 ) 𝑆 𝐶 ) = ( ( 𝐴 𝑆 𝐶 ) 𝐺 ( 𝑧 𝑆 𝐶 ) ) ↔ ( ( 𝐴 + 𝐵 ) 𝑆 𝐶 ) = ( ( 𝐴 𝑆 𝐶 ) 𝐺 ( 𝐵 𝑆 𝐶 ) ) ) )
28	17 22 27	rspc3v	⊢ ( ( 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ ℂ ∀ 𝑧 ∈ ℂ ( ( 𝑦 + 𝑧 ) 𝑆 𝑥 ) = ( ( 𝑦 𝑆 𝑥 ) 𝐺 ( 𝑧 𝑆 𝑥 ) ) → ( ( 𝐴 + 𝐵 ) 𝑆 𝐶 ) = ( ( 𝐴 𝑆 𝐶 ) 𝐺 ( 𝐵 𝑆 𝐶 ) ) ) )
29	12 28	syl5	⊢ ( ( 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝑊 ∈ CVecOLD → ( ( 𝐴 + 𝐵 ) 𝑆 𝐶 ) = ( ( 𝐴 𝑆 𝐶 ) 𝐺 ( 𝐵 𝑆 𝐶 ) ) ) )
30	29	3coml	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) → ( 𝑊 ∈ CVecOLD → ( ( 𝐴 + 𝐵 ) 𝑆 𝐶 ) = ( ( 𝐴 𝑆 𝐶 ) 𝐺 ( 𝐵 𝑆 𝐶 ) ) ) )
31	30	impcom	⊢ ( ( 𝑊 ∈ CVecOLD ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 + 𝐵 ) 𝑆 𝐶 ) = ( ( 𝐴 𝑆 𝐶 ) 𝐺 ( 𝐵 𝑆 𝐶 ) ) )