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

Metamath Proof Explorer

Theorem diaelval

Description: Member of the partial isomorphism A for a lattice K . (Contributed by NM, 3-Dec-2013)

Ref Expression
Hypotheses diaval.b ⊢ B = Base K
diaval.l ⊢ ≤ ˙ = ≤ K
diaval.h ⊢ H = LHyp ⁡ K
diaval.t ⊢ T = LTrn ⁡ K ⁡ W
diaval.r ⊢ R = trL ⁡ K ⁡ W
diaval.i ⊢ I = DIsoA ⁡ K ⁡ W
Assertion diaelval ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → F ∈ I ⁡ X ↔ F ∈ T ∧ R ⁡ F ≤ ˙ X

Proof

Step Hyp Ref Expression
1 diaval.b ⊢ B = Base K
2 diaval.l ⊢ ≤ ˙ = ≤ K
3 diaval.h ⊢ H = LHyp ⁡ K
4 diaval.t ⊢ T = LTrn ⁡ K ⁡ W
5 diaval.r ⊢ R = trL ⁡ K ⁡ W
6 diaval.i ⊢ I = DIsoA ⁡ K ⁡ W
7 1 2 3 4 5 6 diaval ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → I ⁡ X = f ∈ T | R ⁡ f ≤ ˙ X
8 7 eleq2d ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → F ∈ I ⁡ X ↔ F ∈ f ∈ T | R ⁡ f ≤ ˙ X
9 fveq2 ⊢ f = F → R ⁡ f = R ⁡ F
10 9 breq1d ⊢ f = F → R ⁡ f ≤ ˙ X ↔ R ⁡ F ≤ ˙ X
11 10 elrab ⊢ F ∈ f ∈ T | R ⁡ f ≤ ˙ X ↔ F ∈ T ∧ R ⁡ F ≤ ˙ X
12 8 11 bitrdi ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → F ∈ I ⁡ X ↔ F ∈ T ∧ R ⁡ F ≤ ˙ X