Metamath Proof Explorer

Theorem dibffval

Description: The partial isomorphism B for a lattice K . (Contributed by NM, 8-Dec-2013)

Ref Expression
Hypotheses dibval.b ⊢ B = Base K
dibval.h ⊢ H = LHyp ⁡ K
Assertion dibffval ⊢ K ∈ V → DIsoB ⁡ K = w ∈ H ⟼ x ∈ dom ⁡ DIsoA ⁡ K ⁡ w ⟼ DIsoA ⁡ K ⁡ w ⁡ x × f ∈ LTrn ⁡ K ⁡ w ⟼ I ↾ B

Proof

Step Hyp Ref Expression
1 dibval.b ⊢ B = Base K
2 dibval.h ⊢ H = LHyp ⁡ K
3 elex ⊢ K ∈ V → K ∈ V
4 fveq2 ⊢ k = K → LHyp ⁡ k = LHyp ⁡ K
5 4 2 eqtr4di ⊢ k = K → LHyp ⁡ k = H
6 fveq2 ⊢ k = K → DIsoA ⁡ k = DIsoA ⁡ K
7 6 fveq1d ⊢ k = K → DIsoA ⁡ k ⁡ w = DIsoA ⁡ K ⁡ w
8 7 dmeqd ⊢ k = K → dom ⁡ DIsoA ⁡ k ⁡ w = dom ⁡ DIsoA ⁡ K ⁡ w
9 7 fveq1d ⊢ k = K → DIsoA ⁡ k ⁡ w ⁡ x = DIsoA ⁡ K ⁡ w ⁡ x
10 fveq2 ⊢ k = K → LTrn ⁡ k = LTrn ⁡ K
11 10 fveq1d ⊢ k = K → LTrn ⁡ k ⁡ w = LTrn ⁡ K ⁡ w
12 fveq2 ⊢ k = K → Base k = Base K
13 12 1 eqtr4di ⊢ k = K → Base k = B
14 13 reseq2d ⊢ k = K → I ↾ Base k = I ↾ B
15 11 14 mpteq12dv ⊢ k = K → f ∈ LTrn ⁡ k ⁡ w ⟼ I ↾ Base k = f ∈ LTrn ⁡ K ⁡ w ⟼ I ↾ B
16 15 sneqd ⊢ k = K → f ∈ LTrn ⁡ k ⁡ w ⟼ I ↾ Base k = f ∈ LTrn ⁡ K ⁡ w ⟼ I ↾ B
17 9 16 xpeq12d ⊢ k = K → DIsoA ⁡ k ⁡ w ⁡ x × f ∈ LTrn ⁡ k ⁡ w ⟼ I ↾ Base k = DIsoA ⁡ K ⁡ w ⁡ x × f ∈ LTrn ⁡ K ⁡ w ⟼ I ↾ B
18 8 17 mpteq12dv ⊢ k = K → x ∈ dom ⁡ DIsoA ⁡ k ⁡ w ⟼ DIsoA ⁡ k ⁡ w ⁡ x × f ∈ LTrn ⁡ k ⁡ w ⟼ I ↾ Base k = x ∈ dom ⁡ DIsoA ⁡ K ⁡ w ⟼ DIsoA ⁡ K ⁡ w ⁡ x × f ∈ LTrn ⁡ K ⁡ w ⟼ I ↾ B
19 5 18 mpteq12dv ⊢ k = K → w ∈ LHyp ⁡ k ⟼ x ∈ dom ⁡ DIsoA ⁡ k ⁡ w ⟼ DIsoA ⁡ k ⁡ w ⁡ x × f ∈ LTrn ⁡ k ⁡ w ⟼ I ↾ Base k = w ∈ H ⟼ x ∈ dom ⁡ DIsoA ⁡ K ⁡ w ⟼ DIsoA ⁡ K ⁡ w ⁡ x × f ∈ LTrn ⁡ K ⁡ w ⟼ I ↾ B
20 df-dib ⊢ DIsoB = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ x ∈ dom ⁡ DIsoA ⁡ k ⁡ w ⟼ DIsoA ⁡ k ⁡ w ⁡ x × f ∈ LTrn ⁡ k ⁡ w ⟼ I ↾ Base k
21 19 20 2 mptfvmpt ⊢ K ∈ V → DIsoB ⁡ K = w ∈ H ⟼ x ∈ dom ⁡ DIsoA ⁡ K ⁡ w ⟼ DIsoA ⁡ K ⁡ w ⁡ x × f ∈ LTrn ⁡ K ⁡ w ⟼ I ↾ B
22 3 21 syl ⊢ K ∈ V → DIsoB ⁡ K = w ∈ H ⟼ x ∈ dom ⁡ DIsoA ⁡ K ⁡ w ⟼ DIsoA ⁡ K ⁡ w ⁡ x × f ∈ LTrn ⁡ K ⁡ w ⟼ I ↾ B