Metamath Proof Explorer

Theorem 2arwcatlem4

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. )
2arwcatlem4.0 
|- ( ph -> ( .1. ( <. X , Y >. .x. Z ) .0. ) = .0. )
2arwcatlem4.00 
|- ( ph -> ( .0. ( <. X , Y >. .x. Z ) .0. ) e. { .0. , .1. } )
2arwcatlem4.g 
|- ( ph -> ( G = .0. \/ G = .1. ) )
Assertion 2arwcatlem4 
|- ( ph -> ( G ( <. A , B >. .x. C ) F ) e. { .0. , .1. } )

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 2arwcatlem4.0 
 |-  ( ph -> ( .1. ( <. X , Y >. .x. Z ) .0. ) = .0. )
8 2arwcatlem4.00 
 |-  ( ph -> ( .0. ( <. X , Y >. .x. Z ) .0. ) e. { .0. , .1. } )
9 2arwcatlem4.g 
 |-  ( ph -> ( G = .0. \/ G = .1. ) )
10 1 2 opeq12d 
 |-  ( ph -> <. A , B >. = <. X , Y >. )
11 10 3 oveq12d 
 |-  ( ph -> ( <. A , B >. .x. C ) = ( <. X , Y >. .x. Z ) )
12 11 oveqd 
 |-  ( ph -> ( G ( <. A , B >. .x. C ) F ) = ( G ( <. X , Y >. .x. Z ) F ) )
13 simpr 
 |-  ( ( ( ph /\ F = .0. ) /\ G = .0. ) -> G = .0. )
14 simplr 
 |-  ( ( ( ph /\ F = .0. ) /\ G = .0. ) -> F = .0. )
15 13 14 oveq12d 
 |-  ( ( ( ph /\ F = .0. ) /\ G = .0. ) -> ( G ( <. X , Y >. .x. Z ) F ) = ( .0. ( <. X , Y >. .x. Z ) .0. ) )
16 8 ad2antrr 
 |-  ( ( ( ph /\ F = .0. ) /\ G = .0. ) -> ( .0. ( <. X , Y >. .x. Z ) .0. ) e. { .0. , .1. } )
17 15 16 eqeltrd 
 |-  ( ( ( ph /\ F = .0. ) /\ G = .0. ) -> ( G ( <. X , Y >. .x. Z ) F ) e. { .0. , .1. } )
18 simpr 
 |-  ( ( ( ph /\ F = .0. ) /\ G = .1. ) -> G = .1. )
19 simplr 
 |-  ( ( ( ph /\ F = .0. ) /\ G = .1. ) -> F = .0. )
20 18 19 oveq12d 
 |-  ( ( ( ph /\ F = .0. ) /\ G = .1. ) -> ( G ( <. X , Y >. .x. Z ) F ) = ( .1. ( <. X , Y >. .x. Z ) .0. ) )
21 7 ad2antrr 
 |-  ( ( ( ph /\ F = .0. ) /\ G = .1. ) -> ( .1. ( <. X , Y >. .x. Z ) .0. ) = .0. )
22 20 21 eqtrd 
 |-  ( ( ( ph /\ F = .0. ) /\ G = .1. ) -> ( G ( <. X , Y >. .x. Z ) F ) = .0. )
23 ovex 
 |-  ( .1. ( <. X , Y >. .x. Z ) .0. ) e. _V
24 7 23 eqeltrrdi 
 |-  ( ph -> .0. e. _V )
25 prid1g 
 |-  ( .0. e. _V -> .0. e. { .0. , .1. } )
26 24 25 syl 
 |-  ( ph -> .0. e. { .0. , .1. } )
27 26 ad2antrr 
 |-  ( ( ( ph /\ F = .0. ) /\ G = .1. ) -> .0. e. { .0. , .1. } )
28 22 27 eqeltrd 
 |-  ( ( ( ph /\ F = .0. ) /\ G = .1. ) -> ( G ( <. X , Y >. .x. Z ) F ) e. { .0. , .1. } )
29 9 adantr 
 |-  ( ( ph /\ F = .0. ) -> ( G = .0. \/ G = .1. ) )
30 17 28 29 mpjaodan 
 |-  ( ( ph /\ F = .0. ) -> ( G ( <. X , Y >. .x. Z ) F ) e. { .0. , .1. } )
31 simpr 
 |-  ( ( ( ph /\ F = .1. ) /\ G = .0. ) -> G = .0. )
32 simplr 
 |-  ( ( ( ph /\ F = .1. ) /\ G = .0. ) -> F = .1. )
33 31 32 oveq12d 
 |-  ( ( ( ph /\ F = .1. ) /\ G = .0. ) -> ( G ( <. X , Y >. .x. Z ) F ) = ( .0. ( <. X , Y >. .x. Z ) .1. ) )
34 6 ad2antrr 
 |-  ( ( ( ph /\ F = .1. ) /\ G = .0. ) -> ( .0. ( <. X , Y >. .x. Z ) .1. ) = .0. )
35 33 34 eqtrd 
 |-  ( ( ( ph /\ F = .1. ) /\ G = .0. ) -> ( G ( <. X , Y >. .x. Z ) F ) = .0. )
36 26 ad2antrr 
 |-  ( ( ( ph /\ F = .1. ) /\ G = .0. ) -> .0. e. { .0. , .1. } )
37 35 36 eqeltrd 
 |-  ( ( ( ph /\ F = .1. ) /\ G = .0. ) -> ( G ( <. X , Y >. .x. Z ) F ) e. { .0. , .1. } )
38 simpr 
 |-  ( ( ( ph /\ F = .1. ) /\ G = .1. ) -> G = .1. )
39 simplr 
 |-  ( ( ( ph /\ F = .1. ) /\ G = .1. ) -> F = .1. )
40 38 39 oveq12d 
 |-  ( ( ( ph /\ F = .1. ) /\ G = .1. ) -> ( G ( <. X , Y >. .x. Z ) F ) = ( .1. ( <. X , Y >. .x. Z ) .1. ) )
41 5 ad2antrr 
 |-  ( ( ( ph /\ F = .1. ) /\ G = .1. ) -> ( .1. ( <. X , Y >. .x. Z ) .1. ) = .1. )
42 40 41 eqtrd 
 |-  ( ( ( ph /\ F = .1. ) /\ G = .1. ) -> ( G ( <. X , Y >. .x. Z ) F ) = .1. )
43 ovex 
 |-  ( .1. ( <. X , Y >. .x. Z ) .1. ) e. _V
44 5 43 eqeltrrdi 
 |-  ( ph -> .1. e. _V )
45 prid2g 
 |-  ( .1. e. _V -> .1. e. { .0. , .1. } )
46 44 45 syl 
 |-  ( ph -> .1. e. { .0. , .1. } )
47 46 ad2antrr 
 |-  ( ( ( ph /\ F = .1. ) /\ G = .1. ) -> .1. e. { .0. , .1. } )
48 42 47 eqeltrd 
 |-  ( ( ( ph /\ F = .1. ) /\ G = .1. ) -> ( G ( <. X , Y >. .x. Z ) F ) e. { .0. , .1. } )
49 9 adantr 
 |-  ( ( ph /\ F = .1. ) -> ( G = .0. \/ G = .1. ) )
50 37 48 49 mpjaodan 
 |-  ( ( ph /\ F = .1. ) -> ( G ( <. X , Y >. .x. Z ) F ) e. { .0. , .1. } )
51 30 50 4 mpjaodan 
 |-  ( ph -> ( G ( <. X , Y >. .x. Z ) F ) e. { .0. , .1. } )
52 12 51 eqeltrd 
 |-  ( ph -> ( G ( <. A , B >. .x. C ) F ) e. { .0. , .1. } )