Theorem 2arwcatlem5

Description: Lemma for 2arwcat . (Contributed by Zhi Wang, 5-Nov-2025)

	Ref	Expression
Hypotheses	2arwcatlem5.1	|- ( ph -> ( .1. .x. .0. ) = .0. )
	2arwcatlem5.2	|- ( ph -> ( .0. .x. .1. ) = .0. )
	2arwcatlem5.3	|- ( ph -> ( .0. .x. .0. ) e. { .0. , .1. } )
Assertion	2arwcatlem5	|- ( ph -> ( ( .0. .x. .0. ) .x. .0. ) = ( .0. .x. ( .0. .x. .0. ) ) )

Proof

Step	Hyp	Ref	Expression
1		2arwcatlem5.1	|- ( ph -> ( .1. .x. .0. ) = .0. )
2		2arwcatlem5.2	|- ( ph -> ( .0. .x. .1. ) = .0. )
3		2arwcatlem5.3	|- ( ph -> ( .0. .x. .0. ) e. { .0. , .1. } )
4		simpr	|- ( ( ph /\ ( .0. .x. .0. ) = .0. ) -> ( .0. .x. .0. ) = .0. )
5	4	oveq1d	|- ( ( ph /\ ( .0. .x. .0. ) = .0. ) -> ( ( .0. .x. .0. ) .x. .0. ) = ( .0. .x. .0. ) )
6	4	oveq2d	|- ( ( ph /\ ( .0. .x. .0. ) = .0. ) -> ( .0. .x. ( .0. .x. .0. ) ) = ( .0. .x. .0. ) )
7	5 6	eqtr4d	|- ( ( ph /\ ( .0. .x. .0. ) = .0. ) -> ( ( .0. .x. .0. ) .x. .0. ) = ( .0. .x. ( .0. .x. .0. ) ) )
8	1 2	eqtr4d	|- ( ph -> ( .1. .x. .0. ) = ( .0. .x. .1. ) )
9	8	adantr	|- ( ( ph /\ ( .0. .x. .0. ) = .1. ) -> ( .1. .x. .0. ) = ( .0. .x. .1. ) )
10		simpr	|- ( ( ph /\ ( .0. .x. .0. ) = .1. ) -> ( .0. .x. .0. ) = .1. )
11	10	oveq1d	|- ( ( ph /\ ( .0. .x. .0. ) = .1. ) -> ( ( .0. .x. .0. ) .x. .0. ) = ( .1. .x. .0. ) )
12	10	oveq2d	|- ( ( ph /\ ( .0. .x. .0. ) = .1. ) -> ( .0. .x. ( .0. .x. .0. ) ) = ( .0. .x. .1. ) )
13	9 11 12	3eqtr4d	|- ( ( ph /\ ( .0. .x. .0. ) = .1. ) -> ( ( .0. .x. .0. ) .x. .0. ) = ( .0. .x. ( .0. .x. .0. ) ) )
14		ovex	|- ( .0. .x. .0. ) e. _V
15	14	elpr	|- ( ( .0. .x. .0. ) e. { .0. , .1. } <-> ( ( .0. .x. .0. ) = .0. \/ ( .0. .x. .0. ) = .1. ) )
16	3 15	sylib	|- ( ph -> ( ( .0. .x. .0. ) = .0. \/ ( .0. .x. .0. ) = .1. ) )
17	7 13 16	mpjaodan	|- ( ph -> ( ( .0. .x. .0. ) .x. .0. ) = ( .0. .x. ( .0. .x. .0. ) ) )