Metamath Proof Explorer

Theorem his7

Description: Distributive law for inner product. Lemma 3.1(S7) of Beran p. 95. (Contributed by NM, 31-Jul-1999) (New usage is discouraged.)

		Ref	Expression
	Assertion	his7	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐴 ·_ih ( 𝐵 +_ℎ 𝐶 ) ) = ( ( 𝐴 ·_ih 𝐵 ) + ( 𝐴 ·_ih 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ax-his2	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ( 𝐵 +_ℎ 𝐶 ) ·_ih 𝐴 ) = ( ( 𝐵 ·_ih 𝐴 ) + ( 𝐶 ·_ih 𝐴 ) ) )
2	1	fveq2d	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ∗ ‘ ( ( 𝐵 +_ℎ 𝐶 ) ·_ih 𝐴 ) ) = ( ∗ ‘ ( ( 𝐵 ·_ih 𝐴 ) + ( 𝐶 ·_ih 𝐴 ) ) ) )
3		hicl	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( 𝐵 ·_ih 𝐴 ) ∈ ℂ )
4		hicl	⊢ ( ( 𝐶 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( 𝐶 ·_ih 𝐴 ) ∈ ℂ )
5		cjadd	⊢ ( ( ( 𝐵 ·_ih 𝐴 ) ∈ ℂ ∧ ( 𝐶 ·_ih 𝐴 ) ∈ ℂ ) → ( ∗ ‘ ( ( 𝐵 ·_ih 𝐴 ) + ( 𝐶 ·_ih 𝐴 ) ) ) = ( ( ∗ ‘ ( 𝐵 ·_ih 𝐴 ) ) + ( ∗ ‘ ( 𝐶 ·_ih 𝐴 ) ) ) )
6	3 4 5	syl2an	⊢ ( ( ( 𝐵 ∈ ℋ ∧ 𝐴 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐴 ∈ ℋ ) ) → ( ∗ ‘ ( ( 𝐵 ·_ih 𝐴 ) + ( 𝐶 ·_ih 𝐴 ) ) ) = ( ( ∗ ‘ ( 𝐵 ·_ih 𝐴 ) ) + ( ∗ ‘ ( 𝐶 ·_ih 𝐴 ) ) ) )
7	6	3impdir	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ∗ ‘ ( ( 𝐵 ·_ih 𝐴 ) + ( 𝐶 ·_ih 𝐴 ) ) ) = ( ( ∗ ‘ ( 𝐵 ·_ih 𝐴 ) ) + ( ∗ ‘ ( 𝐶 ·_ih 𝐴 ) ) ) )
8	2 7	eqtrd	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( ∗ ‘ ( ( 𝐵 +_ℎ 𝐶 ) ·_ih 𝐴 ) ) = ( ( ∗ ‘ ( 𝐵 ·_ih 𝐴 ) ) + ( ∗ ‘ ( 𝐶 ·_ih 𝐴 ) ) ) )
9	8	3comr	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ∗ ‘ ( ( 𝐵 +_ℎ 𝐶 ) ·_ih 𝐴 ) ) = ( ( ∗ ‘ ( 𝐵 ·_ih 𝐴 ) ) + ( ∗ ‘ ( 𝐶 ·_ih 𝐴 ) ) ) )
10		hvaddcl	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐵 +_ℎ 𝐶 ) ∈ ℋ )
11		ax-his1	⊢ ( ( 𝐴 ∈ ℋ ∧ ( 𝐵 +_ℎ 𝐶 ) ∈ ℋ ) → ( 𝐴 ·_ih ( 𝐵 +_ℎ 𝐶 ) ) = ( ∗ ‘ ( ( 𝐵 +_ℎ 𝐶 ) ·_ih 𝐴 ) ) )
12	10 11	sylan2	⊢ ( ( 𝐴 ∈ ℋ ∧ ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ) → ( 𝐴 ·_ih ( 𝐵 +_ℎ 𝐶 ) ) = ( ∗ ‘ ( ( 𝐵 +_ℎ 𝐶 ) ·_ih 𝐴 ) ) )
13	12	3impb	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐴 ·_ih ( 𝐵 +_ℎ 𝐶 ) ) = ( ∗ ‘ ( ( 𝐵 +_ℎ 𝐶 ) ·_ih 𝐴 ) ) )
14		ax-his1	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ·_ih 𝐵 ) = ( ∗ ‘ ( 𝐵 ·_ih 𝐴 ) ) )
15	14	3adant3	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐴 ·_ih 𝐵 ) = ( ∗ ‘ ( 𝐵 ·_ih 𝐴 ) ) )
16		ax-his1	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐴 ·_ih 𝐶 ) = ( ∗ ‘ ( 𝐶 ·_ih 𝐴 ) ) )
17	16	3adant2	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐴 ·_ih 𝐶 ) = ( ∗ ‘ ( 𝐶 ·_ih 𝐴 ) ) )
18	15 17	oveq12d	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 ·_ih 𝐵 ) + ( 𝐴 ·_ih 𝐶 ) ) = ( ( ∗ ‘ ( 𝐵 ·_ih 𝐴 ) ) + ( ∗ ‘ ( 𝐶 ·_ih 𝐴 ) ) ) )
19	9 13 18	3eqtr4d	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐴 ·_ih ( 𝐵 +_ℎ 𝐶 ) ) = ( ( 𝐴 ·_ih 𝐵 ) + ( 𝐴 ·_ih 𝐶 ) ) )