Theorem invpropd

Description: Two structures with the same base, hom-sets and composition operation have the same inverses. (Contributed by Zhi Wang, 27-Oct-2025)

	Ref	Expression
Hypotheses	sectpropd.1	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
	sectpropd.2	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(D\right)$$
Assertion	invpropd	$$⊢\phi \to \mathrm{Inv}\left(C\right)=\mathrm{Inv}\left(D\right)$$

Proof

Step	Hyp	Ref	Expression
1		sectpropd.1	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$
2		sectpropd.2	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(D\right)$$
3	1 2	invpropdlem	$$⊢\left(\phi \wedge f\in \mathrm{Inv}\left(C\right)\right)\to f\in \mathrm{Inv}\left(D\right)$$
4	1	eqcomd	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(D\right)={\mathrm{Hom}}_{𝑓}\left(C\right)$$
5	2	eqcomd	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(D\right)={\mathrm{comp}}_{𝑓}\left(C\right)$$
6	4 5	invpropdlem	$$⊢\left(\phi \wedge f\in \mathrm{Inv}\left(D\right)\right)\to f\in \mathrm{Inv}\left(C\right)$$
7	3 6	impbida	$$⊢\phi \to \left(f\in \mathrm{Inv}\left(C\right)\leftrightarrow f\in \mathrm{Inv}\left(D\right)\right)$$
8	7	eqrdv	$$⊢\phi \to \mathrm{Inv}\left(C\right)=\mathrm{Inv}\left(D\right)$$