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

Metamath Proof Explorer

Theorem dihopcl

Description: Closure of an ordered pair (vector) member of a value of isomorphism H. (Contributed by NM, 26-Sep-2014)

Ref Expression
Hypotheses dihopcl.b ⊢ B = Base K
dihopcl.h ⊢ H = LHyp ⁡ K
dihopcl.t ⊢ T = LTrn ⁡ K ⁡ W
dihopcl.e ⊢ E = TEndo ⁡ K ⁡ W
dihopcl.i ⊢ I = DIsoH ⁡ K ⁡ W
dihopcl.k ⊢ φ → K ∈ HL ∧ W ∈ H
dihopcl.x ⊢ φ → X ∈ B
dihopcl.y ⊢ φ → F S ∈ I ⁡ X
Assertion dihopcl ⊢ φ → F ∈ T ∧ S ∈ E

Proof

Step Hyp Ref Expression
1 dihopcl.b ⊢ B = Base K
2 dihopcl.h ⊢ H = LHyp ⁡ K
3 dihopcl.t ⊢ T = LTrn ⁡ K ⁡ W
4 dihopcl.e ⊢ E = TEndo ⁡ K ⁡ W
5 dihopcl.i ⊢ I = DIsoH ⁡ K ⁡ W
6 dihopcl.k ⊢ φ → K ∈ HL ∧ W ∈ H
7 dihopcl.x ⊢ φ → X ∈ B
8 dihopcl.y ⊢ φ → F S ∈ I ⁡ X
9 1 2 3 4 5 6 7 dihssxp ⊢ φ → I ⁡ X ⊆ T × E
10 9 8 sseldd ⊢ φ → F S ∈ T × E
11 opelxp ⊢ F S ∈ T × E ↔ F ∈ T ∧ S ∈ E
12 10 11 sylib ⊢ φ → F ∈ T ∧ S ∈ E