Theorem xpcoid

Description: Composition of two Cartesian squares. (Contributed by Thierry Arnoux, 14-Jan-2018)

	Ref	Expression
Assertion	xpcoid	|- ( ( A X. A ) o. ( A X. A ) ) = ( A X. A )

Proof

Step	Hyp	Ref	Expression
1		co01	|- ( (/) o. (/) ) = (/)
2		id	|- ( A = (/) -> A = (/) )
3	2	sqxpeqd	|- ( A = (/) -> ( A X. A ) = ( (/) X. (/) ) )
4		0xp	|- ( (/) X. (/) ) = (/)
5	3 4	eqtrdi	|- ( A = (/) -> ( A X. A ) = (/) )
6	5 5	coeq12d	|- ( A = (/) -> ( ( A X. A ) o. ( A X. A ) ) = ( (/) o. (/) ) )
7	1 6 5	3eqtr4a	|- ( A = (/) -> ( ( A X. A ) o. ( A X. A ) ) = ( A X. A ) )
8		xpco	|- ( A =/= (/) -> ( ( A X. A ) o. ( A X. A ) ) = ( A X. A ) )
9	7 8	pm2.61ine	|- ( ( A X. A ) o. ( A X. A ) ) = ( A X. A )