Metamath Proof Explorer

Theorem isotr

Description: Composition (transitive) law for isomorphism. Proposition 6.30(3) of TakeutiZaring p. 33. (Contributed by NM, 27-Apr-2004) (Proof shortened by Mario Carneiro, 5-Dec-2016)

Ref Expression
Assertion isotr 
|- ( ( H Isom R , S ( A , B ) /\ G Isom S , T ( B , C ) ) -> ( G o. H ) Isom R , T ( A , C ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( G : B -1-1-onto-> C /\ A. z e. B A. w e. B ( z S w <-> ( G ` z ) T ( G ` w ) ) ) -> G : B -1-1-onto-> C )
2 simpl 
 |-  ( ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) -> H : A -1-1-onto-> B )
3 f1oco 
 |-  ( ( G : B -1-1-onto-> C /\ H : A -1-1-onto-> B ) -> ( G o. H ) : A -1-1-onto-> C )
4 1 2 3 syl2anr 
 |-  ( ( ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) /\ ( G : B -1-1-onto-> C /\ A. z e. B A. w e. B ( z S w <-> ( G ` z ) T ( G ` w ) ) ) ) -> ( G o. H ) : A -1-1-onto-> C )
5 f1of 
 |-  ( H : A -1-1-onto-> B -> H : A --> B )
6 5 ad2antrr 
 |-  ( ( ( H : A -1-1-onto-> B /\ ( G : B -1-1-onto-> C /\ A. z e. B A. w e. B ( z S w <-> ( G ` z ) T ( G ` w ) ) ) ) /\ ( x e. A /\ y e. A ) ) -> H : A --> B )
7 simprl 
 |-  ( ( ( H : A -1-1-onto-> B /\ ( G : B -1-1-onto-> C /\ A. z e. B A. w e. B ( z S w <-> ( G ` z ) T ( G ` w ) ) ) ) /\ ( x e. A /\ y e. A ) ) -> x e. A )
8 6 7 ffvelrnd 
 |-  ( ( ( H : A -1-1-onto-> B /\ ( G : B -1-1-onto-> C /\ A. z e. B A. w e. B ( z S w <-> ( G ` z ) T ( G ` w ) ) ) ) /\ ( x e. A /\ y e. A ) ) -> ( H ` x ) e. B )
9 simprr 
 |-  ( ( ( H : A -1-1-onto-> B /\ ( G : B -1-1-onto-> C /\ A. z e. B A. w e. B ( z S w <-> ( G ` z ) T ( G ` w ) ) ) ) /\ ( x e. A /\ y e. A ) ) -> y e. A )
10 6 9 ffvelrnd 
 |-  ( ( ( H : A -1-1-onto-> B /\ ( G : B -1-1-onto-> C /\ A. z e. B A. w e. B ( z S w <-> ( G ` z ) T ( G ` w ) ) ) ) /\ ( x e. A /\ y e. A ) ) -> ( H ` y ) e. B )
11 simplrr 
 |-  ( ( ( H : A -1-1-onto-> B /\ ( G : B -1-1-onto-> C /\ A. z e. B A. w e. B ( z S w <-> ( G ` z ) T ( G ` w ) ) ) ) /\ ( x e. A /\ y e. A ) ) -> A. z e. B A. w e. B ( z S w <-> ( G ` z ) T ( G ` w ) ) )
12 breq1 
 |-  ( z = ( H ` x ) -> ( z S w <-> ( H ` x ) S w ) )
13 fveq2 
 |-  ( z = ( H ` x ) -> ( G ` z ) = ( G ` ( H ` x ) ) )
14 13 breq1d 
 |-  ( z = ( H ` x ) -> ( ( G ` z ) T ( G ` w ) <-> ( G ` ( H ` x ) ) T ( G ` w ) ) )
15 12 14 bibi12d 
 |-  ( z = ( H ` x ) -> ( ( z S w <-> ( G ` z ) T ( G ` w ) ) <-> ( ( H ` x ) S w <-> ( G ` ( H ` x ) ) T ( G ` w ) ) ) )
16 breq2 
 |-  ( w = ( H ` y ) -> ( ( H ` x ) S w <-> ( H ` x ) S ( H ` y ) ) )
17 fveq2 
 |-  ( w = ( H ` y ) -> ( G ` w ) = ( G ` ( H ` y ) ) )
18 17 breq2d 
 |-  ( w = ( H ` y ) -> ( ( G ` ( H ` x ) ) T ( G ` w ) <-> ( G ` ( H ` x ) ) T ( G ` ( H ` y ) ) ) )
19 16 18 bibi12d 
 |-  ( w = ( H ` y ) -> ( ( ( H ` x ) S w <-> ( G ` ( H ` x ) ) T ( G ` w ) ) <-> ( ( H ` x ) S ( H ` y ) <-> ( G ` ( H ` x ) ) T ( G ` ( H ` y ) ) ) ) )
20 15 19 rspc2va 
 |-  ( ( ( ( H ` x ) e. B /\ ( H ` y ) e. B ) /\ A. z e. B A. w e. B ( z S w <-> ( G ` z ) T ( G ` w ) ) ) -> ( ( H ` x ) S ( H ` y ) <-> ( G ` ( H ` x ) ) T ( G ` ( H ` y ) ) ) )
21 8 10 11 20 syl21anc 
 |-  ( ( ( H : A -1-1-onto-> B /\ ( G : B -1-1-onto-> C /\ A. z e. B A. w e. B ( z S w <-> ( G ` z ) T ( G ` w ) ) ) ) /\ ( x e. A /\ y e. A ) ) -> ( ( H ` x ) S ( H ` y ) <-> ( G ` ( H ` x ) ) T ( G ` ( H ` y ) ) ) )
22 fvco3 
 |-  ( ( H : A --> B /\ x e. A ) -> ( ( G o. H ) ` x ) = ( G ` ( H ` x ) ) )
23 6 7 22 syl2anc 
 |-  ( ( ( H : A -1-1-onto-> B /\ ( G : B -1-1-onto-> C /\ A. z e. B A. w e. B ( z S w <-> ( G ` z ) T ( G ` w ) ) ) ) /\ ( x e. A /\ y e. A ) ) -> ( ( G o. H ) ` x ) = ( G ` ( H ` x ) ) )
24 fvco3 
 |-  ( ( H : A --> B /\ y e. A ) -> ( ( G o. H ) ` y ) = ( G ` ( H ` y ) ) )
25 6 9 24 syl2anc 
 |-  ( ( ( H : A -1-1-onto-> B /\ ( G : B -1-1-onto-> C /\ A. z e. B A. w e. B ( z S w <-> ( G ` z ) T ( G ` w ) ) ) ) /\ ( x e. A /\ y e. A ) ) -> ( ( G o. H ) ` y ) = ( G ` ( H ` y ) ) )
26 23 25 breq12d 
 |-  ( ( ( H : A -1-1-onto-> B /\ ( G : B -1-1-onto-> C /\ A. z e. B A. w e. B ( z S w <-> ( G ` z ) T ( G ` w ) ) ) ) /\ ( x e. A /\ y e. A ) ) -> ( ( ( G o. H ) ` x ) T ( ( G o. H ) ` y ) <-> ( G ` ( H ` x ) ) T ( G ` ( H ` y ) ) ) )
27 21 26 bitr4d 
 |-  ( ( ( H : A -1-1-onto-> B /\ ( G : B -1-1-onto-> C /\ A. z e. B A. w e. B ( z S w <-> ( G ` z ) T ( G ` w ) ) ) ) /\ ( x e. A /\ y e. A ) ) -> ( ( H ` x ) S ( H ` y ) <-> ( ( G o. H ) ` x ) T ( ( G o. H ) ` y ) ) )
28 27 bibi2d 
 |-  ( ( ( H : A -1-1-onto-> B /\ ( G : B -1-1-onto-> C /\ A. z e. B A. w e. B ( z S w <-> ( G ` z ) T ( G ` w ) ) ) ) /\ ( x e. A /\ y e. A ) ) -> ( ( x R y <-> ( H ` x ) S ( H ` y ) ) <-> ( x R y <-> ( ( G o. H ) ` x ) T ( ( G o. H ) ` y ) ) ) )
29 28 2ralbidva 
 |-  ( ( H : A -1-1-onto-> B /\ ( G : B -1-1-onto-> C /\ A. z e. B A. w e. B ( z S w <-> ( G ` z ) T ( G ` w ) ) ) ) -> ( A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) <-> A. x e. A A. y e. A ( x R y <-> ( ( G o. H ) ` x ) T ( ( G o. H ) ` y ) ) ) )
30 29 biimpd 
 |-  ( ( H : A -1-1-onto-> B /\ ( G : B -1-1-onto-> C /\ A. z e. B A. w e. B ( z S w <-> ( G ` z ) T ( G ` w ) ) ) ) -> ( A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) -> A. x e. A A. y e. A ( x R y <-> ( ( G o. H ) ` x ) T ( ( G o. H ) ` y ) ) ) )
31 30 impancom 
 |-  ( ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) -> ( ( G : B -1-1-onto-> C /\ A. z e. B A. w e. B ( z S w <-> ( G ` z ) T ( G ` w ) ) ) -> A. x e. A A. y e. A ( x R y <-> ( ( G o. H ) ` x ) T ( ( G o. H ) ` y ) ) ) )
32 31 imp 
 |-  ( ( ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) /\ ( G : B -1-1-onto-> C /\ A. z e. B A. w e. B ( z S w <-> ( G ` z ) T ( G ` w ) ) ) ) -> A. x e. A A. y e. A ( x R y <-> ( ( G o. H ) ` x ) T ( ( G o. H ) ` y ) ) )
33 4 32 jca 
 |-  ( ( ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) /\ ( G : B -1-1-onto-> C /\ A. z e. B A. w e. B ( z S w <-> ( G ` z ) T ( G ` w ) ) ) ) -> ( ( G o. H ) : A -1-1-onto-> C /\ A. x e. A A. y e. A ( x R y <-> ( ( G o. H ) ` x ) T ( ( G o. H ) ` y ) ) ) )
34 df-isom 
 |-  ( H Isom R , S ( A , B ) <-> ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) )
35 df-isom 
 |-  ( G Isom S , T ( B , C ) <-> ( G : B -1-1-onto-> C /\ A. z e. B A. w e. B ( z S w <-> ( G ` z ) T ( G ` w ) ) ) )
36 34 35 anbi12i 
 |-  ( ( H Isom R , S ( A , B ) /\ G Isom S , T ( B , C ) ) <-> ( ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) /\ ( G : B -1-1-onto-> C /\ A. z e. B A. w e. B ( z S w <-> ( G ` z ) T ( G ` w ) ) ) ) )
37 df-isom 
 |-  ( ( G o. H ) Isom R , T ( A , C ) <-> ( ( G o. H ) : A -1-1-onto-> C /\ A. x e. A A. y e. A ( x R y <-> ( ( G o. H ) ` x ) T ( ( G o. H ) ` y ) ) ) )
38 33 36 37 3imtr4i 
 |-  ( ( H Isom R , S ( A , B ) /\ G Isom S , T ( B , C ) ) -> ( G o. H ) Isom R , T ( A , C ) )