Metamath Proof Explorer

Theorem diafval

Description: The partial isomorphism A for a lattice K . (Contributed by NM, 15-Oct-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 diafval ⊢ K ∈ V ∧ W ∈ H → I = x ∈ y ∈ B | y ≤ ˙ W ⟼ 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 diaffval ⊢ K ∈ V → DIsoA ⁡ K = w ∈ H ⟼ x ∈ y ∈ B | y ≤ ˙ w ⟼ f ∈ LTrn ⁡ K ⁡ w | trL ⁡ K ⁡ w ⁡ f ≤ ˙ x
8 7 fveq1d ⊢ K ∈ V → DIsoA ⁡ K ⁡ W = w ∈ H ⟼ x ∈ y ∈ B | y ≤ ˙ w ⟼ f ∈ LTrn ⁡ K ⁡ w | trL ⁡ K ⁡ w ⁡ f ≤ ˙ x ⁡ W
9 6 8 eqtrid ⊢ K ∈ V → I = w ∈ H ⟼ x ∈ y ∈ B | y ≤ ˙ w ⟼ f ∈ LTrn ⁡ K ⁡ w | trL ⁡ K ⁡ w ⁡ f ≤ ˙ x ⁡ W
10 breq2 ⊢ w = W → y ≤ ˙ w ↔ y ≤ ˙ W
11 10 rabbidv ⊢ w = W → y ∈ B | y ≤ ˙ w = y ∈ B | y ≤ ˙ W
12 fveq2 ⊢ w = W → LTrn ⁡ K ⁡ w = LTrn ⁡ K ⁡ W
13 12 4 eqtr4di ⊢ w = W → LTrn ⁡ K ⁡ w = T
14 fveq2 ⊢ w = W → trL ⁡ K ⁡ w = trL ⁡ K ⁡ W
15 14 5 eqtr4di ⊢ w = W → trL ⁡ K ⁡ w = R
16 15 fveq1d ⊢ w = W → trL ⁡ K ⁡ w ⁡ f = R ⁡ f
17 16 breq1d ⊢ w = W → trL ⁡ K ⁡ w ⁡ f ≤ ˙ x ↔ R ⁡ f ≤ ˙ x
18 13 17 rabeqbidv ⊢ w = W → f ∈ LTrn ⁡ K ⁡ w | trL ⁡ K ⁡ w ⁡ f ≤ ˙ x = f ∈ T | R ⁡ f ≤ ˙ x
19 11 18 mpteq12dv ⊢ w = W → x ∈ y ∈ B | y ≤ ˙ w ⟼ f ∈ LTrn ⁡ K ⁡ w | trL ⁡ K ⁡ w ⁡ f ≤ ˙ x = x ∈ y ∈ B | y ≤ ˙ W ⟼ f ∈ T | R ⁡ f ≤ ˙ x
20 eqid ⊢ w ∈ H ⟼ x ∈ y ∈ B | y ≤ ˙ w ⟼ f ∈ LTrn ⁡ K ⁡ w | trL ⁡ K ⁡ w ⁡ f ≤ ˙ x = w ∈ H ⟼ x ∈ y ∈ B | y ≤ ˙ w ⟼ f ∈ LTrn ⁡ K ⁡ w | trL ⁡ K ⁡ w ⁡ f ≤ ˙ x
21 1 fvexi ⊢ B ∈ V
22 21 mptrabex ⊢ x ∈ y ∈ B | y ≤ ˙ W ⟼ f ∈ T | R ⁡ f ≤ ˙ x ∈ V
23 19 20 22 fvmpt ⊢ W ∈ H → w ∈ H ⟼ x ∈ y ∈ B | y ≤ ˙ w ⟼ f ∈ LTrn ⁡ K ⁡ w | trL ⁡ K ⁡ w ⁡ f ≤ ˙ x ⁡ W = x ∈ y ∈ B | y ≤ ˙ W ⟼ f ∈ T | R ⁡ f ≤ ˙ x
24 9 23 sylan9eq ⊢ K ∈ V ∧ W ∈ H → I = x ∈ y ∈ B | y ≤ ˙ W ⟼ f ∈ T | R ⁡ f ≤ ˙ x