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	⊢ ( 𝜑 → ( ( 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 ∧ 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐾 ) → 𝐺 = 𝐾 ) )

Metamath Proof Explorer

Theorem inveq

Proof