Metamath Proof Explorer

Theorem inveq

Description: If there are two inverses of a morphism, these inverses are equal. Corollary 3.11 of Adamek p. 28. (Contributed by AV, 10-Apr-2020) (Revised by AV, 3-Jul-2022)

Ref Expression
Hypotheses inveq.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
inveq.n ⊢ 𝑁 = ( Inv ‘ 𝐶 )
inveq.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
inveq.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
inveq.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion inveq ( 𝜑 → ( ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ∧ 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐾 ) → 𝐺 = 𝐾 ) )

Proof

Step Hyp Ref Expression
1 inveq.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 inveq.n ⊢ 𝑁 = ( Inv ‘ 𝐶 )
3 inveq.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
4 inveq.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 inveq.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 eqid ⊢ ( Sect ‘ 𝐶 ) = ( Sect ‘ 𝐶 )
7 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ∧ 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐾 ) ) → 𝐶 ∈ Cat )
8 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ∧ 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐾 ) ) → 𝑌 ∈ 𝐵 )
9 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ∧ 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐾 ) ) → 𝑋 ∈ 𝐵 )
10 1 2 3 4 5 6 isinv ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ↔ ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐺 ∧ 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ) ) )
11 simpr ⊢ ( ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐺 ∧ 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ) → 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 )
12 10 11 biimtrdi ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 → 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ) )
13 12 com12 ⊢ ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 → ( 𝜑 → 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ) )
14 13 adantr ⊢ ( ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ∧ 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐾 ) → ( 𝜑 → 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ) )
15 14 impcom ⊢ ( ( 𝜑 ∧ ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ∧ 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐾 ) ) → 𝐺 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 )
16 1 2 3 4 5 6 isinv ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐾 ↔ ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐾 ∧ 𝐾 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ) ) )
17 simpl ⊢ ( ( 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐾 ∧ 𝐾 ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) 𝐹 ) → 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐾 )
18 16 17 biimtrdi ⊢ ( 𝜑 → ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐾 → 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐾 ) )
19 18 adantld ⊢ ( 𝜑 → ( ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ∧ 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐾 ) → 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐾 ) )
20 19 imp ⊢ ( ( 𝜑 ∧ ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ∧ 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐾 ) ) → 𝐹 ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) 𝐾 )
21 1 6 7 8 9 15 20 sectcan ⊢ ( ( 𝜑 ∧ ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ∧ 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐾 ) ) → 𝐺 = 𝐾 )
22 21 ex ⊢ ( 𝜑 → ( ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ∧ 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐾 ) → 𝐺 = 𝐾 ) )