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

Metamath Proof Explorer

Theorem zeroopropd

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

Ref Expression
Hypotheses initopropd.1 
|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
initopropd.2 
|- ( ph -> ( comf ` C ) = ( comf ` D ) )
Assertion zeroopropd 
|- ( ph -> ( ZeroO ` C ) = ( ZeroO ` D ) )

Proof

Step Hyp Ref Expression
1 initopropd.1 
 |-  ( ph -> ( Homf ` C ) = ( Homf ` D ) )
2 initopropd.2 
 |-  ( ph -> ( comf ` C ) = ( comf ` D ) )
3 1 adantr 
 |-  ( ( ph /\ -. C e. _V ) -> ( Homf ` C ) = ( Homf ` D ) )
4 2 adantr 
 |-  ( ( ph /\ -. C e. _V ) -> ( comf ` C ) = ( comf ` D ) )
5 simpr 
 |-  ( ( ph /\ -. C e. _V ) -> -. C e. _V )
6 3 4 5 zeroopropdlem 
 |-  ( ( ph /\ -. C e. _V ) -> ( ZeroO ` C ) = ( ZeroO ` D ) )
7 1 adantr 
 |-  ( ( ph /\ -. D e. _V ) -> ( Homf ` C ) = ( Homf ` D ) )
8 7 eqcomd 
 |-  ( ( ph /\ -. D e. _V ) -> ( Homf ` D ) = ( Homf ` C ) )
9 2 adantr 
 |-  ( ( ph /\ -. D e. _V ) -> ( comf ` C ) = ( comf ` D ) )
10 9 eqcomd 
 |-  ( ( ph /\ -. D e. _V ) -> ( comf ` D ) = ( comf ` C ) )
11 simpr 
 |-  ( ( ph /\ -. D e. _V ) -> -. D e. _V )
12 8 10 11 zeroopropdlem 
 |-  ( ( ph /\ -. D e. _V ) -> ( ZeroO ` D ) = ( ZeroO ` C ) )
13 12 eqcomd 
 |-  ( ( ph /\ -. D e. _V ) -> ( ZeroO ` C ) = ( ZeroO ` D ) )
14 1 ad2antrr 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> ( Homf ` C ) = ( Homf ` D ) )
15 2 ad2antrr 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> ( comf ` C ) = ( comf ` D ) )
16 14 15 initopropd 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> ( InitO ` C ) = ( InitO ` D ) )
17 14 15 termopropd 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> ( TermO ` C ) = ( TermO ` D ) )
18 16 17 ineq12d 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> ( ( InitO ` C ) i^i ( TermO ` C ) ) = ( ( InitO ` D ) i^i ( TermO ` D ) ) )
19 simpr 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> C e. Cat )
20 eqid 
 |-  ( Base ` C ) = ( Base ` C )
21 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
22 19 20 21 zerooval 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> ( ZeroO ` C ) = ( ( InitO ` C ) i^i ( TermO ` C ) ) )
23 1 adantr 
 |-  ( ( ph /\ ( C e. _V /\ D e. _V ) ) -> ( Homf ` C ) = ( Homf ` D ) )
24 2 adantr 
 |-  ( ( ph /\ ( C e. _V /\ D e. _V ) ) -> ( comf ` C ) = ( comf ` D ) )
25 simprl 
 |-  ( ( ph /\ ( C e. _V /\ D e. _V ) ) -> C e. _V )
26 simprr 
 |-  ( ( ph /\ ( C e. _V /\ D e. _V ) ) -> D e. _V )
27 23 24 25 26 catpropd 
 |-  ( ( ph /\ ( C e. _V /\ D e. _V ) ) -> ( C e. Cat <-> D e. Cat ) )
28 27 biimpa 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> D e. Cat )
29 eqid 
 |-  ( Base ` D ) = ( Base ` D )
30 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
31 28 29 30 zerooval 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> ( ZeroO ` D ) = ( ( InitO ` D ) i^i ( TermO ` D ) ) )
32 18 22 31 3eqtr4d 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) -> ( ZeroO ` C ) = ( ZeroO ` D ) )
33 27 pm5.32i 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ C e. Cat ) <-> ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ D e. Cat ) )
34 33 32 sylbir 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ D e. Cat ) -> ( ZeroO ` C ) = ( ZeroO ` D ) )
35 zeroofn 
 |-  ZeroO Fn Cat
36 35 fndmi 
 |-  dom ZeroO = Cat
37 36 eleq2i 
 |-  ( C e. dom ZeroO <-> C e. Cat )
38 ndmfv 
 |-  ( -. C e. dom ZeroO -> ( ZeroO ` C ) = (/) )
39 37 38 sylnbir 
 |-  ( -. C e. Cat -> ( ZeroO ` C ) = (/) )
40 39 ad2antrl 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ ( -. C e. Cat /\ -. D e. Cat ) ) -> ( ZeroO ` C ) = (/) )
41 36 eleq2i 
 |-  ( D e. dom ZeroO <-> D e. Cat )
42 ndmfv 
 |-  ( -. D e. dom ZeroO -> ( ZeroO ` D ) = (/) )
43 41 42 sylnbir 
 |-  ( -. D e. Cat -> ( ZeroO ` D ) = (/) )
44 43 ad2antll 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ ( -. C e. Cat /\ -. D e. Cat ) ) -> ( ZeroO ` D ) = (/) )
45 40 44 eqtr4d 
 |-  ( ( ( ph /\ ( C e. _V /\ D e. _V ) ) /\ ( -. C e. Cat /\ -. D e. Cat ) ) -> ( ZeroO ` C ) = ( ZeroO ` D ) )
46 32 34 45 pm2.61ddan 
 |-  ( ( ph /\ ( C e. _V /\ D e. _V ) ) -> ( ZeroO ` C ) = ( ZeroO ` D ) )
47 6 13 46 pm2.61dda 
 |-  ( ph -> ( ZeroO ` C ) = ( ZeroO ` D ) )