Theorem 2arwcatlem2

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

	Ref	Expression
Hypotheses	2arwcatlem2.a	|- ( ph -> A = X )
	2arwcatlem2.b	|- ( ph -> B = Y )
	2arwcatlem2.c	|- ( ph -> C = Z )
	2arwcatlem2.f	|- ( ph -> ( F = .0. \/ F = .1. ) )
	2arwcatlem2.1	|- ( ph -> ( .1. ( <. X , Y >. .x. Z ) .1. ) = .1. )
	2arwcatlem2.0	|- ( ph -> ( .1. ( <. X , Y >. .x. Z ) .0. ) = .0. )
Assertion	2arwcatlem2	|- ( ph -> ( .1. ( <. A , B >. .x. C ) F ) = F )

Proof

Step	Hyp	Ref	Expression
1		2arwcatlem2.a	|- ( ph -> A = X )
2		2arwcatlem2.b	|- ( ph -> B = Y )
3		2arwcatlem2.c	|- ( ph -> C = Z )
4		2arwcatlem2.f	|- ( ph -> ( F = .0. \/ F = .1. ) )
5		2arwcatlem2.1	|- ( ph -> ( .1. ( <. X , Y >. .x. Z ) .1. ) = .1. )
6		2arwcatlem2.0	|- ( ph -> ( .1. ( <. X , Y >. .x. Z ) .0. ) = .0. )
7	1 2	opeq12d	|- ( ph -> <. A , B >. = <. X , Y >. )
8	7 3	oveq12d	|- ( ph -> ( <. A , B >. .x. C ) = ( <. X , Y >. .x. Z ) )
9	8	oveqd	|- ( ph -> ( .1. ( <. A , B >. .x. C ) F ) = ( .1. ( <. X , Y >. .x. Z ) F ) )
10	6	adantr	|- ( ( ph /\ F = .0. ) -> ( .1. ( <. X , Y >. .x. Z ) .0. ) = .0. )
11		simpr	|- ( ( ph /\ F = .0. ) -> F = .0. )
12	11	oveq2d	|- ( ( ph /\ F = .0. ) -> ( .1. ( <. X , Y >. .x. Z ) F ) = ( .1. ( <. X , Y >. .x. Z ) .0. ) )
13	10 12 11	3eqtr4d	|- ( ( ph /\ F = .0. ) -> ( .1. ( <. X , Y >. .x. Z ) F ) = F )
14	5	adantr	|- ( ( ph /\ F = .1. ) -> ( .1. ( <. X , Y >. .x. Z ) .1. ) = .1. )
15		simpr	|- ( ( ph /\ F = .1. ) -> F = .1. )
16	15	oveq2d	|- ( ( ph /\ F = .1. ) -> ( .1. ( <. X , Y >. .x. Z ) F ) = ( .1. ( <. X , Y >. .x. Z ) .1. ) )
17	14 16 15	3eqtr4d	|- ( ( ph /\ F = .1. ) -> ( .1. ( <. X , Y >. .x. Z ) F ) = F )
18	13 17 4	mpjaodan	|- ( ph -> ( .1. ( <. X , Y >. .x. Z ) F ) = F )
19	9 18	eqtrd	|- ( ph -> ( .1. ( <. A , B >. .x. C ) F ) = F )