Metamath Proof Explorer

Theorem mndtccatid

Description: Lemma for mndtccat and mndtcid . (Contributed by Zhi Wang, 22-Sep-2024)

Ref Expression
Hypotheses mndtccat.c ⊢ φ → C = MndToCat ⁡ M
mndtccat.m ⊢ φ → M ∈ Mnd
Assertion mndtccatid ⊢ φ → C ∈ Cat ∧ Id ⁡ C = y ∈ Base C ⟼ 0 M

Proof

Step Hyp Ref Expression
1 mndtccat.c ⊢ φ → C = MndToCat ⁡ M
2 mndtccat.m ⊢ φ → M ∈ Mnd
3 eqidd ⊢ φ → Base C = Base C
4 eqidd ⊢ φ → Hom ⁡ C = Hom ⁡ C
5 eqidd ⊢ φ → comp ⁡ C = comp ⁡ C
6 fvexd ⊢ φ → MndToCat ⁡ M ∈ V
7 1 6 eqeltrd ⊢ φ → C ∈ V
8 biid ⊢ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w ↔ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w
9 eqid ⊢ Base M = Base M
10 eqid ⊢ 0 M = 0 M
11 9 10 mndidcl ⊢ M ∈ Mnd → 0 M ∈ Base M
12 2 11 syl ⊢ φ → 0 M ∈ Base M
13 12 adantr ⊢ φ ∧ y ∈ Base C → 0 M ∈ Base M
14 1 adantr ⊢ φ ∧ y ∈ Base C → C = MndToCat ⁡ M
15 2 adantr ⊢ φ ∧ y ∈ Base C → M ∈ Mnd
16 eqidd ⊢ φ ∧ y ∈ Base C → Base C = Base C
17 simpr ⊢ φ ∧ y ∈ Base C → y ∈ Base C
18 eqidd ⊢ φ ∧ y ∈ Base C → Hom ⁡ C = Hom ⁡ C
19 14 15 16 17 17 18 mndtchom ⊢ φ ∧ y ∈ Base C → y Hom ⁡ C y = Base M
20 13 19 eleqtrrd ⊢ φ ∧ y ∈ Base C → 0 M ∈ y Hom ⁡ C y
21 1 adantr ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → C = MndToCat ⁡ M
22 2 adantr ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → M ∈ Mnd
23 eqidd ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → Base C = Base C
24 simpr1l ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → x ∈ Base C
25 simpr1r ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → y ∈ Base C
26 eqidd ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → comp ⁡ C = comp ⁡ C
27 21 22 23 24 25 25 26 mndtcco ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → x y comp ⁡ C y = + M
28 27 oveqd ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → 0 M x y comp ⁡ C y f = 0 M + M f
29 simpr31 ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → f ∈ x Hom ⁡ C y
30 eqidd ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → Hom ⁡ C = Hom ⁡ C
31 21 22 23 24 25 30 mndtchom ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → x Hom ⁡ C y = Base M
32 29 31 eleqtrd ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → f ∈ Base M
33 eqid ⊢ + M = + M
34 9 33 10 mndlid ⊢ M ∈ Mnd ∧ f ∈ Base M → 0 M + M f = f
35 22 32 34 syl2anc ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → 0 M + M f = f
36 28 35 eqtrd ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → 0 M x y comp ⁡ C y f = f
37 simpr2l ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → z ∈ Base C
38 21 22 23 25 25 37 26 mndtcco ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → y y comp ⁡ C z = + M
39 38 oveqd ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → g y y comp ⁡ C z 0 M = g + M 0 M
40 simpr32 ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → g ∈ y Hom ⁡ C z
41 21 22 23 25 37 30 mndtchom ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → y Hom ⁡ C z = Base M
42 40 41 eleqtrd ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → g ∈ Base M
43 9 33 10 mndrid ⊢ M ∈ Mnd ∧ g ∈ Base M → g + M 0 M = g
44 22 42 43 syl2anc ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → g + M 0 M = g
45 39 44 eqtrd ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → g y y comp ⁡ C z 0 M = g
46 9 33 mndcl ⊢ M ∈ Mnd ∧ g ∈ Base M ∧ f ∈ Base M → g + M f ∈ Base M
47 22 42 32 46 syl3anc ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → g + M f ∈ Base M
48 21 22 23 24 25 37 26 mndtcco ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → x y comp ⁡ C z = + M
49 48 oveqd ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → g x y comp ⁡ C z f = g + M f
50 21 22 23 24 37 30 mndtchom ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → x Hom ⁡ C z = Base M
51 47 49 50 3eltr4d ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → g x y comp ⁡ C z f ∈ x Hom ⁡ C z
52 simpr33 ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → k ∈ z Hom ⁡ C w
53 simpr2r ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → w ∈ Base C
54 21 22 23 37 53 30 mndtchom ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → z Hom ⁡ C w = Base M
55 52 54 eleqtrd ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → k ∈ Base M
56 9 33 mndass ⊢ M ∈ Mnd ∧ k ∈ Base M ∧ g ∈ Base M ∧ f ∈ Base M → k + M g + M f = k + M g + M f
57 22 55 42 32 56 syl13anc ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → k + M g + M f = k + M g + M f
58 21 22 23 24 25 53 26 mndtcco ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → x y comp ⁡ C w = + M
59 21 22 23 25 37 53 26 mndtcco ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → y z comp ⁡ C w = + M
60 59 oveqd ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → k y z comp ⁡ C w g = k + M g
61 eqidd ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → f = f
62 58 60 61 oveq123d ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → k y z comp ⁡ C w g x y comp ⁡ C w f = k + M g + M f
63 21 22 23 24 37 53 26 mndtcco ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → x z comp ⁡ C w = + M
64 eqidd ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → k = k
65 63 64 49 oveq123d ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → k x z comp ⁡ C w g x y comp ⁡ C z f = k + M g + M f
66 57 62 65 3eqtr4d ⊢ φ ∧ x ∈ Base C ∧ y ∈ Base C ∧ z ∈ Base C ∧ w ∈ Base C ∧ f ∈ x Hom ⁡ C y ∧ g ∈ y Hom ⁡ C z ∧ k ∈ z Hom ⁡ C w → k y z comp ⁡ C w g x y comp ⁡ C w f = k x z comp ⁡ C w g x y comp ⁡ C z f
67 3 4 5 7 8 20 36 45 51 66 iscatd2 ⊢ φ → C ∈ Cat ∧ Id ⁡ C = y ∈ Base C ⟼ 0 M