Step |
Hyp |
Ref |
Expression |
1 |
|
df-nmhm |
|- NMHom = ( s e. NrmMod , t e. NrmMod |-> ( ( s LMHom t ) i^i ( s NGHom t ) ) ) |
2 |
1
|
elmpocl |
|- ( F e. ( S NMHom T ) -> ( S e. NrmMod /\ T e. NrmMod ) ) |
3 |
|
oveq12 |
|- ( ( s = S /\ t = T ) -> ( s LMHom t ) = ( S LMHom T ) ) |
4 |
|
oveq12 |
|- ( ( s = S /\ t = T ) -> ( s NGHom t ) = ( S NGHom T ) ) |
5 |
3 4
|
ineq12d |
|- ( ( s = S /\ t = T ) -> ( ( s LMHom t ) i^i ( s NGHom t ) ) = ( ( S LMHom T ) i^i ( S NGHom T ) ) ) |
6 |
|
ovex |
|- ( S LMHom T ) e. _V |
7 |
6
|
inex1 |
|- ( ( S LMHom T ) i^i ( S NGHom T ) ) e. _V |
8 |
5 1 7
|
ovmpoa |
|- ( ( S e. NrmMod /\ T e. NrmMod ) -> ( S NMHom T ) = ( ( S LMHom T ) i^i ( S NGHom T ) ) ) |
9 |
8
|
eleq2d |
|- ( ( S e. NrmMod /\ T e. NrmMod ) -> ( F e. ( S NMHom T ) <-> F e. ( ( S LMHom T ) i^i ( S NGHom T ) ) ) ) |
10 |
|
elin |
|- ( F e. ( ( S LMHom T ) i^i ( S NGHom T ) ) <-> ( F e. ( S LMHom T ) /\ F e. ( S NGHom T ) ) ) |
11 |
9 10
|
bitrdi |
|- ( ( S e. NrmMod /\ T e. NrmMod ) -> ( F e. ( S NMHom T ) <-> ( F e. ( S LMHom T ) /\ F e. ( S NGHom T ) ) ) ) |
12 |
2 11
|
biadanii |
|- ( F e. ( S NMHom T ) <-> ( ( S e. NrmMod /\ T e. NrmMod ) /\ ( F e. ( S LMHom T ) /\ F e. ( S NGHom T ) ) ) ) |