Step |
Hyp |
Ref |
Expression |
1 |
|
isrim0 |
⊢ ( 𝐹 ∈ ( 𝑆 RingIso 𝑇 ) ↔ ( 𝐹 ∈ ( 𝑆 RingHom 𝑇 ) ∧ ◡ 𝐹 ∈ ( 𝑇 RingHom 𝑆 ) ) ) |
2 |
|
isrim0 |
⊢ ( 𝐺 ∈ ( 𝑅 RingIso 𝑆 ) ↔ ( 𝐺 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ◡ 𝐺 ∈ ( 𝑆 RingHom 𝑅 ) ) ) |
3 |
|
rhmco |
⊢ ( ( 𝐹 ∈ ( 𝑆 RingHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑅 RingHom 𝑆 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑅 RingHom 𝑇 ) ) |
4 |
|
cnvco |
⊢ ◡ ( 𝐹 ∘ 𝐺 ) = ( ◡ 𝐺 ∘ ◡ 𝐹 ) |
5 |
|
rhmco |
⊢ ( ( ◡ 𝐺 ∈ ( 𝑆 RingHom 𝑅 ) ∧ ◡ 𝐹 ∈ ( 𝑇 RingHom 𝑆 ) ) → ( ◡ 𝐺 ∘ ◡ 𝐹 ) ∈ ( 𝑇 RingHom 𝑅 ) ) |
6 |
5
|
ancoms |
⊢ ( ( ◡ 𝐹 ∈ ( 𝑇 RingHom 𝑆 ) ∧ ◡ 𝐺 ∈ ( 𝑆 RingHom 𝑅 ) ) → ( ◡ 𝐺 ∘ ◡ 𝐹 ) ∈ ( 𝑇 RingHom 𝑅 ) ) |
7 |
4 6
|
eqeltrid |
⊢ ( ( ◡ 𝐹 ∈ ( 𝑇 RingHom 𝑆 ) ∧ ◡ 𝐺 ∈ ( 𝑆 RingHom 𝑅 ) ) → ◡ ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑇 RingHom 𝑅 ) ) |
8 |
3 7
|
anim12i |
⊢ ( ( ( 𝐹 ∈ ( 𝑆 RingHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑅 RingHom 𝑆 ) ) ∧ ( ◡ 𝐹 ∈ ( 𝑇 RingHom 𝑆 ) ∧ ◡ 𝐺 ∈ ( 𝑆 RingHom 𝑅 ) ) ) → ( ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑅 RingHom 𝑇 ) ∧ ◡ ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑇 RingHom 𝑅 ) ) ) |
9 |
8
|
an4s |
⊢ ( ( ( 𝐹 ∈ ( 𝑆 RingHom 𝑇 ) ∧ ◡ 𝐹 ∈ ( 𝑇 RingHom 𝑆 ) ) ∧ ( 𝐺 ∈ ( 𝑅 RingHom 𝑆 ) ∧ ◡ 𝐺 ∈ ( 𝑆 RingHom 𝑅 ) ) ) → ( ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑅 RingHom 𝑇 ) ∧ ◡ ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑇 RingHom 𝑅 ) ) ) |
10 |
1 2 9
|
syl2anb |
⊢ ( ( 𝐹 ∈ ( 𝑆 RingIso 𝑇 ) ∧ 𝐺 ∈ ( 𝑅 RingIso 𝑆 ) ) → ( ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑅 RingHom 𝑇 ) ∧ ◡ ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑇 RingHom 𝑅 ) ) ) |
11 |
|
isrim0 |
⊢ ( ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑅 RingIso 𝑇 ) ↔ ( ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑅 RingHom 𝑇 ) ∧ ◡ ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑇 RingHom 𝑅 ) ) ) |
12 |
10 11
|
sylibr |
⊢ ( ( 𝐹 ∈ ( 𝑆 RingIso 𝑇 ) ∧ 𝐺 ∈ ( 𝑅 RingIso 𝑆 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ( 𝑅 RingIso 𝑇 ) ) |