Metamath Proof Explorer

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 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 − 𝐵 ) , 𝐶 ) = ( ( 𝐴 , 𝐶 ) 𝑆 ( 𝐵 , 𝐶 ) ) )