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	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	phllmhm.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
	phllmhm.v	$$⊢V={\mathrm{Base}}_W$$
	ipdir.g	$$⊢\underset{\dot{}}{+}={+}_W$$
	ipdir.p	$$⊢\underset{\dot{}}{⨣}={+}_F$$
Assertion	ipdir	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\in V\right)\right)\to \left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{,}C=\left(A\underset{\dot{}}{,}C\right)\underset{\dot{}}{⨣}\left(B\underset{\dot{}}{,}C\right)$$

Proof

Step	Hyp	Ref	Expression
1		phlsrng.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2		phllmhm.h	$$⊢\underset{\dot{}}{,}={\cdot }_{𝑖}\left(W\right)$$
3		phllmhm.v	$$⊢V={\mathrm{Base}}_W$$
4		ipdir.g	$$⊢\underset{\dot{}}{+}={+}_W$$
5		ipdir.p	$$⊢\underset{\dot{}}{⨣}={+}_F$$
6		eqid	$$⊢\left(x\in V⟼x\underset{\dot{}}{,}C\right)=\left(x\in V⟼x\underset{\dot{}}{,}C\right)$$
7	1 2 3 6	phllmhm	$$⊢\left(W\in \mathrm{PreHil}\wedge C\in V\right)\to \left(x\in V⟼x\underset{\dot{}}{,}C\right)\in \left(W\mathrm{LMHom}\mathrm{ringLMod}\left(F\right)\right)$$
8	7	3ad2antr3	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\in V\right)\right)\to \left(x\in V⟼x\underset{\dot{}}{,}C\right)\in \left(W\mathrm{LMHom}\mathrm{ringLMod}\left(F\right)\right)$$
9		lmghm	$$⊢\left(x\in V⟼x\underset{\dot{}}{,}C\right)\in \left(W\mathrm{LMHom}\mathrm{ringLMod}\left(F\right)\right)\to \left(x\in V⟼x\underset{\dot{}}{,}C\right)\in \left(W\mathrm{GrpHom}\mathrm{ringLMod}\left(F\right)\right)$$
10	8 9	syl	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\in V\right)\right)\to \left(x\in V⟼x\underset{\dot{}}{,}C\right)\in \left(W\mathrm{GrpHom}\mathrm{ringLMod}\left(F\right)\right)$$
11		simpr1	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\in V\right)\right)\to A\in V$$
12		simpr2	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\in V\right)\right)\to B\in V$$
13		rlmplusg	$$⊢{+}_F={+}_{\mathrm{ringLMod}\left(F\right)}$$
14	5 13	eqtri	$$⊢\underset{\dot{}}{⨣}={+}_{\mathrm{ringLMod}\left(F\right)}$$
15	3 4 14	ghmlin	$$⊢\left(\left(x\in V⟼x\underset{\dot{}}{,}C\right)\in \left(W\mathrm{GrpHom}\mathrm{ringLMod}\left(F\right)\right)\wedge A\in V\wedge B\in V\right)\to \left(x\in V⟼x\underset{\dot{}}{,}C\right)\left(A\underset{\dot{}}{+}B\right)=\left(x\in V⟼x\underset{\dot{}}{,}C\right)\left(A\right)\underset{\dot{}}{⨣}\left(x\in V⟼x\underset{\dot{}}{,}C\right)\left(B\right)$$
16	10 11 12 15	syl3anc	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\in V\right)\right)\to \left(x\in V⟼x\underset{\dot{}}{,}C\right)\left(A\underset{\dot{}}{+}B\right)=\left(x\in V⟼x\underset{\dot{}}{,}C\right)\left(A\right)\underset{\dot{}}{⨣}\left(x\in V⟼x\underset{\dot{}}{,}C\right)\left(B\right)$$
17		phllmod	$$⊢W\in \mathrm{PreHil}\to W\in \mathrm{LMod}$$
18	3 4	lmodvacl	$$⊢\left(W\in \mathrm{LMod}\wedge A\in V\wedge B\in V\right)\to A\underset{\dot{}}{+}B\in V$$
19	17 18	syl3an1	$$⊢\left(W\in \mathrm{PreHil}\wedge A\in V\wedge B\in V\right)\to A\underset{\dot{}}{+}B\in V$$
20	19	3adant3r3	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\in V\right)\right)\to A\underset{\dot{}}{+}B\in V$$
21		oveq1	$$⊢x=A\underset{\dot{}}{+}B\to x\underset{\dot{}}{,}C=\left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{,}C$$
22		ovex	$$⊢x\underset{\dot{}}{,}C\in \mathrm{V}$$
23	21 6 22	fvmpt3i	$$⊢A\underset{\dot{}}{+}B\in V\to \left(x\in V⟼x\underset{\dot{}}{,}C\right)\left(A\underset{\dot{}}{+}B\right)=\left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{,}C$$
24	20 23	syl	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\in V\right)\right)\to \left(x\in V⟼x\underset{\dot{}}{,}C\right)\left(A\underset{\dot{}}{+}B\right)=\left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{,}C$$
25		oveq1	$$⊢x=A\to x\underset{\dot{}}{,}C=A\underset{\dot{}}{,}C$$
26	25 6 22	fvmpt3i	$$⊢A\in V\to \left(x\in V⟼x\underset{\dot{}}{,}C\right)\left(A\right)=A\underset{\dot{}}{,}C$$
27	11 26	syl	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\in V\right)\right)\to \left(x\in V⟼x\underset{\dot{}}{,}C\right)\left(A\right)=A\underset{\dot{}}{,}C$$
28		oveq1	$$⊢x=B\to x\underset{\dot{}}{,}C=B\underset{\dot{}}{,}C$$
29	28 6 22	fvmpt3i	$$⊢B\in V\to \left(x\in V⟼x\underset{\dot{}}{,}C\right)\left(B\right)=B\underset{\dot{}}{,}C$$
30	12 29	syl	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\in V\right)\right)\to \left(x\in V⟼x\underset{\dot{}}{,}C\right)\left(B\right)=B\underset{\dot{}}{,}C$$
31	27 30	oveq12d	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\in V\right)\right)\to \left(x\in V⟼x\underset{\dot{}}{,}C\right)\left(A\right)\underset{\dot{}}{⨣}\left(x\in V⟼x\underset{\dot{}}{,}C\right)\left(B\right)=\left(A\underset{\dot{}}{,}C\right)\underset{\dot{}}{⨣}\left(B\underset{\dot{}}{,}C\right)$$
32	16 24 31	3eqtr3d	$$⊢\left(W\in \mathrm{PreHil}\wedge \left(A\in V\wedge B\in V\wedge C\in V\right)\right)\to \left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{,}C=\left(A\underset{\dot{}}{,}C\right)\underset{\dot{}}{⨣}\left(B\underset{\dot{}}{,}C\right)$$