This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem braadd

Description: Linearity property of bra for addition. (Contributed by NM, 23-May-2006) (New usage is discouraged.)

Ref Expression
Assertion braadd ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → bra ⁡ A ⁡ B + ℎ C = bra ⁡ A ⁡ B + bra ⁡ A ⁡ C

Proof

Step Hyp Ref Expression
1 ax-his2 ⊢ B ∈ ℋ ∧ C ∈ ℋ ∧ A ∈ ℋ → B + ℎ C ⋅ ih A = B ⋅ ih A + C ⋅ ih A
2 1 3comr ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → B + ℎ C ⋅ ih A = B ⋅ ih A + C ⋅ ih A
3 hvaddcl ⊢ B ∈ ℋ ∧ C ∈ ℋ → B + ℎ C ∈ ℋ
4 braval ⊢ A ∈ ℋ ∧ B + ℎ C ∈ ℋ → bra ⁡ A ⁡ B + ℎ C = B + ℎ C ⋅ ih A
5 3 4 sylan2 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → bra ⁡ A ⁡ B + ℎ C = B + ℎ C ⋅ ih A
6 5 3impb ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → bra ⁡ A ⁡ B + ℎ C = B + ℎ C ⋅ ih A
7 braval ⊢ A ∈ ℋ ∧ B ∈ ℋ → bra ⁡ A ⁡ B = B ⋅ ih A
8 7 3adant3 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → bra ⁡ A ⁡ B = B ⋅ ih A
9 braval ⊢ A ∈ ℋ ∧ C ∈ ℋ → bra ⁡ A ⁡ C = C ⋅ ih A
10 9 3adant2 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → bra ⁡ A ⁡ C = C ⋅ ih A
11 8 10 oveq12d ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → bra ⁡ A ⁡ B + bra ⁡ A ⁡ C = B ⋅ ih A + C ⋅ ih A
12 2 6 11 3eqtr4d ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → bra ⁡ A ⁡ B + ℎ C = bra ⁡ A ⁡ B + bra ⁡ A ⁡ C