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 ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐺 Isom 𝑆 , 𝑇 ( 𝐵 , 𝐶 ) ) → ( 𝐺 ∘ 𝐻 ) Isom 𝑅 , 𝑇 ( 𝐴 , 𝐶 ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐺 : 𝐵 –1-1-onto→ 𝐶 ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝑆 𝑤 ↔ ( 𝐺 ‘ 𝑧 ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) ) → 𝐺 : 𝐵 –1-1-onto→ 𝐶 )
2 simpl ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) → 𝐻 : 𝐴 –1-1-onto→ 𝐵 )
3 f1oco ⊢ ( ( 𝐺 : 𝐵 –1-1-onto→ 𝐶 ∧ 𝐻 : 𝐴 –1-1-onto→ 𝐵 ) → ( 𝐺 ∘ 𝐻 ) : 𝐴 –1-1-onto→ 𝐶 )
4 1 2 3 syl2anr ⊢ ( ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ∧ ( 𝐺 : 𝐵 –1-1-onto→ 𝐶 ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝑆 𝑤 ↔ ( 𝐺 ‘ 𝑧 ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) ) ) → ( 𝐺 ∘ 𝐻 ) : 𝐴 –1-1-onto→ 𝐶 )
5 f1of ⊢ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 → 𝐻 : 𝐴 ⟶ 𝐵 )
6 5 ad2antrr ⊢ ( ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝐺 : 𝐵 –1-1-onto→ 𝐶 ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝑆 𝑤 ↔ ( 𝐺 ‘ 𝑧 ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → 𝐻 : 𝐴 ⟶ 𝐵 )
7 simprl ⊢ ( ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝐺 : 𝐵 –1-1-onto→ 𝐶 ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝑆 𝑤 ↔ ( 𝐺 ‘ 𝑧 ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → 𝑥 ∈ 𝐴 )
8 6 7 ffvelcdmd ⊢ ( ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝐺 : 𝐵 –1-1-onto→ 𝐶 ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝑆 𝑤 ↔ ( 𝐺 ‘ 𝑧 ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝐻 ‘ 𝑥 ) ∈ 𝐵 )
9 simprr ⊢ ( ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝐺 : 𝐵 –1-1-onto→ 𝐶 ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝑆 𝑤 ↔ ( 𝐺 ‘ 𝑧 ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → 𝑦 ∈ 𝐴 )
10 6 9 ffvelcdmd ⊢ ( ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝐺 : 𝐵 –1-1-onto→ 𝐶 ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝑆 𝑤 ↔ ( 𝐺 ‘ 𝑧 ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝐻 ‘ 𝑦 ) ∈ 𝐵 )
11 simplrr ⊢ ( ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝐺 : 𝐵 –1-1-onto→ 𝐶 ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝑆 𝑤 ↔ ( 𝐺 ‘ 𝑧 ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝑆 𝑤 ↔ ( 𝐺 ‘ 𝑧 ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) )
12 breq1 ⊢ ( 𝑧 = ( 𝐻 ‘ 𝑥 ) → ( 𝑧 𝑆 𝑤 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 𝑤 ) )
13 fveq2 ⊢ ( 𝑧 = ( 𝐻 ‘ 𝑥 ) → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ ( 𝐻 ‘ 𝑥 ) ) )
14 13 breq1d ⊢ ( 𝑧 = ( 𝐻 ‘ 𝑥 ) → ( ( 𝐺 ‘ 𝑧 ) 𝑇 ( 𝐺 ‘ 𝑤 ) ↔ ( 𝐺 ‘ ( 𝐻 ‘ 𝑥 ) ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) )
15 12 14 bibi12d ⊢ ( 𝑧 = ( 𝐻 ‘ 𝑥 ) → ( ( 𝑧 𝑆 𝑤 ↔ ( 𝐺 ‘ 𝑧 ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) ↔ ( ( 𝐻 ‘ 𝑥 ) 𝑆 𝑤 ↔ ( 𝐺 ‘ ( 𝐻 ‘ 𝑥 ) ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) ) )
16 breq2 ⊢ ( 𝑤 = ( 𝐻 ‘ 𝑦 ) → ( ( 𝐻 ‘ 𝑥 ) 𝑆 𝑤 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) )
17 fveq2 ⊢ ( 𝑤 = ( 𝐻 ‘ 𝑦 ) → ( 𝐺 ‘ 𝑤 ) = ( 𝐺 ‘ ( 𝐻 ‘ 𝑦 ) ) )
18 17 breq2d ⊢ ( 𝑤 = ( 𝐻 ‘ 𝑦 ) → ( ( 𝐺 ‘ ( 𝐻 ‘ 𝑥 ) ) 𝑇 ( 𝐺 ‘ 𝑤 ) ↔ ( 𝐺 ‘ ( 𝐻 ‘ 𝑥 ) ) 𝑇 ( 𝐺 ‘ ( 𝐻 ‘ 𝑦 ) ) ) )
19 16 18 bibi12d ⊢ ( 𝑤 = ( 𝐻 ‘ 𝑦 ) → ( ( ( 𝐻 ‘ 𝑥 ) 𝑆 𝑤 ↔ ( 𝐺 ‘ ( 𝐻 ‘ 𝑥 ) ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) ↔ ( ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ↔ ( 𝐺 ‘ ( 𝐻 ‘ 𝑥 ) ) 𝑇 ( 𝐺 ‘ ( 𝐻 ‘ 𝑦 ) ) ) ) )
20 15 19 rspc2va ⊢ ( ( ( ( 𝐻 ‘ 𝑥 ) ∈ 𝐵 ∧ ( 𝐻 ‘ 𝑦 ) ∈ 𝐵 ) ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝑆 𝑤 ↔ ( 𝐺 ‘ 𝑧 ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) ) → ( ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ↔ ( 𝐺 ‘ ( 𝐻 ‘ 𝑥 ) ) 𝑇 ( 𝐺 ‘ ( 𝐻 ‘ 𝑦 ) ) ) )
21 8 10 11 20 syl21anc ⊢ ( ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝐺 : 𝐵 –1-1-onto→ 𝐶 ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝑆 𝑤 ↔ ( 𝐺 ‘ 𝑧 ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ↔ ( 𝐺 ‘ ( 𝐻 ‘ 𝑥 ) ) 𝑇 ( 𝐺 ‘ ( 𝐻 ‘ 𝑦 ) ) ) )
22 fvco3 ⊢ ( ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐺 ∘ 𝐻 ) ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐻 ‘ 𝑥 ) ) )
23 6 7 22 syl2anc ⊢ ( ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝐺 : 𝐵 –1-1-onto→ 𝐶 ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝑆 𝑤 ↔ ( 𝐺 ‘ 𝑧 ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝐺 ∘ 𝐻 ) ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝐻 ‘ 𝑥 ) ) )
24 fvco3 ⊢ ( ( 𝐻 : 𝐴 ⟶ 𝐵 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐺 ∘ 𝐻 ) ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐻 ‘ 𝑦 ) ) )
25 6 9 24 syl2anc ⊢ ( ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝐺 : 𝐵 –1-1-onto→ 𝐶 ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝑆 𝑤 ↔ ( 𝐺 ‘ 𝑧 ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝐺 ∘ 𝐻 ) ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝐻 ‘ 𝑦 ) ) )
26 23 25 breq12d ⊢ ( ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝐺 : 𝐵 –1-1-onto→ 𝐶 ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝑆 𝑤 ↔ ( 𝐺 ‘ 𝑧 ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( ( 𝐺 ∘ 𝐻 ) ‘ 𝑥 ) 𝑇 ( ( 𝐺 ∘ 𝐻 ) ‘ 𝑦 ) ↔ ( 𝐺 ‘ ( 𝐻 ‘ 𝑥 ) ) 𝑇 ( 𝐺 ‘ ( 𝐻 ‘ 𝑦 ) ) ) )
27 21 26 bitr4d ⊢ ( ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝐺 : 𝐵 –1-1-onto→ 𝐶 ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝑆 𝑤 ↔ ( 𝐺 ‘ 𝑧 ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ↔ ( ( 𝐺 ∘ 𝐻 ) ‘ 𝑥 ) 𝑇 ( ( 𝐺 ∘ 𝐻 ) ‘ 𝑦 ) ) )
28 27 bibi2d ⊢ ( ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝐺 : 𝐵 –1-1-onto→ 𝐶 ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝑆 𝑤 ↔ ( 𝐺 ‘ 𝑧 ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ↔ ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐺 ∘ 𝐻 ) ‘ 𝑥 ) 𝑇 ( ( 𝐺 ∘ 𝐻 ) ‘ 𝑦 ) ) ) )
29 28 2ralbidva ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝐺 : 𝐵 –1-1-onto→ 𝐶 ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝑆 𝑤 ↔ ( 𝐺 ‘ 𝑧 ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) ) ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐺 ∘ 𝐻 ) ‘ 𝑥 ) 𝑇 ( ( 𝐺 ∘ 𝐻 ) ‘ 𝑦 ) ) ) )
30 29 biimpd ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝐺 : 𝐵 –1-1-onto→ 𝐶 ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝑆 𝑤 ↔ ( 𝐺 ‘ 𝑧 ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) ) ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐺 ∘ 𝐻 ) ‘ 𝑥 ) 𝑇 ( ( 𝐺 ∘ 𝐻 ) ‘ 𝑦 ) ) ) )
31 30 impancom ⊢ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) → ( ( 𝐺 : 𝐵 –1-1-onto→ 𝐶 ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝑆 𝑤 ↔ ( 𝐺 ‘ 𝑧 ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐺 ∘ 𝐻 ) ‘ 𝑥 ) 𝑇 ( ( 𝐺 ∘ 𝐻 ) ‘ 𝑦 ) ) ) )
32 31 imp ⊢ ( ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ∧ ( 𝐺 : 𝐵 –1-1-onto→ 𝐶 ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝑆 𝑤 ↔ ( 𝐺 ‘ 𝑧 ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐺 ∘ 𝐻 ) ‘ 𝑥 ) 𝑇 ( ( 𝐺 ∘ 𝐻 ) ‘ 𝑦 ) ) )
33 4 32 jca ⊢ ( ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ∧ ( 𝐺 : 𝐵 –1-1-onto→ 𝐶 ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝑆 𝑤 ↔ ( 𝐺 ‘ 𝑧 ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) ) ) → ( ( 𝐺 ∘ 𝐻 ) : 𝐴 –1-1-onto→ 𝐶 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐺 ∘ 𝐻 ) ‘ 𝑥 ) 𝑇 ( ( 𝐺 ∘ 𝐻 ) ‘ 𝑦 ) ) ) )
34 df-isom ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) )
35 df-isom ⊢ ( 𝐺 Isom 𝑆 , 𝑇 ( 𝐵 , 𝐶 ) ↔ ( 𝐺 : 𝐵 –1-1-onto→ 𝐶 ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝑆 𝑤 ↔ ( 𝐺 ‘ 𝑧 ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) ) )
36 34 35 anbi12i ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐺 Isom 𝑆 , 𝑇 ( 𝐵 , 𝐶 ) ) ↔ ( ( 𝐻 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻 ‘ 𝑥 ) 𝑆 ( 𝐻 ‘ 𝑦 ) ) ) ∧ ( 𝐺 : 𝐵 –1-1-onto→ 𝐶 ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑤 ∈ 𝐵 ( 𝑧 𝑆 𝑤 ↔ ( 𝐺 ‘ 𝑧 ) 𝑇 ( 𝐺 ‘ 𝑤 ) ) ) ) )
37 df-isom ⊢ ( ( 𝐺 ∘ 𝐻 ) Isom 𝑅 , 𝑇 ( 𝐴 , 𝐶 ) ↔ ( ( 𝐺 ∘ 𝐻 ) : 𝐴 –1-1-onto→ 𝐶 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 𝑅 𝑦 ↔ ( ( 𝐺 ∘ 𝐻 ) ‘ 𝑥 ) 𝑇 ( ( 𝐺 ∘ 𝐻 ) ‘ 𝑦 ) ) ) )
38 33 36 37 3imtr4i ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ 𝐺 Isom 𝑆 , 𝑇 ( 𝐵 , 𝐶 ) ) → ( 𝐺 ∘ 𝐻 ) Isom 𝑅 , 𝑇 ( 𝐴 , 𝐶 ) )