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

Metamath Proof Explorer

Theorem dia0eldmN

Description: The lattice zero belongs to the domain of partial isomorphism A. (Contributed by NM, 5-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses dia0eldm.z ⊢ 0 = ( 0. ‘ 𝐾 )
dia0eldm.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dia0eldm.i ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
Assertion dia0eldmN ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 0 ∈ dom 𝐼 )

Proof

Step Hyp Ref Expression
1 dia0eldm.z ⊢ 0 = ( 0. ‘ 𝐾 )
2 dia0eldm.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 dia0eldm.i ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
4 hlop ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
5 4 adantr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐾 ∈ OP )
6 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
7 6 1 op0cl ⊢ ( 𝐾 ∈ OP → 0 ∈ ( Base ‘ 𝐾 ) )
8 5 7 syl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 0 ∈ ( Base ‘ 𝐾 ) )
9 6 2 lhpbase ⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
10 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
11 6 10 1 op0le ⊢ ( ( 𝐾 ∈ OP ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → 0 ( le ‘ 𝐾 ) 𝑊 )
12 4 9 11 syl2an ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 0 ( le ‘ 𝐾 ) 𝑊 )
13 6 10 2 3 diaeldm ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 0 ∈ dom 𝐼 ↔ ( 0 ∈ ( Base ‘ 𝐾 ) ∧ 0 ( le ‘ 𝐾 ) 𝑊 ) ) )
14 8 12 13 mpbir2and ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 0 ∈ dom 𝐼 )