This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem invco

Description: The composition of two isomorphisms is an isomorphism, and the inverse is the composition of the individual inverses. Proposition 3.14(2) of Adamek p. 29. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses invfval.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
invfval.n ⊢ 𝑁 = ( Inv ‘ 𝐶 )
invfval.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
invss.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
invss.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
isoval.n ⊢ 𝐼 = ( Iso ‘ 𝐶 )
invinv.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )
invco.o ⊢ · = ( comp ‘ 𝐶 )
invco.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
invco.f ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐼 𝑍 ) )
Assertion invco ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ( 𝑋 𝑁 𝑍 ) ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 invfval.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 invfval.n ⊢ 𝑁 = ( Inv ‘ 𝐶 )
3 invfval.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
4 invss.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 invss.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 isoval.n ⊢ 𝐼 = ( Iso ‘ 𝐶 )
7 invinv.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐼 𝑌 ) )
8 invco.o ⊢ · = ( comp ‘ 𝐶 )
9 invco.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
10 invco.f ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐼 𝑍 ) )
11 eqid ⊢ ( Sect ‘ 𝐶 ) = ( Sect ‘ 𝐶 )
12 1 2 3 4 5 6 isoval ⊢ ( 𝜑 → ( 𝑋 𝐼 𝑌 ) = dom ( 𝑋 𝑁 𝑌 ) )
13 7 12 eleqtrd ⊢ ( 𝜑 → 𝐹 ∈ dom ( 𝑋 𝑁 𝑌 ) )
14 1 2 3 4 5 invfun ⊢ ( 𝜑 → Fun ( 𝑋 𝑁 𝑌 ) )
15 funfvbrb ⊢ ( Fun ( 𝑋 𝑁 𝑌 ) → ( 𝐹 ∈ dom ( 𝑋 𝑁 𝑌 ) ↔ 𝐹 ( 𝑋 𝑁 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ) )
16 14 15 syl ⊢ ( 𝜑 → ( 𝐹 ∈ dom ( 𝑋 𝑁 𝑌 ) ↔ 𝐹 ( 𝑋 𝑁 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ) )
17 13 16 mpbid ⊢ ( 𝜑 → 𝐹 ( 𝑋 𝑁 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) )
18 1 2 3 4 5 11 isinv ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑁 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ↔ ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ∧ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ) ) )
19 17 18 mpbid ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ∧ ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ) )
20 19 simpld ⊢ ( 𝜑 → 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) )
21 1 2 3 5 9 6 isoval ⊢ ( 𝜑 → ( 𝑌 𝐼 𝑍 ) = dom ( 𝑌 𝑁 𝑍 ) )
22 10 21 eleqtrd ⊢ ( 𝜑 → 𝐺 ∈ dom ( 𝑌 𝑁 𝑍 ) )
23 1 2 3 5 9 invfun ⊢ ( 𝜑 → Fun ( 𝑌 𝑁 𝑍 ) )
24 funfvbrb ⊢ ( Fun ( 𝑌 𝑁 𝑍 ) → ( 𝐺 ∈ dom ( 𝑌 𝑁 𝑍 ) ↔ 𝐺 ( 𝑌 𝑁 𝑍 ) ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) ) )
25 23 24 syl ⊢ ( 𝜑 → ( 𝐺 ∈ dom ( 𝑌 𝑁 𝑍 ) ↔ 𝐺 ( 𝑌 𝑁 𝑍 ) ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) ) )
26 22 25 mpbid ⊢ ( 𝜑 → 𝐺 ( 𝑌 𝑁 𝑍 ) ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) )
27 1 2 3 5 9 11 isinv ⊢ ( 𝜑 → ( 𝐺 ( 𝑌 𝑁 𝑍 ) ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) ↔ ( 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑍 ) ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) ∧ ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) ( 𝑍 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐺 ) ) )
28 26 27 mpbid ⊢ ( 𝜑 → ( 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑍 ) ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) ∧ ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) ( 𝑍 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐺 ) )
29 28 simpld ⊢ ( 𝜑 → 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑍 ) ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) )
30 1 8 11 3 4 5 9 20 29 sectco ⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ( 𝑋 ( Sect ‘ 𝐶 ) 𝑍 ) ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) ) )
31 28 simprd ⊢ ( 𝜑 → ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) ( 𝑍 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐺 )
32 19 simprd ⊢ ( 𝜑 → ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 )
33 1 8 11 3 9 5 4 31 32 sectco ⊢ ( 𝜑 → ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) ) ( 𝑍 ( Sect ‘ 𝐶 ) 𝑋 ) ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) )
34 1 2 3 4 9 11 isinv ⊢ ( 𝜑 → ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ( 𝑋 𝑁 𝑍 ) ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) ) ↔ ( ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ( 𝑋 ( Sect ‘ 𝐶 ) 𝑍 ) ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) ) ∧ ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) ) ( 𝑍 ( Sect ‘ 𝐶 ) 𝑋 ) ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ) ) )
35 30 33 34 mpbir2and ⊢ ( 𝜑 → ( 𝐺 ( ⟨ 𝑋 , 𝑌 ⟩ · 𝑍 ) 𝐹 ) ( 𝑋 𝑁 𝑍 ) ( ( ( 𝑋 𝑁 𝑌 ) ‘ 𝐹 ) ( ⟨ 𝑍 , 𝑌 ⟩ · 𝑋 ) ( ( 𝑌 𝑁 𝑍 ) ‘ 𝐺 ) ) )