Metamath Proof Explorer

Theorem dihffval

Description: The isomorphism H for a lattice K . Definition of isomorphism map in Crawley p. 122 line 3. (Contributed by NM, 28-Jan-2014)

Ref Expression
Hypotheses dihval.b ⊢ B = Base K
dihval.l ⊢ ≤ ˙ = ≤ K
dihval.j ⊢ ∨ ˙ = join ⁡ K
dihval.m ⊢ ∧ ˙ = meet ⁡ K
dihval.a ⊢ A = Atoms ⁡ K
dihval.h ⊢ H = LHyp ⁡ K
Assertion dihffval ⊢ K ∈ V → DIsoH ⁡ K = w ∈ H ⟼ x ∈ B ⟼ if x ≤ ˙ w DIsoB ⁡ K ⁡ w ⁡ x ι u ∈ LSubSp ⁡ DVecH ⁡ K ⁡ w | ∀ q ∈ A ¬ q ≤ ˙ w ∧ q ∨ ˙ x ∧ ˙ w = x → u = DIsoC ⁡ K ⁡ w ⁡ q LSSum ⁡ DVecH ⁡ K ⁡ w DIsoB ⁡ K ⁡ w ⁡ x ∧ ˙ w

Proof

Step Hyp Ref Expression
1 dihval.b ⊢ B = Base K
2 dihval.l ⊢ ≤ ˙ = ≤ K
3 dihval.j ⊢ ∨ ˙ = join ⁡ K
4 dihval.m ⊢ ∧ ˙ = meet ⁡ K
5 dihval.a ⊢ A = Atoms ⁡ K
6 dihval.h ⊢ H = LHyp ⁡ K
7 elex ⊢ K ∈ V → K ∈ V
8 fveq2 ⊢ k = K → LHyp ⁡ k = LHyp ⁡ K
9 8 6 eqtr4di ⊢ k = K → LHyp ⁡ k = H
10 fveq2 ⊢ k = K → Base k = Base K
11 10 1 eqtr4di ⊢ k = K → Base k = B
12 fveq2 ⊢ k = K → ≤ k = ≤ K
13 12 2 eqtr4di ⊢ k = K → ≤ k = ≤ ˙
14 13 breqd ⊢ k = K → x ≤ k w ↔ x ≤ ˙ w
15 fveq2 ⊢ k = K → DIsoB ⁡ k = DIsoB ⁡ K
16 15 fveq1d ⊢ k = K → DIsoB ⁡ k ⁡ w = DIsoB ⁡ K ⁡ w
17 16 fveq1d ⊢ k = K → DIsoB ⁡ k ⁡ w ⁡ x = DIsoB ⁡ K ⁡ w ⁡ x
18 fveq2 ⊢ k = K → DVecH ⁡ k = DVecH ⁡ K
19 18 fveq1d ⊢ k = K → DVecH ⁡ k ⁡ w = DVecH ⁡ K ⁡ w
20 19 fveq2d ⊢ k = K → LSubSp ⁡ DVecH ⁡ k ⁡ w = LSubSp ⁡ DVecH ⁡ K ⁡ w
21 fveq2 ⊢ k = K → Atoms ⁡ k = Atoms ⁡ K
22 21 5 eqtr4di ⊢ k = K → Atoms ⁡ k = A
23 13 breqd ⊢ k = K → q ≤ k w ↔ q ≤ ˙ w
24 23 notbid ⊢ k = K → ¬ q ≤ k w ↔ ¬ q ≤ ˙ w
25 fveq2 ⊢ k = K → join ⁡ k = join ⁡ K
26 25 3 eqtr4di ⊢ k = K → join ⁡ k = ∨ ˙
27 eqidd ⊢ k = K → q = q
28 fveq2 ⊢ k = K → meet ⁡ k = meet ⁡ K
29 28 4 eqtr4di ⊢ k = K → meet ⁡ k = ∧ ˙
30 29 oveqd ⊢ k = K → x meet ⁡ k w = x ∧ ˙ w
31 26 27 30 oveq123d ⊢ k = K → q join ⁡ k x meet ⁡ k w = q ∨ ˙ x ∧ ˙ w
32 31 eqeq1d ⊢ k = K → q join ⁡ k x meet ⁡ k w = x ↔ q ∨ ˙ x ∧ ˙ w = x
33 24 32 anbi12d ⊢ k = K → ¬ q ≤ k w ∧ q join ⁡ k x meet ⁡ k w = x ↔ ¬ q ≤ ˙ w ∧ q ∨ ˙ x ∧ ˙ w = x
34 19 fveq2d ⊢ k = K → LSSum ⁡ DVecH ⁡ k ⁡ w = LSSum ⁡ DVecH ⁡ K ⁡ w
35 fveq2 ⊢ k = K → DIsoC ⁡ k = DIsoC ⁡ K
36 35 fveq1d ⊢ k = K → DIsoC ⁡ k ⁡ w = DIsoC ⁡ K ⁡ w
37 36 fveq1d ⊢ k = K → DIsoC ⁡ k ⁡ w ⁡ q = DIsoC ⁡ K ⁡ w ⁡ q
38 16 30 fveq12d ⊢ k = K → DIsoB ⁡ k ⁡ w ⁡ x meet ⁡ k w = DIsoB ⁡ K ⁡ w ⁡ x ∧ ˙ w
39 34 37 38 oveq123d ⊢ k = K → DIsoC ⁡ k ⁡ w ⁡ q LSSum ⁡ DVecH ⁡ k ⁡ w DIsoB ⁡ k ⁡ w ⁡ x meet ⁡ k w = DIsoC ⁡ K ⁡ w ⁡ q LSSum ⁡ DVecH ⁡ K ⁡ w DIsoB ⁡ K ⁡ w ⁡ x ∧ ˙ w
40 39 eqeq2d ⊢ k = K → u = DIsoC ⁡ k ⁡ w ⁡ q LSSum ⁡ DVecH ⁡ k ⁡ w DIsoB ⁡ k ⁡ w ⁡ x meet ⁡ k w ↔ u = DIsoC ⁡ K ⁡ w ⁡ q LSSum ⁡ DVecH ⁡ K ⁡ w DIsoB ⁡ K ⁡ w ⁡ x ∧ ˙ w
41 33 40 imbi12d ⊢ k = K → ¬ q ≤ k w ∧ q join ⁡ k x meet ⁡ k w = x → u = DIsoC ⁡ k ⁡ w ⁡ q LSSum ⁡ DVecH ⁡ k ⁡ w DIsoB ⁡ k ⁡ w ⁡ x meet ⁡ k w ↔ ¬ q ≤ ˙ w ∧ q ∨ ˙ x ∧ ˙ w = x → u = DIsoC ⁡ K ⁡ w ⁡ q LSSum ⁡ DVecH ⁡ K ⁡ w DIsoB ⁡ K ⁡ w ⁡ x ∧ ˙ w
42 22 41 raleqbidv ⊢ k = K → ∀ q ∈ Atoms ⁡ k ¬ q ≤ k w ∧ q join ⁡ k x meet ⁡ k w = x → u = DIsoC ⁡ k ⁡ w ⁡ q LSSum ⁡ DVecH ⁡ k ⁡ w DIsoB ⁡ k ⁡ w ⁡ x meet ⁡ k w ↔ ∀ q ∈ A ¬ q ≤ ˙ w ∧ q ∨ ˙ x ∧ ˙ w = x → u = DIsoC ⁡ K ⁡ w ⁡ q LSSum ⁡ DVecH ⁡ K ⁡ w DIsoB ⁡ K ⁡ w ⁡ x ∧ ˙ w
43 20 42 riotaeqbidv ⊢ k = K → ι u ∈ LSubSp ⁡ DVecH ⁡ k ⁡ w | ∀ q ∈ Atoms ⁡ k ¬ q ≤ k w ∧ q join ⁡ k x meet ⁡ k w = x → u = DIsoC ⁡ k ⁡ w ⁡ q LSSum ⁡ DVecH ⁡ k ⁡ w DIsoB ⁡ k ⁡ w ⁡ x meet ⁡ k w = ι u ∈ LSubSp ⁡ DVecH ⁡ K ⁡ w | ∀ q ∈ A ¬ q ≤ ˙ w ∧ q ∨ ˙ x ∧ ˙ w = x → u = DIsoC ⁡ K ⁡ w ⁡ q LSSum ⁡ DVecH ⁡ K ⁡ w DIsoB ⁡ K ⁡ w ⁡ x ∧ ˙ w
44 14 17 43 ifbieq12d ⊢ k = K → if x ≤ k w DIsoB ⁡ k ⁡ w ⁡ x ι u ∈ LSubSp ⁡ DVecH ⁡ k ⁡ w | ∀ q ∈ Atoms ⁡ k ¬ q ≤ k w ∧ q join ⁡ k x meet ⁡ k w = x → u = DIsoC ⁡ k ⁡ w ⁡ q LSSum ⁡ DVecH ⁡ k ⁡ w DIsoB ⁡ k ⁡ w ⁡ x meet ⁡ k w = if x ≤ ˙ w DIsoB ⁡ K ⁡ w ⁡ x ι u ∈ LSubSp ⁡ DVecH ⁡ K ⁡ w | ∀ q ∈ A ¬ q ≤ ˙ w ∧ q ∨ ˙ x ∧ ˙ w = x → u = DIsoC ⁡ K ⁡ w ⁡ q LSSum ⁡ DVecH ⁡ K ⁡ w DIsoB ⁡ K ⁡ w ⁡ x ∧ ˙ w
45 11 44 mpteq12dv ⊢ k = K → x ∈ Base k ⟼ if x ≤ k w DIsoB ⁡ k ⁡ w ⁡ x ι u ∈ LSubSp ⁡ DVecH ⁡ k ⁡ w | ∀ q ∈ Atoms ⁡ k ¬ q ≤ k w ∧ q join ⁡ k x meet ⁡ k w = x → u = DIsoC ⁡ k ⁡ w ⁡ q LSSum ⁡ DVecH ⁡ k ⁡ w DIsoB ⁡ k ⁡ w ⁡ x meet ⁡ k w = x ∈ B ⟼ if x ≤ ˙ w DIsoB ⁡ K ⁡ w ⁡ x ι u ∈ LSubSp ⁡ DVecH ⁡ K ⁡ w | ∀ q ∈ A ¬ q ≤ ˙ w ∧ q ∨ ˙ x ∧ ˙ w = x → u = DIsoC ⁡ K ⁡ w ⁡ q LSSum ⁡ DVecH ⁡ K ⁡ w DIsoB ⁡ K ⁡ w ⁡ x ∧ ˙ w
46 9 45 mpteq12dv ⊢ k = K → w ∈ LHyp ⁡ k ⟼ x ∈ Base k ⟼ if x ≤ k w DIsoB ⁡ k ⁡ w ⁡ x ι u ∈ LSubSp ⁡ DVecH ⁡ k ⁡ w | ∀ q ∈ Atoms ⁡ k ¬ q ≤ k w ∧ q join ⁡ k x meet ⁡ k w = x → u = DIsoC ⁡ k ⁡ w ⁡ q LSSum ⁡ DVecH ⁡ k ⁡ w DIsoB ⁡ k ⁡ w ⁡ x meet ⁡ k w = w ∈ H ⟼ x ∈ B ⟼ if x ≤ ˙ w DIsoB ⁡ K ⁡ w ⁡ x ι u ∈ LSubSp ⁡ DVecH ⁡ K ⁡ w | ∀ q ∈ A ¬ q ≤ ˙ w ∧ q ∨ ˙ x ∧ ˙ w = x → u = DIsoC ⁡ K ⁡ w ⁡ q LSSum ⁡ DVecH ⁡ K ⁡ w DIsoB ⁡ K ⁡ w ⁡ x ∧ ˙ w
47 df-dih ⊢ DIsoH = k ∈ V ⟼ w ∈ LHyp ⁡ k ⟼ x ∈ Base k ⟼ if x ≤ k w DIsoB ⁡ k ⁡ w ⁡ x ι u ∈ LSubSp ⁡ DVecH ⁡ k ⁡ w | ∀ q ∈ Atoms ⁡ k ¬ q ≤ k w ∧ q join ⁡ k x meet ⁡ k w = x → u = DIsoC ⁡ k ⁡ w ⁡ q LSSum ⁡ DVecH ⁡ k ⁡ w DIsoB ⁡ k ⁡ w ⁡ x meet ⁡ k w
48 46 47 6 mptfvmpt ⊢ K ∈ V → DIsoH ⁡ K = w ∈ H ⟼ x ∈ B ⟼ if x ≤ ˙ w DIsoB ⁡ K ⁡ w ⁡ x ι u ∈ LSubSp ⁡ DVecH ⁡ K ⁡ w | ∀ q ∈ A ¬ q ≤ ˙ w ∧ q ∨ ˙ x ∧ ˙ w = x → u = DIsoC ⁡ K ⁡ w ⁡ q LSSum ⁡ DVecH ⁡ K ⁡ w DIsoB ⁡ K ⁡ w ⁡ x ∧ ˙ w
49 7 48 syl ⊢ K ∈ V → DIsoH ⁡ K = w ∈ H ⟼ x ∈ B ⟼ if x ≤ ˙ w DIsoB ⁡ K ⁡ w ⁡ x ι u ∈ LSubSp ⁡ DVecH ⁡ K ⁡ w | ∀ q ∈ A ¬ q ≤ ˙ w ∧ q ∨ ˙ x ∧ ˙ w = x → u = DIsoC ⁡ K ⁡ w ⁡ q LSSum ⁡ DVecH ⁡ K ⁡ w DIsoB ⁡ K ⁡ w ⁡ x ∧ ˙ w