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

Metamath Proof Explorer

Theorem sqsumi

Description: A sum squared. (Contributed by Steven Nguyen, 16-Sep-2022)

Ref Expression
Hypotheses sqsumi.1 ⊢ 𝐴 ∈ ℂ
sqsumi.2 ⊢ 𝐵 ∈ ℂ
Assertion sqsumi ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) = ( ( ( 𝐴 · 𝐴 ) + ( 𝐵 · 𝐵 ) ) + ( 2 · ( 𝐴 · 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 sqsumi.1 ⊢ 𝐴 ∈ ℂ
2 sqsumi.2 ⊢ 𝐵 ∈ ℂ
3 1 2 1 2 muladdi ⊢ ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) = ( ( ( 𝐴 · 𝐴 ) + ( 𝐵 · 𝐵 ) ) + ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐵 ) ) )
4 1 2 mulcli ⊢ ( 𝐴 · 𝐵 ) ∈ ℂ
5 4 2timesi ⊢ ( 2 · ( 𝐴 · 𝐵 ) ) = ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐵 ) )
6 5 eqcomi ⊢ ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐵 ) ) = ( 2 · ( 𝐴 · 𝐵 ) )
7 6 oveq2i ⊢ ( ( ( 𝐴 · 𝐴 ) + ( 𝐵 · 𝐵 ) ) + ( ( 𝐴 · 𝐵 ) + ( 𝐴 · 𝐵 ) ) ) = ( ( ( 𝐴 · 𝐴 ) + ( 𝐵 · 𝐵 ) ) + ( 2 · ( 𝐴 · 𝐵 ) ) )
8 3 7 eqtri ⊢ ( ( 𝐴 + 𝐵 ) · ( 𝐴 + 𝐵 ) ) = ( ( ( 𝐴 · 𝐴 ) + ( 𝐵 · 𝐵 ) ) + ( 2 · ( 𝐴 · 𝐵 ) ) )