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

Metamath Proof Explorer

Theorem isohom

Description: An isomorphism is a homomorphism. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypotheses isohom.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
isohom.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
isohom.i ⊢ 𝐼 = ( Iso ‘ 𝐶 )
isohom.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
isohom.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
isohom.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion isohom ( 𝜑 → ( 𝑋 𝐼 𝑌 ) ⊆ ( 𝑋 𝐻 𝑌 ) )

Proof

Step Hyp Ref Expression
1 isohom.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 isohom.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
3 isohom.i ⊢ 𝐼 = ( Iso ‘ 𝐶 )
4 isohom.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
5 isohom.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 isohom.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7 eqid ⊢ ( Inv ‘ 𝐶 ) = ( Inv ‘ 𝐶 )
8 1 7 4 5 6 3 isoval ⊢ ( 𝜑 → ( 𝑋 𝐼 𝑌 ) = dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) )
9 1 7 4 5 6 2 invss ⊢ ( 𝜑 → ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ⊆ ( ( 𝑋 𝐻 𝑌 ) × ( 𝑌 𝐻 𝑋 ) ) )
10 dmss ⊢ ( ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ⊆ ( ( 𝑋 𝐻 𝑌 ) × ( 𝑌 𝐻 𝑋 ) ) → dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ⊆ dom ( ( 𝑋 𝐻 𝑌 ) × ( 𝑌 𝐻 𝑋 ) ) )
11 9 10 syl ⊢ ( 𝜑 → dom ( 𝑋 ( Inv ‘ 𝐶 ) 𝑌 ) ⊆ dom ( ( 𝑋 𝐻 𝑌 ) × ( 𝑌 𝐻 𝑋 ) ) )
12 8 11 eqsstrd ⊢ ( 𝜑 → ( 𝑋 𝐼 𝑌 ) ⊆ dom ( ( 𝑋 𝐻 𝑌 ) × ( 𝑌 𝐻 𝑋 ) ) )
13 dmxpss ⊢ dom ( ( 𝑋 𝐻 𝑌 ) × ( 𝑌 𝐻 𝑋 ) ) ⊆ ( 𝑋 𝐻 𝑌 )
14 12 13 sstrdi ⊢ ( 𝜑 → ( 𝑋 𝐼 𝑌 ) ⊆ ( 𝑋 𝐻 𝑌 ) )