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 ∘ H Isom R , T A C

Proof

Step Hyp Ref Expression
1 simpl ⊢ G : B ⟶ 1-1 onto C ∧ ∀ z ∈ B ∀ w ∈ B z S w ↔ G ⁡ z T G ⁡ w → G : B ⟶ 1-1 onto C
2 simpl ⊢ H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ 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 ∘ H : A ⟶ 1-1 onto C
4 1 2 3 syl2anr ⊢ H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y ∧ G : B ⟶ 1-1 onto C ∧ ∀ z ∈ B ∀ w ∈ B z S w ↔ G ⁡ z T G ⁡ w → G ∘ 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 ∧ ∀ z ∈ B ∀ w ∈ B z S w ↔ G ⁡ z T G ⁡ w ∧ x ∈ A ∧ y ∈ A → H : A ⟶ B
7 simprl ⊢ H : A ⟶ 1-1 onto B ∧ G : B ⟶ 1-1 onto C ∧ ∀ z ∈ B ∀ w ∈ B z S w ↔ G ⁡ z T G ⁡ w ∧ x ∈ A ∧ y ∈ A → x ∈ A
8 6 7 ffvelcdmd ⊢ H : A ⟶ 1-1 onto B ∧ G : B ⟶ 1-1 onto C ∧ ∀ z ∈ B ∀ w ∈ B z S w ↔ G ⁡ z T G ⁡ w ∧ x ∈ A ∧ y ∈ A → H ⁡ x ∈ B
9 simprr ⊢ H : A ⟶ 1-1 onto B ∧ G : B ⟶ 1-1 onto C ∧ ∀ z ∈ B ∀ w ∈ B z S w ↔ G ⁡ z T G ⁡ w ∧ x ∈ A ∧ y ∈ A → y ∈ A
10 6 9 ffvelcdmd ⊢ H : A ⟶ 1-1 onto B ∧ G : B ⟶ 1-1 onto C ∧ ∀ z ∈ B ∀ w ∈ B z S w ↔ G ⁡ z T G ⁡ w ∧ x ∈ A ∧ y ∈ A → H ⁡ y ∈ B
11 simplrr ⊢ H : A ⟶ 1-1 onto B ∧ G : B ⟶ 1-1 onto C ∧ ∀ z ∈ B ∀ w ∈ B z S w ↔ G ⁡ z T G ⁡ w ∧ x ∈ A ∧ y ∈ A → ∀ z ∈ B ∀ w ∈ 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 ∈ B ∧ H ⁡ y ∈ B ∧ ∀ z ∈ B ∀ w ∈ 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 ∧ ∀ z ∈ B ∀ w ∈ B z S w ↔ G ⁡ z T G ⁡ w ∧ x ∈ A ∧ y ∈ A → H ⁡ x S H ⁡ y ↔ G ⁡ H ⁡ x T G ⁡ H ⁡ y
22 fvco3 ⊢ H : A ⟶ B ∧ x ∈ A → G ∘ H ⁡ x = G ⁡ H ⁡ x
23 6 7 22 syl2anc ⊢ H : A ⟶ 1-1 onto B ∧ G : B ⟶ 1-1 onto C ∧ ∀ z ∈ B ∀ w ∈ B z S w ↔ G ⁡ z T G ⁡ w ∧ x ∈ A ∧ y ∈ A → G ∘ H ⁡ x = G ⁡ H ⁡ x
24 fvco3 ⊢ H : A ⟶ B ∧ y ∈ A → G ∘ H ⁡ y = G ⁡ H ⁡ y
25 6 9 24 syl2anc ⊢ H : A ⟶ 1-1 onto B ∧ G : B ⟶ 1-1 onto C ∧ ∀ z ∈ B ∀ w ∈ B z S w ↔ G ⁡ z T G ⁡ w ∧ x ∈ A ∧ y ∈ A → G ∘ H ⁡ y = G ⁡ H ⁡ y
26 23 25 breq12d ⊢ H : A ⟶ 1-1 onto B ∧ G : B ⟶ 1-1 onto C ∧ ∀ z ∈ B ∀ w ∈ B z S w ↔ G ⁡ z T G ⁡ w ∧ x ∈ A ∧ y ∈ A → G ∘ H ⁡ x T G ∘ 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 ∧ ∀ z ∈ B ∀ w ∈ B z S w ↔ G ⁡ z T G ⁡ w ∧ x ∈ A ∧ y ∈ A → H ⁡ x S H ⁡ y ↔ G ∘ H ⁡ x T G ∘ H ⁡ y
28 27 bibi2d ⊢ H : A ⟶ 1-1 onto B ∧ G : B ⟶ 1-1 onto C ∧ ∀ z ∈ B ∀ w ∈ B z S w ↔ G ⁡ z T G ⁡ w ∧ x ∈ A ∧ y ∈ A → x R y ↔ H ⁡ x S H ⁡ y ↔ x R y ↔ G ∘ H ⁡ x T G ∘ H ⁡ y
29 28 2ralbidva ⊢ H : A ⟶ 1-1 onto B ∧ G : B ⟶ 1-1 onto C ∧ ∀ z ∈ B ∀ w ∈ B z S w ↔ G ⁡ z T G ⁡ w → ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y ↔ ∀ x ∈ A ∀ y ∈ A x R y ↔ G ∘ H ⁡ x T G ∘ H ⁡ y
30 29 biimpd ⊢ H : A ⟶ 1-1 onto B ∧ G : B ⟶ 1-1 onto C ∧ ∀ z ∈ B ∀ w ∈ B z S w ↔ G ⁡ z T G ⁡ w → ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y → ∀ x ∈ A ∀ y ∈ A x R y ↔ G ∘ H ⁡ x T G ∘ H ⁡ y
31 30 impancom ⊢ H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y → G : B ⟶ 1-1 onto C ∧ ∀ z ∈ B ∀ w ∈ B z S w ↔ G ⁡ z T G ⁡ w → ∀ x ∈ A ∀ y ∈ A x R y ↔ G ∘ H ⁡ x T G ∘ H ⁡ y
32 31 imp ⊢ H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y ∧ G : B ⟶ 1-1 onto C ∧ ∀ z ∈ B ∀ w ∈ B z S w ↔ G ⁡ z T G ⁡ w → ∀ x ∈ A ∀ y ∈ A x R y ↔ G ∘ H ⁡ x T G ∘ H ⁡ y
33 4 32 jca ⊢ H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y ∧ G : B ⟶ 1-1 onto C ∧ ∀ z ∈ B ∀ w ∈ B z S w ↔ G ⁡ z T G ⁡ w → G ∘ H : A ⟶ 1-1 onto C ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ G ∘ H ⁡ x T G ∘ H ⁡ y
34 df-isom ⊢ H Isom R , S A B ↔ H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y
35 df-isom ⊢ G Isom S , T B C ↔ G : B ⟶ 1-1 onto C ∧ ∀ z ∈ B ∀ w ∈ 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 ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y ∧ G : B ⟶ 1-1 onto C ∧ ∀ z ∈ B ∀ w ∈ B z S w ↔ G ⁡ z T G ⁡ w
37 df-isom ⊢ G ∘ H Isom R , T A C ↔ G ∘ H : A ⟶ 1-1 onto C ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ G ∘ H ⁡ x T G ∘ H ⁡ y
38 33 36 37 3imtr4i ⊢ H Isom R , S A B ∧ G Isom S , T B C → G ∘ H Isom R , T A C