Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Structures
ismhmd
Next ⟩
ablcmnd
Metamath Proof Explorer
Ascii
Unicode
Theorem
ismhmd
Description:
Deduction version of
ismhm
.
(Contributed by
SN
, 27-Jul-2024)
Ref
Expression
Hypotheses
ismhmd.b
⊢
B
=
Base
S
ismhmd.c
⊢
C
=
Base
T
ismhmd.p
⊢
+
˙
=
+
S
ismhmd.q
⊢
⨣
˙
=
+
T
ismhmd.0
⊢
0
˙
=
0
S
ismhmd.z
⊢
Z
=
0
T
ismhmd.s
⊢
φ
→
S
∈
Mnd
ismhmd.t
⊢
φ
→
T
∈
Mnd
ismhmd.f
⊢
φ
→
F
:
B
⟶
C
ismhmd.a
⊢
φ
∧
x
∈
B
∧
y
∈
B
→
F
⁡
x
+
˙
y
=
F
⁡
x
⨣
˙
F
⁡
y
ismhmd.h
⊢
φ
→
F
⁡
0
˙
=
Z
Assertion
ismhmd
⊢
φ
→
F
∈
S
MndHom
T
Proof
Step
Hyp
Ref
Expression
1
ismhmd.b
⊢
B
=
Base
S
2
ismhmd.c
⊢
C
=
Base
T
3
ismhmd.p
⊢
+
˙
=
+
S
4
ismhmd.q
⊢
⨣
˙
=
+
T
5
ismhmd.0
⊢
0
˙
=
0
S
6
ismhmd.z
⊢
Z
=
0
T
7
ismhmd.s
⊢
φ
→
S
∈
Mnd
8
ismhmd.t
⊢
φ
→
T
∈
Mnd
9
ismhmd.f
⊢
φ
→
F
:
B
⟶
C
10
ismhmd.a
⊢
φ
∧
x
∈
B
∧
y
∈
B
→
F
⁡
x
+
˙
y
=
F
⁡
x
⨣
˙
F
⁡
y
11
ismhmd.h
⊢
φ
→
F
⁡
0
˙
=
Z
12
10
ralrimivva
⊢
φ
→
∀
x
∈
B
∀
y
∈
B
F
⁡
x
+
˙
y
=
F
⁡
x
⨣
˙
F
⁡
y
13
9
12
11
3jca
⊢
φ
→
F
:
B
⟶
C
∧
∀
x
∈
B
∀
y
∈
B
F
⁡
x
+
˙
y
=
F
⁡
x
⨣
˙
F
⁡
y
∧
F
⁡
0
˙
=
Z
14
1
2
3
4
5
6
ismhm
⊢
F
∈
S
MndHom
T
↔
S
∈
Mnd
∧
T
∈
Mnd
∧
F
:
B
⟶
C
∧
∀
x
∈
B
∀
y
∈
B
F
⁡
x
+
˙
y
=
F
⁡
x
⨣
˙
F
⁡
y
∧
F
⁡
0
˙
=
Z
15
7
8
13
14
syl21anbrc
⊢
φ
→
F
∈
S
MndHom
T