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⋅ihA=B⋅ihA+C⋅ihA
2 1 3comr ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→B+ℎC⋅ihA=B⋅ihA+C⋅ihA
3 hvaddcl ⊢B∈ℋ∧C∈ℋ→B+ℎC∈ℋ
4 braval ⊢A∈ℋ∧B+ℎC∈ℋ→bra⁡A⁡B+ℎC=B+ℎC⋅ihA
5 3 4 sylan2 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→bra⁡A⁡B+ℎC=B+ℎC⋅ihA
6 5 3impb ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→bra⁡A⁡B+ℎC=B+ℎC⋅ihA
7 braval ⊢A∈ℋ∧B∈ℋ→bra⁡A⁡B=B⋅ihA
8 7 3adant3 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→bra⁡A⁡B=B⋅ihA
9 braval ⊢A∈ℋ∧C∈ℋ→bra⁡A⁡C=C⋅ihA
10 9 3adant2 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→bra⁡A⁡C=C⋅ihA
11 8 10 oveq12d ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→bra⁡A⁡B+bra⁡A⁡C=B⋅ihA+C⋅ihA
12 2 6 11 3eqtr4d ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→bra⁡A⁡B+ℎC=bra⁡A⁡B+bra⁡A⁡C