This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )