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 ⊢ B = Base K
dihf11.h ⊢ H = LHyp ⁡ K
dihf11.i ⊢ I = DIsoH ⁡ K ⁡ W
dihf11.u ⊢ U = DVecH ⁡ K ⁡ W
dihf11.s ⊢ S = LSubSp ⁡ U
Assertion dihf11 ⊢ K ∈ HL ∧ W ∈ H → I : B ⟶ 1-1 S

Proof

Step Hyp Ref Expression
1 dihf11.b ⊢ B = Base K
2 dihf11.h ⊢ H = LHyp ⁡ K
3 dihf11.i ⊢ I = DIsoH ⁡ K ⁡ W
4 dihf11.u ⊢ U = DVecH ⁡ K ⁡ W
5 dihf11.s ⊢ S = LSubSp ⁡ U
6 1 2 3 4 5 dihf11lem ⊢ K ∈ HL ∧ W ∈ H → I : B ⟶ S
7 1 2 3 dih11 ⊢ K ∈ HL ∧ W ∈ H ∧ x ∈ B ∧ y ∈ B → I ⁡ x = I ⁡ y ↔ x = y
8 7 biimpd ⊢ K ∈ HL ∧ W ∈ H ∧ x ∈ B ∧ y ∈ B → I ⁡ x = I ⁡ y → x = y
9 8 3expb ⊢ K ∈ HL ∧ W ∈ H ∧ x ∈ B ∧ y ∈ B → I ⁡ x = I ⁡ y → x = y
10 9 ralrimivva ⊢ K ∈ HL ∧ W ∈ H → ∀ x ∈ B ∀ y ∈ B I ⁡ x = I ⁡ y → x = y
11 dff13 ⊢ I : B ⟶ 1-1 S ↔ I : B ⟶ S ∧ ∀ x ∈ B ∀ y ∈ B I ⁡ x = I ⁡ y → x = y
12 6 10 11 sylanbrc ⊢ K ∈ HL ∧ W ∈ H → I : B ⟶ 1-1 S