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

Metamath Proof Explorer

Theorem dibval3N

Description: Value of the partial isomorphism B for a lattice K . (Contributed by NM, 24-Feb-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dibval3.b ⊢ B = Base K
dibval3.l ⊢ ≤ ˙ = ≤ K
dibval3.h ⊢ H = LHyp ⁡ K
dibval3.t ⊢ T = LTrn ⁡ K ⁡ W
dibval3.r ⊢ R = trL ⁡ K ⁡ W
dibval3.o ⊢ 0 ˙ = g ∈ T ⟼ I ↾ B
dibval3.i ⊢ I = DIsoB ⁡ K ⁡ W
Assertion dibval3N ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → I ⁡ X = f ∈ T | R ⁡ f ≤ ˙ X × 0 ˙

Proof

Step Hyp Ref Expression
1 dibval3.b ⊢ B = Base K
2 dibval3.l ⊢ ≤ ˙ = ≤ K
3 dibval3.h ⊢ H = LHyp ⁡ K
4 dibval3.t ⊢ T = LTrn ⁡ K ⁡ W
5 dibval3.r ⊢ R = trL ⁡ K ⁡ W
6 dibval3.o ⊢ 0 ˙ = g ∈ T ⟼ I ↾ B
7 dibval3.i ⊢ I = DIsoB ⁡ K ⁡ W
8 eqid ⊢ DIsoA ⁡ K ⁡ W = DIsoA ⁡ K ⁡ W
9 1 2 3 4 6 8 7 dibval2 ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → I ⁡ X = DIsoA ⁡ K ⁡ W ⁡ X × 0 ˙
10 1 2 3 4 5 8 diaval ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → DIsoA ⁡ K ⁡ W ⁡ X = f ∈ T | R ⁡ f ≤ ˙ X
11 10 xpeq1d ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → DIsoA ⁡ K ⁡ W ⁡ X × 0 ˙ = f ∈ T | R ⁡ f ≤ ˙ X × 0 ˙
12 9 11 eqtrd ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → I ⁡ X = f ∈ T | R ⁡ f ≤ ˙ X × 0 ˙