Theorem absmulrposd

Description: Specialization of absmuld with absidd . (Contributed by Stanislas Polu, 9-Mar-2020)

	Ref	Expression
Hypotheses	absmulrposd.1	|- ( ph -> 0 <_ A )
	absmulrposd.2	|- ( ph -> A e. RR )
	absmulrposd.3	|- ( ph -> B e. RR )
Assertion	absmulrposd	|- ( ph -> ( abs ` ( A x. B ) ) = ( A x. ( abs ` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		absmulrposd.1	|- ( ph -> 0 <_ A )
2		absmulrposd.2	|- ( ph -> A e. RR )
3		absmulrposd.3	|- ( ph -> B e. RR )
4	2	recnd	|- ( ph -> A e. CC )
5	3	recnd	|- ( ph -> B e. CC )
6	4 5	absmuld	|- ( ph -> ( abs ` ( A x. B ) ) = ( ( abs ` A ) x. ( abs ` B ) ) )
7	2 1	absidd	|- ( ph -> ( abs ` A ) = A )
8	7	oveq1d	|- ( ph -> ( ( abs ` A ) x. ( abs ` B ) ) = ( A x. ( abs ` B ) ) )
9	6 8	eqtrd	|- ( ph -> ( abs ` ( A x. B ) ) = ( A x. ( abs ` B ) ) )