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 syl6bi
 |-  ( ( ( 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 syl5bi
 |-  ( ( 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 )