Metamath Proof Explorer

Theorem diaf11N

Description: The partial isomorphism A for a lattice K is a one-to-one function. Part of Lemma M of Crawley p. 120 line 27. (Contributed by NM, 4-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses dia1o.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dia1o.i ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
Assertion diaf11N ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 : dom 𝐼 –1-1-onto→ ran 𝐼 )

Proof

Step Hyp Ref Expression
1 dia1o.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dia1o.i ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
3 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
4 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
5 3 4 1 2 diafn ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 Fn { 𝑥 ∈ ( Base ‘ 𝐾 ) ∣ 𝑥 ( le ‘ 𝐾 ) 𝑊 } )
6 fnfun ⊢ ( 𝐼 Fn { 𝑥 ∈ ( Base ‘ 𝐾 ) ∣ 𝑥 ( le ‘ 𝐾 ) 𝑊 } → Fun 𝐼 )
7 funfn ⊢ ( Fun 𝐼 ↔ 𝐼 Fn dom 𝐼 )
8 6 7 sylib ⊢ ( 𝐼 Fn { 𝑥 ∈ ( Base ‘ 𝐾 ) ∣ 𝑥 ( le ‘ 𝐾 ) 𝑊 } → 𝐼 Fn dom 𝐼 )
9 5 8 syl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 Fn dom 𝐼 )
10 eqidd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ran 𝐼 = ran 𝐼 )
11 3 4 1 2 diaeldm ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑥 ∈ dom 𝐼 ↔ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) ) )
12 3 4 1 2 diaeldm ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑦 ∈ dom 𝐼 ↔ ( 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ( le ‘ 𝐾 ) 𝑊 ) ) )
13 11 12 anbi12d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( 𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼 ) ↔ ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ( le ‘ 𝐾 ) 𝑊 ) ) ) )
14 3 4 1 2 dia11N ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ( le ‘ 𝐾 ) 𝑊 ) ) → ( ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑦 ) ↔ 𝑥 = 𝑦 ) )
15 14 biimpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ( le ‘ 𝐾 ) 𝑊 ) ) → ( ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
16 15 3expib ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( ( 𝑥 ∈ ( Base ‘ 𝐾 ) ∧ 𝑥 ( le ‘ 𝐾 ) 𝑊 ) ∧ ( 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ 𝑦 ( le ‘ 𝐾 ) 𝑊 ) ) → ( ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
17 13 16 sylbid ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( 𝑥 ∈ dom 𝐼 ∧ 𝑦 ∈ dom 𝐼 ) → ( ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
18 17 ralrimivv ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∀ 𝑥 ∈ dom 𝐼 ∀ 𝑦 ∈ dom 𝐼 ( ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
19 dff1o6 ⊢ ( 𝐼 : dom 𝐼 –1-1-onto→ ran 𝐼 ↔ ( 𝐼 Fn dom 𝐼 ∧ ran 𝐼 = ran 𝐼 ∧ ∀ 𝑥 ∈ dom 𝐼 ∀ 𝑦 ∈ dom 𝐼 ( ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
20 9 10 18 19 syl3anbrc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 : dom 𝐼 –1-1-onto→ ran 𝐼 )