Metamath Proof Explorer

Theorem 2arwcatlem3

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. )
2arwcatlem3.0 
|- ( ph -> ( .0. ( <. X , Y >. .x. Z ) .1. ) = .0. )
Assertion 2arwcatlem3 
|- ( ph -> ( F ( <. A , B >. .x. C ) .1. ) = 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 2arwcatlem3.0 
 |-  ( ph -> ( .0. ( <. X , Y >. .x. Z ) .1. ) = .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 -> ( F ( <. A , B >. .x. C ) .1. ) = ( F ( <. X , Y >. .x. Z ) .1. ) )
10 6 adantr 
 |-  ( ( ph /\ F = .0. ) -> ( .0. ( <. X , Y >. .x. Z ) .1. ) = .0. )
11 simpr 
 |-  ( ( ph /\ F = .0. ) -> F = .0. )
12 11 oveq1d 
 |-  ( ( ph /\ F = .0. ) -> ( F ( <. X , Y >. .x. Z ) .1. ) = ( .0. ( <. X , Y >. .x. Z ) .1. ) )
13 10 12 11 3eqtr4d 
 |-  ( ( ph /\ F = .0. ) -> ( F ( <. X , Y >. .x. Z ) .1. ) = F )
14 5 adantr 
 |-  ( ( ph /\ F = .1. ) -> ( .1. ( <. X , Y >. .x. Z ) .1. ) = .1. )
15 simpr 
 |-  ( ( ph /\ F = .1. ) -> F = .1. )
16 15 oveq1d 
 |-  ( ( ph /\ F = .1. ) -> ( F ( <. X , Y >. .x. Z ) .1. ) = ( .1. ( <. X , Y >. .x. Z ) .1. ) )
17 14 16 15 3eqtr4d 
 |-  ( ( ph /\ F = .1. ) -> ( F ( <. X , Y >. .x. Z ) .1. ) = F )
18 13 17 4 mpjaodan 
 |-  ( ph -> ( F ( <. X , Y >. .x. Z ) .1. ) = F )
19 9 18 eqtrd 
 |-  ( ph -> ( F ( <. A , B >. .x. C ) .1. ) = F )