Theorem resubdi

Description: Distribution of multiplication over real subtraction. (Contributed by Steven Nguyen, 3-Jun-2023)

	Ref	Expression
Assertion	resubdi	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A x. ( B -R C ) ) = ( ( A x. B ) -R ( A x. C ) ) )

Proof

Step	Hyp	Ref	Expression
1		remulcl	|- ( ( A e. RR /\ C e. RR ) -> ( A x. C ) e. RR )
2	1	3adant2	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A x. C ) e. RR )
3		simp1	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A e. RR )
4		rersubcl	|- ( ( B e. RR /\ C e. RR ) -> ( B -R C ) e. RR )
5	4	3adant1	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B -R C ) e. RR )
6	3 5	remulcld	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A x. ( B -R C ) ) e. RR )
7	3	recnd	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A e. CC )
8		simp3	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> C e. RR )
9	8	recnd	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> C e. CC )
10	5	recnd	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B -R C ) e. CC )
11	7 9 10	adddid	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A x. ( C + ( B -R C ) ) ) = ( ( A x. C ) + ( A x. ( B -R C ) ) ) )
12		repncan3	|- ( ( C e. RR /\ B e. RR ) -> ( C + ( B -R C ) ) = B )
13	12	ancoms	|- ( ( B e. RR /\ C e. RR ) -> ( C + ( B -R C ) ) = B )
14	13	3adant1	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( C + ( B -R C ) ) = B )
15	14	oveq2d	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A x. ( C + ( B -R C ) ) ) = ( A x. B ) )
16	11 15	eqtr3d	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A x. C ) + ( A x. ( B -R C ) ) ) = ( A x. B ) )
17	2 6 16	reladdrsub	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A x. ( B -R C ) ) = ( ( A x. B ) -R ( A x. C ) ) )