Theorem sqsumi

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

	Ref	Expression
Hypotheses	sqsumi.1	|- A e. CC
	sqsumi.2	|- B e. CC
Assertion	sqsumi	|- ( ( A + B ) x. ( A + B ) ) = ( ( ( A x. A ) + ( B x. B ) ) + ( 2 x. ( A x. B ) ) )

Proof

Step	Hyp	Ref	Expression
1		sqsumi.1	|- A e. CC
2		sqsumi.2	|- B e. CC
3	1 2 1 2	muladdi	|- ( ( A + B ) x. ( A + B ) ) = ( ( ( A x. A ) + ( B x. B ) ) + ( ( A x. B ) + ( A x. B ) ) )
4	1 2	mulcli	|- ( A x. B ) e. CC
5	4	2timesi	|- ( 2 x. ( A x. B ) ) = ( ( A x. B ) + ( A x. B ) )
6	5	eqcomi	|- ( ( A x. B ) + ( A x. B ) ) = ( 2 x. ( A x. B ) )
7	6	oveq2i	|- ( ( ( A x. A ) + ( B x. B ) ) + ( ( A x. B ) + ( A x. B ) ) ) = ( ( ( A x. A ) + ( B x. B ) ) + ( 2 x. ( A x. B ) ) )
8	3 7	eqtri	|- ( ( A + B ) x. ( A + B ) ) = ( ( ( A x. A ) + ( B x. B ) ) + ( 2 x. ( A x. B ) ) )