Metamath Proof Explorer

Theorem dibopelval3

Description: Member of the partial isomorphism B. (Contributed by NM, 3-Mar-2014)

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 dibopelval3 ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → F S ∈ I ⁡ X ↔ F ∈ T ∧ R ⁡ F ≤ ˙ X ∧ S = 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 dibopelval2 ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → F S ∈ I ⁡ X ↔ F ∈ DIsoA ⁡ K ⁡ W ⁡ X ∧ S = 0 ˙
10 1 2 3 4 5 8 diaelval ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → F ∈ DIsoA ⁡ K ⁡ W ⁡ X ↔ F ∈ T ∧ R ⁡ F ≤ ˙ X
11 10 anbi1d ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → F ∈ DIsoA ⁡ K ⁡ W ⁡ X ∧ S = 0 ˙ ↔ F ∈ T ∧ R ⁡ F ≤ ˙ X ∧ S = 0 ˙
12 9 11 bitrd ⊢ K ∈ V ∧ W ∈ H ∧ X ∈ B ∧ X ≤ ˙ W → F S ∈ I ⁡ X ↔ F ∈ T ∧ R ⁡ F ≤ ˙ X ∧ S = 0 ˙