Metamath Proof Explorer

Theorem satffunlem

Description: Lemma for satffunlem1lem1 and satffunlem2lem1 . (Contributed by AV, 27-Oct-2023)

Ref Expression
Assertion satffunlem 
|- ( ( ( Fun Z /\ ( s e. Z /\ r e. Z ) /\ ( u e. Z /\ v e. Z ) ) /\ ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) /\ ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) -> y = w )

Proof

Step Hyp Ref Expression
1 eqtr2 
 |-  ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ x = ( ( 1st ` s ) |g ( 1st ` r ) ) ) -> ( ( 1st ` u ) |g ( 1st ` v ) ) = ( ( 1st ` s ) |g ( 1st ` r ) ) )
2 fvex 
 |-  ( 1st ` u ) e. _V
3 fvex 
 |-  ( 1st ` v ) e. _V
4 gonafv 
 |-  ( ( ( 1st ` u ) e. _V /\ ( 1st ` v ) e. _V ) -> ( ( 1st ` u ) |g ( 1st ` v ) ) = <. 1o , <. ( 1st ` u ) , ( 1st ` v ) >. >. )
5 2 3 4 mp2an 
 |-  ( ( 1st ` u ) |g ( 1st ` v ) ) = <. 1o , <. ( 1st ` u ) , ( 1st ` v ) >. >.
6 fvex 
 |-  ( 1st ` s ) e. _V
7 fvex 
 |-  ( 1st ` r ) e. _V
8 gonafv 
 |-  ( ( ( 1st ` s ) e. _V /\ ( 1st ` r ) e. _V ) -> ( ( 1st ` s ) |g ( 1st ` r ) ) = <. 1o , <. ( 1st ` s ) , ( 1st ` r ) >. >. )
9 6 7 8 mp2an 
 |-  ( ( 1st ` s ) |g ( 1st ` r ) ) = <. 1o , <. ( 1st ` s ) , ( 1st ` r ) >. >.
10 5 9 eqeq12i 
 |-  ( ( ( 1st ` u ) |g ( 1st ` v ) ) = ( ( 1st ` s ) |g ( 1st ` r ) ) <-> <. 1o , <. ( 1st ` u ) , ( 1st ` v ) >. >. = <. 1o , <. ( 1st ` s ) , ( 1st ` r ) >. >. )
11 1oex 
 |-  1o e. _V
12 opex 
 |-  <. ( 1st ` u ) , ( 1st ` v ) >. e. _V
13 11 12 opth 
 |-  ( <. 1o , <. ( 1st ` u ) , ( 1st ` v ) >. >. = <. 1o , <. ( 1st ` s ) , ( 1st ` r ) >. >. <-> ( 1o = 1o /\ <. ( 1st ` u ) , ( 1st ` v ) >. = <. ( 1st ` s ) , ( 1st ` r ) >. ) )
14 2 3 opth 
 |-  ( <. ( 1st ` u ) , ( 1st ` v ) >. = <. ( 1st ` s ) , ( 1st ` r ) >. <-> ( ( 1st ` u ) = ( 1st ` s ) /\ ( 1st ` v ) = ( 1st ` r ) ) )
15 14 anbi2i 
 |-  ( ( 1o = 1o /\ <. ( 1st ` u ) , ( 1st ` v ) >. = <. ( 1st ` s ) , ( 1st ` r ) >. ) <-> ( 1o = 1o /\ ( ( 1st ` u ) = ( 1st ` s ) /\ ( 1st ` v ) = ( 1st ` r ) ) ) )
16 10 13 15 3bitri 
 |-  ( ( ( 1st ` u ) |g ( 1st ` v ) ) = ( ( 1st ` s ) |g ( 1st ` r ) ) <-> ( 1o = 1o /\ ( ( 1st ` u ) = ( 1st ` s ) /\ ( 1st ` v ) = ( 1st ` r ) ) ) )
17 funfv1st2nd 
 |-  ( ( Fun Z /\ s e. Z ) -> ( Z ` ( 1st ` s ) ) = ( 2nd ` s ) )
18 17 ex 
 |-  ( Fun Z -> ( s e. Z -> ( Z ` ( 1st ` s ) ) = ( 2nd ` s ) ) )
19 funfv1st2nd 
 |-  ( ( Fun Z /\ r e. Z ) -> ( Z ` ( 1st ` r ) ) = ( 2nd ` r ) )
20 19 ex 
 |-  ( Fun Z -> ( r e. Z -> ( Z ` ( 1st ` r ) ) = ( 2nd ` r ) ) )
21 18 20 anim12d 
 |-  ( Fun Z -> ( ( s e. Z /\ r e. Z ) -> ( ( Z ` ( 1st ` s ) ) = ( 2nd ` s ) /\ ( Z ` ( 1st ` r ) ) = ( 2nd ` r ) ) ) )
22 funfv1st2nd 
 |-  ( ( Fun Z /\ u e. Z ) -> ( Z ` ( 1st ` u ) ) = ( 2nd ` u ) )
23 22 ex 
 |-  ( Fun Z -> ( u e. Z -> ( Z ` ( 1st ` u ) ) = ( 2nd ` u ) ) )
24 funfv1st2nd 
 |-  ( ( Fun Z /\ v e. Z ) -> ( Z ` ( 1st ` v ) ) = ( 2nd ` v ) )
25 24 ex 
 |-  ( Fun Z -> ( v e. Z -> ( Z ` ( 1st ` v ) ) = ( 2nd ` v ) ) )
26 23 25 anim12d 
 |-  ( Fun Z -> ( ( u e. Z /\ v e. Z ) -> ( ( Z ` ( 1st ` u ) ) = ( 2nd ` u ) /\ ( Z ` ( 1st ` v ) ) = ( 2nd ` v ) ) ) )
27 fveq2 
 |-  ( ( 1st ` s ) = ( 1st ` u ) -> ( Z ` ( 1st ` s ) ) = ( Z ` ( 1st ` u ) ) )
28 27 eqcoms 
 |-  ( ( 1st ` u ) = ( 1st ` s ) -> ( Z ` ( 1st ` s ) ) = ( Z ` ( 1st ` u ) ) )
29 28 adantr 
 |-  ( ( ( 1st ` u ) = ( 1st ` s ) /\ ( 1st ` v ) = ( 1st ` r ) ) -> ( Z ` ( 1st ` s ) ) = ( Z ` ( 1st ` u ) ) )
30 29 eqeq1d 
 |-  ( ( ( 1st ` u ) = ( 1st ` s ) /\ ( 1st ` v ) = ( 1st ` r ) ) -> ( ( Z ` ( 1st ` s ) ) = ( 2nd ` s ) <-> ( Z ` ( 1st ` u ) ) = ( 2nd ` s ) ) )
31 fveq2 
 |-  ( ( 1st ` r ) = ( 1st ` v ) -> ( Z ` ( 1st ` r ) ) = ( Z ` ( 1st ` v ) ) )
32 31 eqcoms 
 |-  ( ( 1st ` v ) = ( 1st ` r ) -> ( Z ` ( 1st ` r ) ) = ( Z ` ( 1st ` v ) ) )
33 32 adantl 
 |-  ( ( ( 1st ` u ) = ( 1st ` s ) /\ ( 1st ` v ) = ( 1st ` r ) ) -> ( Z ` ( 1st ` r ) ) = ( Z ` ( 1st ` v ) ) )
34 33 eqeq1d 
 |-  ( ( ( 1st ` u ) = ( 1st ` s ) /\ ( 1st ` v ) = ( 1st ` r ) ) -> ( ( Z ` ( 1st ` r ) ) = ( 2nd ` r ) <-> ( Z ` ( 1st ` v ) ) = ( 2nd ` r ) ) )
35 30 34 anbi12d 
 |-  ( ( ( 1st ` u ) = ( 1st ` s ) /\ ( 1st ` v ) = ( 1st ` r ) ) -> ( ( ( Z ` ( 1st ` s ) ) = ( 2nd ` s ) /\ ( Z ` ( 1st ` r ) ) = ( 2nd ` r ) ) <-> ( ( Z ` ( 1st ` u ) ) = ( 2nd ` s ) /\ ( Z ` ( 1st ` v ) ) = ( 2nd ` r ) ) ) )
36 35 anbi1d 
 |-  ( ( ( 1st ` u ) = ( 1st ` s ) /\ ( 1st ` v ) = ( 1st ` r ) ) -> ( ( ( ( Z ` ( 1st ` s ) ) = ( 2nd ` s ) /\ ( Z ` ( 1st ` r ) ) = ( 2nd ` r ) ) /\ ( ( Z ` ( 1st ` u ) ) = ( 2nd ` u ) /\ ( Z ` ( 1st ` v ) ) = ( 2nd ` v ) ) ) <-> ( ( ( Z ` ( 1st ` u ) ) = ( 2nd ` s ) /\ ( Z ` ( 1st ` v ) ) = ( 2nd ` r ) ) /\ ( ( Z ` ( 1st ` u ) ) = ( 2nd ` u ) /\ ( Z ` ( 1st ` v ) ) = ( 2nd ` v ) ) ) ) )
37 eqtr2 
 |-  ( ( ( Z ` ( 1st ` u ) ) = ( 2nd ` s ) /\ ( Z ` ( 1st ` u ) ) = ( 2nd ` u ) ) -> ( 2nd ` s ) = ( 2nd ` u ) )
38 37 ad2ant2r 
 |-  ( ( ( ( Z ` ( 1st ` u ) ) = ( 2nd ` s ) /\ ( Z ` ( 1st ` v ) ) = ( 2nd ` r ) ) /\ ( ( Z ` ( 1st ` u ) ) = ( 2nd ` u ) /\ ( Z ` ( 1st ` v ) ) = ( 2nd ` v ) ) ) -> ( 2nd ` s ) = ( 2nd ` u ) )
39 eqtr2 
 |-  ( ( ( Z ` ( 1st ` v ) ) = ( 2nd ` r ) /\ ( Z ` ( 1st ` v ) ) = ( 2nd ` v ) ) -> ( 2nd ` r ) = ( 2nd ` v ) )
40 39 ad2ant2l 
 |-  ( ( ( ( Z ` ( 1st ` u ) ) = ( 2nd ` s ) /\ ( Z ` ( 1st ` v ) ) = ( 2nd ` r ) ) /\ ( ( Z ` ( 1st ` u ) ) = ( 2nd ` u ) /\ ( Z ` ( 1st ` v ) ) = ( 2nd ` v ) ) ) -> ( 2nd ` r ) = ( 2nd ` v ) )
41 38 40 ineq12d 
 |-  ( ( ( ( Z ` ( 1st ` u ) ) = ( 2nd ` s ) /\ ( Z ` ( 1st ` v ) ) = ( 2nd ` r ) ) /\ ( ( Z ` ( 1st ` u ) ) = ( 2nd ` u ) /\ ( Z ` ( 1st ` v ) ) = ( 2nd ` v ) ) ) -> ( ( 2nd ` s ) i^i ( 2nd ` r ) ) = ( ( 2nd ` u ) i^i ( 2nd ` v ) ) )
42 36 41 biimtrdi 
 |-  ( ( ( 1st ` u ) = ( 1st ` s ) /\ ( 1st ` v ) = ( 1st ` r ) ) -> ( ( ( ( Z ` ( 1st ` s ) ) = ( 2nd ` s ) /\ ( Z ` ( 1st ` r ) ) = ( 2nd ` r ) ) /\ ( ( Z ` ( 1st ` u ) ) = ( 2nd ` u ) /\ ( Z ` ( 1st ` v ) ) = ( 2nd ` v ) ) ) -> ( ( 2nd ` s ) i^i ( 2nd ` r ) ) = ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) )
43 42 com12 
 |-  ( ( ( ( Z ` ( 1st ` s ) ) = ( 2nd ` s ) /\ ( Z ` ( 1st ` r ) ) = ( 2nd ` r ) ) /\ ( ( Z ` ( 1st ` u ) ) = ( 2nd ` u ) /\ ( Z ` ( 1st ` v ) ) = ( 2nd ` v ) ) ) -> ( ( ( 1st ` u ) = ( 1st ` s ) /\ ( 1st ` v ) = ( 1st ` r ) ) -> ( ( 2nd ` s ) i^i ( 2nd ` r ) ) = ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) )
44 43 a1i 
 |-  ( Fun Z -> ( ( ( ( Z ` ( 1st ` s ) ) = ( 2nd ` s ) /\ ( Z ` ( 1st ` r ) ) = ( 2nd ` r ) ) /\ ( ( Z ` ( 1st ` u ) ) = ( 2nd ` u ) /\ ( Z ` ( 1st ` v ) ) = ( 2nd ` v ) ) ) -> ( ( ( 1st ` u ) = ( 1st ` s ) /\ ( 1st ` v ) = ( 1st ` r ) ) -> ( ( 2nd ` s ) i^i ( 2nd ` r ) ) = ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) )
45 21 26 44 syl2and 
 |-  ( Fun Z -> ( ( ( s e. Z /\ r e. Z ) /\ ( u e. Z /\ v e. Z ) ) -> ( ( ( 1st ` u ) = ( 1st ` s ) /\ ( 1st ` v ) = ( 1st ` r ) ) -> ( ( 2nd ` s ) i^i ( 2nd ` r ) ) = ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) )
46 45 expd 
 |-  ( Fun Z -> ( ( s e. Z /\ r e. Z ) -> ( ( u e. Z /\ v e. Z ) -> ( ( ( 1st ` u ) = ( 1st ` s ) /\ ( 1st ` v ) = ( 1st ` r ) ) -> ( ( 2nd ` s ) i^i ( 2nd ` r ) ) = ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) )
47 46 3imp1 
 |-  ( ( ( Fun Z /\ ( s e. Z /\ r e. Z ) /\ ( u e. Z /\ v e. Z ) ) /\ ( ( 1st ` u ) = ( 1st ` s ) /\ ( 1st ` v ) = ( 1st ` r ) ) ) -> ( ( 2nd ` s ) i^i ( 2nd ` r ) ) = ( ( 2nd ` u ) i^i ( 2nd ` v ) ) )
48 47 difeq2d 
 |-  ( ( ( Fun Z /\ ( s e. Z /\ r e. Z ) /\ ( u e. Z /\ v e. Z ) ) /\ ( ( 1st ` u ) = ( 1st ` s ) /\ ( 1st ` v ) = ( 1st ` r ) ) ) -> ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) )
49 48 adantr 
 |-  ( ( ( ( Fun Z /\ ( s e. Z /\ r e. Z ) /\ ( u e. Z /\ v e. Z ) ) /\ ( ( 1st ` u ) = ( 1st ` s ) /\ ( 1st ` v ) = ( 1st ` r ) ) ) /\ ( y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) /\ w = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) -> ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) )
50 eqeq12 
 |-  ( ( y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) /\ w = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) -> ( y = w <-> ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) )
51 50 adantl 
 |-  ( ( ( ( Fun Z /\ ( s e. Z /\ r e. Z ) /\ ( u e. Z /\ v e. Z ) ) /\ ( ( 1st ` u ) = ( 1st ` s ) /\ ( 1st ` v ) = ( 1st ` r ) ) ) /\ ( y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) /\ w = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) -> ( y = w <-> ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) )
52 49 51 mpbird 
 |-  ( ( ( ( Fun Z /\ ( s e. Z /\ r e. Z ) /\ ( u e. Z /\ v e. Z ) ) /\ ( ( 1st ` u ) = ( 1st ` s ) /\ ( 1st ` v ) = ( 1st ` r ) ) ) /\ ( y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) /\ w = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) -> y = w )
53 52 exp43 
 |-  ( ( Fun Z /\ ( s e. Z /\ r e. Z ) /\ ( u e. Z /\ v e. Z ) ) -> ( ( ( 1st ` u ) = ( 1st ` s ) /\ ( 1st ` v ) = ( 1st ` r ) ) -> ( y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) -> ( w = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) -> y = w ) ) ) )
54 53 adantld 
 |-  ( ( Fun Z /\ ( s e. Z /\ r e. Z ) /\ ( u e. Z /\ v e. Z ) ) -> ( ( 1o = 1o /\ ( ( 1st ` u ) = ( 1st ` s ) /\ ( 1st ` v ) = ( 1st ` r ) ) ) -> ( y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) -> ( w = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) -> y = w ) ) ) )
55 16 54 biimtrid 
 |-  ( ( Fun Z /\ ( s e. Z /\ r e. Z ) /\ ( u e. Z /\ v e. Z ) ) -> ( ( ( 1st ` u ) |g ( 1st ` v ) ) = ( ( 1st ` s ) |g ( 1st ` r ) ) -> ( y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) -> ( w = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) -> y = w ) ) ) )
56 1 55 syl5 
 |-  ( ( Fun Z /\ ( s e. Z /\ r e. Z ) /\ ( u e. Z /\ v e. Z ) ) -> ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ x = ( ( 1st ` s ) |g ( 1st ` r ) ) ) -> ( y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) -> ( w = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) -> y = w ) ) ) )
57 56 expd 
 |-  ( ( Fun Z /\ ( s e. Z /\ r e. Z ) /\ ( u e. Z /\ v e. Z ) ) -> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) -> ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) -> ( y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) -> ( w = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) -> y = w ) ) ) ) )
58 57 com35 
 |-  ( ( Fun Z /\ ( s e. Z /\ r e. Z ) /\ ( u e. Z /\ v e. Z ) ) -> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) -> ( w = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) -> ( y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) -> ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) -> y = w ) ) ) ) )
59 58 impd 
 |-  ( ( Fun Z /\ ( s e. Z /\ r e. Z ) /\ ( u e. Z /\ v e. Z ) ) -> ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) -> ( y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) -> ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) -> y = w ) ) ) )
60 59 com24 
 |-  ( ( Fun Z /\ ( s e. Z /\ r e. Z ) /\ ( u e. Z /\ v e. Z ) ) -> ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) -> ( y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) -> ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) -> y = w ) ) ) )
61 60 impd 
 |-  ( ( Fun Z /\ ( s e. Z /\ r e. Z ) /\ ( u e. Z /\ v e. Z ) ) -> ( ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) -> ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) -> y = w ) ) )
62 61 3imp 
 |-  ( ( ( Fun Z /\ ( s e. Z /\ r e. Z ) /\ ( u e. Z /\ v e. Z ) ) /\ ( x = ( ( 1st ` s ) |g ( 1st ` r ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` s ) i^i ( 2nd ` r ) ) ) ) /\ ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ w = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) -> y = w )