Theorem ipsubdir

Description: Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007) (Revised by Mario Carneiro, 7-Oct-2015)

	Ref	Expression
Hypotheses	phlsrng.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	phllmhm.h	⊢ , = ( ·𝑖 ‘ 𝑊 )
	phllmhm.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	ipsubdir.m	⊢ − = ( -g ‘ 𝑊 )
	ipsubdir.s	⊢ 𝑆 = ( -g ‘ 𝐹 )
Assertion	ipsubdir	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 − 𝐵 ) , 𝐶 ) = ( ( 𝐴 , 𝐶 ) 𝑆 ( 𝐵 , 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		phlsrng.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		phllmhm.h	⊢ , = ( ·𝑖 ‘ 𝑊 )
3		phllmhm.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
4		ipsubdir.m	⊢ − = ( -g ‘ 𝑊 )
5		ipsubdir.s	⊢ 𝑆 = ( -g ‘ 𝐹 )
6		simpl	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝑊 ∈ PreHil )
7		phllmod	⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod )
8	7	adantr	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝑊 ∈ LMod )
9		lmodgrp	⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
10	8 9	syl	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝑊 ∈ Grp )
11		simpr1	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐴 ∈ 𝑉 )
12		simpr2	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐵 ∈ 𝑉 )
13	3 4	grpsubcl	⊢ ( ( 𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 − 𝐵 ) ∈ 𝑉 )
14	10 11 12 13	syl3anc	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐴 − 𝐵 ) ∈ 𝑉 )
15		simpr3	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐶 ∈ 𝑉 )
16		eqid	⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
17		eqid	⊢ ( +g ‘ 𝐹 ) = ( +g ‘ 𝐹 )
18	1 2 3 16 17	ipdir	⊢ ( ( 𝑊 ∈ PreHil ∧ ( ( 𝐴 − 𝐵 ) ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( ( 𝐴 − 𝐵 ) ( +g ‘ 𝑊 ) 𝐵 ) , 𝐶 ) = ( ( ( 𝐴 − 𝐵 ) , 𝐶 ) ( +g ‘ 𝐹 ) ( 𝐵 , 𝐶 ) ) )
19	6 14 12 15 18	syl13anc	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( ( 𝐴 − 𝐵 ) ( +g ‘ 𝑊 ) 𝐵 ) , 𝐶 ) = ( ( ( 𝐴 − 𝐵 ) , 𝐶 ) ( +g ‘ 𝐹 ) ( 𝐵 , 𝐶 ) ) )
20	3 16 4	grpnpcan	⊢ ( ( 𝑊 ∈ Grp ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝐴 − 𝐵 ) ( +g ‘ 𝑊 ) 𝐵 ) = 𝐴 )
21	10 11 12 20	syl3anc	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 − 𝐵 ) ( +g ‘ 𝑊 ) 𝐵 ) = 𝐴 )
22	21	oveq1d	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( ( 𝐴 − 𝐵 ) ( +g ‘ 𝑊 ) 𝐵 ) , 𝐶 ) = ( 𝐴 , 𝐶 ) )
23	19 22	eqtr3d	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( ( 𝐴 − 𝐵 ) , 𝐶 ) ( +g ‘ 𝐹 ) ( 𝐵 , 𝐶 ) ) = ( 𝐴 , 𝐶 ) )
24	1	lmodfgrp	⊢ ( 𝑊 ∈ LMod → 𝐹 ∈ Grp )
25	8 24	syl	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐹 ∈ Grp )
26		eqid	⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
27	1 2 3 26	ipcl	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐴 , 𝐶 ) ∈ ( Base ‘ 𝐹 ) )
28	6 11 15 27	syl3anc	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐴 , 𝐶 ) ∈ ( Base ‘ 𝐹 ) )
29	1 2 3 26	ipcl	⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐵 , 𝐶 ) ∈ ( Base ‘ 𝐹 ) )
30	6 12 15 29	syl3anc	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐵 , 𝐶 ) ∈ ( Base ‘ 𝐹 ) )
31	1 2 3 26	ipcl	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 − 𝐵 ) ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ( 𝐴 − 𝐵 ) , 𝐶 ) ∈ ( Base ‘ 𝐹 ) )
32	6 14 15 31	syl3anc	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 − 𝐵 ) , 𝐶 ) ∈ ( Base ‘ 𝐹 ) )
33	26 17 5	grpsubadd	⊢ ( ( 𝐹 ∈ Grp ∧ ( ( 𝐴 , 𝐶 ) ∈ ( Base ‘ 𝐹 ) ∧ ( 𝐵 , 𝐶 ) ∈ ( Base ‘ 𝐹 ) ∧ ( ( 𝐴 − 𝐵 ) , 𝐶 ) ∈ ( Base ‘ 𝐹 ) ) ) → ( ( ( 𝐴 , 𝐶 ) 𝑆 ( 𝐵 , 𝐶 ) ) = ( ( 𝐴 − 𝐵 ) , 𝐶 ) ↔ ( ( ( 𝐴 − 𝐵 ) , 𝐶 ) ( +g ‘ 𝐹 ) ( 𝐵 , 𝐶 ) ) = ( 𝐴 , 𝐶 ) ) )
34	25 28 30 32 33	syl13anc	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( ( 𝐴 , 𝐶 ) 𝑆 ( 𝐵 , 𝐶 ) ) = ( ( 𝐴 − 𝐵 ) , 𝐶 ) ↔ ( ( ( 𝐴 − 𝐵 ) , 𝐶 ) ( +g ‘ 𝐹 ) ( 𝐵 , 𝐶 ) ) = ( 𝐴 , 𝐶 ) ) )
35	23 34	mpbird	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 , 𝐶 ) 𝑆 ( 𝐵 , 𝐶 ) ) = ( ( 𝐴 − 𝐵 ) , 𝐶 ) )
36	35	eqcomd	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 − 𝐵 ) , 𝐶 ) = ( ( 𝐴 , 𝐶 ) 𝑆 ( 𝐵 , 𝐶 ) ) )