Step |
Hyp |
Ref |
Expression |
1 |
|
df-nmhm |
⊢ NMHom = ( 𝑠 ∈ NrmMod , 𝑡 ∈ NrmMod ↦ ( ( 𝑠 LMHom 𝑡 ) ∩ ( 𝑠 NGHom 𝑡 ) ) ) |
2 |
1
|
elmpocl |
⊢ ( 𝐹 ∈ ( 𝑆 NMHom 𝑇 ) → ( 𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ) ) |
3 |
|
oveq12 |
⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( 𝑠 LMHom 𝑡 ) = ( 𝑆 LMHom 𝑇 ) ) |
4 |
|
oveq12 |
⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( 𝑠 NGHom 𝑡 ) = ( 𝑆 NGHom 𝑇 ) ) |
5 |
3 4
|
ineq12d |
⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( ( 𝑠 LMHom 𝑡 ) ∩ ( 𝑠 NGHom 𝑡 ) ) = ( ( 𝑆 LMHom 𝑇 ) ∩ ( 𝑆 NGHom 𝑇 ) ) ) |
6 |
|
ovex |
⊢ ( 𝑆 LMHom 𝑇 ) ∈ V |
7 |
6
|
inex1 |
⊢ ( ( 𝑆 LMHom 𝑇 ) ∩ ( 𝑆 NGHom 𝑇 ) ) ∈ V |
8 |
5 1 7
|
ovmpoa |
⊢ ( ( 𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ) → ( 𝑆 NMHom 𝑇 ) = ( ( 𝑆 LMHom 𝑇 ) ∩ ( 𝑆 NGHom 𝑇 ) ) ) |
9 |
8
|
eleq2d |
⊢ ( ( 𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ) → ( 𝐹 ∈ ( 𝑆 NMHom 𝑇 ) ↔ 𝐹 ∈ ( ( 𝑆 LMHom 𝑇 ) ∩ ( 𝑆 NGHom 𝑇 ) ) ) ) |
10 |
|
elin |
⊢ ( 𝐹 ∈ ( ( 𝑆 LMHom 𝑇 ) ∩ ( 𝑆 NGHom 𝑇 ) ) ↔ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ) ) |
11 |
9 10
|
bitrdi |
⊢ ( ( 𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ) → ( 𝐹 ∈ ( 𝑆 NMHom 𝑇 ) ↔ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ) ) ) |
12 |
2 11
|
biadanii |
⊢ ( 𝐹 ∈ ( 𝑆 NMHom 𝑇 ) ↔ ( ( 𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ) ∧ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) ∧ 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ) ) ) |