Theorem mulcxplem

Description: Lemma for mulcxp . (Contributed by Mario Carneiro, 2-Aug-2014)

	Ref	Expression
Hypotheses	mulcxp.1	|- ( ph -> A e. CC )
	mulcxp.2	|- ( ph -> C e. CC )
Assertion	mulcxplem	|- ( ph -> ( 0 ^c C ) = ( ( A ^c C ) x. ( 0 ^c C ) ) )

Proof

Step	Hyp	Ref	Expression
1		mulcxp.1	|- ( ph -> A e. CC )
2		mulcxp.2	|- ( ph -> C e. CC )
3		oveq2	|- ( C = 0 -> ( 0 ^c C ) = ( 0 ^c 0 ) )
4		0cn	|- 0 e. CC
5		cxp0	|- ( 0 e. CC -> ( 0 ^c 0 ) = 1 )
6	4 5	ax-mp	|- ( 0 ^c 0 ) = 1
7	3 6	eqtrdi	|- ( C = 0 -> ( 0 ^c C ) = 1 )
8		oveq2	|- ( C = 0 -> ( A ^c C ) = ( A ^c 0 ) )
9	8 7	oveq12d	|- ( C = 0 -> ( ( A ^c C ) x. ( 0 ^c C ) ) = ( ( A ^c 0 ) x. 1 ) )
10	7 9	eqeq12d	|- ( C = 0 -> ( ( 0 ^c C ) = ( ( A ^c C ) x. ( 0 ^c C ) ) <-> 1 = ( ( A ^c 0 ) x. 1 ) ) )
11		cxpcl	|- ( ( A e. CC /\ C e. CC ) -> ( A ^c C ) e. CC )
12	1 2 11	syl2anc	|- ( ph -> ( A ^c C ) e. CC )
13	12	adantr	|- ( ( ph /\ C =/= 0 ) -> ( A ^c C ) e. CC )
14	13	mul01d	|- ( ( ph /\ C =/= 0 ) -> ( ( A ^c C ) x. 0 ) = 0 )
15		0cxp	|- ( ( C e. CC /\ C =/= 0 ) -> ( 0 ^c C ) = 0 )
16	2 15	sylan	|- ( ( ph /\ C =/= 0 ) -> ( 0 ^c C ) = 0 )
17	16	oveq2d	|- ( ( ph /\ C =/= 0 ) -> ( ( A ^c C ) x. ( 0 ^c C ) ) = ( ( A ^c C ) x. 0 ) )
18	14 17 16	3eqtr4rd	|- ( ( ph /\ C =/= 0 ) -> ( 0 ^c C ) = ( ( A ^c C ) x. ( 0 ^c C ) ) )
19		cxp0	|- ( A e. CC -> ( A ^c 0 ) = 1 )
20	1 19	syl	|- ( ph -> ( A ^c 0 ) = 1 )
21	20	oveq1d	|- ( ph -> ( ( A ^c 0 ) x. 1 ) = ( 1 x. 1 ) )
22		1t1e1	|- ( 1 x. 1 ) = 1
23	21 22	eqtr2di	|- ( ph -> 1 = ( ( A ^c 0 ) x. 1 ) )
24	10 18 23	pm2.61ne	|- ( ph -> ( 0 ^c C ) = ( ( A ^c C ) x. ( 0 ^c C ) ) )