Theorem ipdir

Description: Distributive law for inner product (right-distributivity). Equation I3 of Ponnusamy p. 362. (Contributed by NM, 25-Aug-2007) (Revised by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Hypotheses	phlsrng.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	phllmhm.h	⊢ , = ( ·𝑖 ‘ 𝑊 )
	phllmhm.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	ipdir.g	⊢ + = ( +g ‘ 𝑊 )
	ipdir.p	⊢ ⨣ = ( +g ‘ 𝐹 )
Assertion	ipdir	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 + 𝐵 ) , 𝐶 ) = ( ( 𝐴 , 𝐶 ) ⨣ ( 𝐵 , 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		phlsrng.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		phllmhm.h	⊢ , = ( ·𝑖 ‘ 𝑊 )
3		phllmhm.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
4		ipdir.g	⊢ + = ( +g ‘ 𝑊 )
5		ipdir.p	⊢ ⨣ = ( +g ‘ 𝐹 )
6		eqid	⊢ ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) = ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) )
7	1 2 3 6	phllmhm	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐶 ∈ 𝑉 ) → ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) )
8	7	3ad2antr3	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) )
9		lmghm	⊢ ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) → ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ∈ ( 𝑊 GrpHom ( ringLMod ‘ 𝐹 ) ) )
10	8 9	syl	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ∈ ( 𝑊 GrpHom ( ringLMod ‘ 𝐹 ) ) )
11		simpr1	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐴 ∈ 𝑉 )
12		simpr2	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐵 ∈ 𝑉 )
13		rlmplusg	⊢ ( +g ‘ 𝐹 ) = ( +g ‘ ( ringLMod ‘ 𝐹 ) )
14	5 13	eqtri	⊢ ⨣ = ( +g ‘ ( ringLMod ‘ 𝐹 ) )
15	3 4 14	ghmlin	⊢ ( ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ∈ ( 𝑊 GrpHom ( ringLMod ‘ 𝐹 ) ) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ 𝐴 ) ⨣ ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ 𝐵 ) ) )
16	10 11 12 15	syl3anc	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ 𝐴 ) ⨣ ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ 𝐵 ) ) )
17		phllmod	⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod )
18	3 4	lmodvacl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 + 𝐵 ) ∈ 𝑉 )
19	17 18	syl3an1	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 + 𝐵 ) ∈ 𝑉 )
20	19	3adant3r3	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐴 + 𝐵 ) ∈ 𝑉 )
21		oveq1	⊢ ( 𝑥 = ( 𝐴 + 𝐵 ) → ( 𝑥 , 𝐶 ) = ( ( 𝐴 + 𝐵 ) , 𝐶 ) )
22		ovex	⊢ ( 𝑥 , 𝐶 ) ∈ V
23	21 6 22	fvmpt3i	⊢ ( ( 𝐴 + 𝐵 ) ∈ 𝑉 → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ ( 𝐴 + 𝐵 ) ) = ( ( 𝐴 + 𝐵 ) , 𝐶 ) )
24	20 23	syl	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ ( 𝐴 + 𝐵 ) ) = ( ( 𝐴 + 𝐵 ) , 𝐶 ) )
25		oveq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 , 𝐶 ) = ( 𝐴 , 𝐶 ) )
26	25 6 22	fvmpt3i	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ 𝐴 ) = ( 𝐴 , 𝐶 ) )
27	11 26	syl	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ 𝐴 ) = ( 𝐴 , 𝐶 ) )
28		oveq1	⊢ ( 𝑥 = 𝐵 → ( 𝑥 , 𝐶 ) = ( 𝐵 , 𝐶 ) )
29	28 6 22	fvmpt3i	⊢ ( 𝐵 ∈ 𝑉 → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ 𝐵 ) = ( 𝐵 , 𝐶 ) )
30	12 29	syl	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ 𝐵 ) = ( 𝐵 , 𝐶 ) )
31	27 30	oveq12d	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ 𝐴 ) ⨣ ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐶 ) ) ‘ 𝐵 ) ) = ( ( 𝐴 , 𝐶 ) ⨣ ( 𝐵 , 𝐶 ) ) )
32	16 24 31	3eqtr3d	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 + 𝐵 ) , 𝐶 ) = ( ( 𝐴 , 𝐶 ) ⨣ ( 𝐵 , 𝐶 ) ) )