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

Metamath Proof Explorer

Theorem dihf11

Description: The isomorphism H for a lattice K is a one-to-one function. Part of proof after Lemma N of Crawley p. 122 line 6. (Contributed by NM, 7-Mar-2014)

Ref Expression
Hypotheses dihf11.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dihf11.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihf11.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dihf11.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dihf11.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
Assertion dihf11 ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 : 𝐵 –1-1→ 𝑆 )

Proof

Step Hyp Ref Expression
1 dihf11.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dihf11.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 dihf11.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
4 dihf11.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 dihf11.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
6 1 2 3 4 5 dihf11lem ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 : 𝐵 ⟶ 𝑆 )
7 1 2 3 dih11 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑦 ) ↔ 𝑥 = 𝑦 ) )
8 7 biimpd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
9 8 3expb ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
10 9 ralrimivva ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
11 dff13 ⊢ ( 𝐼 : 𝐵 –1-1→ 𝑆 ↔ ( 𝐼 : 𝐵 ⟶ 𝑆 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝐼 ‘ 𝑥 ) = ( 𝐼 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
12 6 10 11 sylanbrc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 : 𝐵 –1-1→ 𝑆 )