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 | ⊢ 𝐵 = ( Base ‘ 𝐾 ) | |
dihopcl.h | ⊢ 𝐻 = ( LHyp ‘ 𝐾 ) | ||
dihopcl.t | ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) | ||
dihopcl.e | ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) | ||
dihopcl.i | ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) | ||
dihopcl.k | ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) | ||
dihopcl.x | ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) | ||
dihopcl.y | ⊢ ( 𝜑 → 〈 𝐹 , 𝑆 〉 ∈ ( 𝐼 ‘ 𝑋 ) ) | ||
Assertion | dihopcl | ⊢ ( 𝜑 → ( 𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dihopcl.b | ⊢ 𝐵 = ( Base ‘ 𝐾 ) | |
2 | dihopcl.h | ⊢ 𝐻 = ( LHyp ‘ 𝐾 ) | |
3 | dihopcl.t | ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) | |
4 | dihopcl.e | ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) | |
5 | dihopcl.i | ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) | |
6 | dihopcl.k | ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) | |
7 | dihopcl.x | ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 ) | |
8 | dihopcl.y | ⊢ ( 𝜑 → 〈 𝐹 , 𝑆 〉 ∈ ( 𝐼 ‘ 𝑋 ) ) | |
9 | 1 2 3 4 5 6 7 | dihssxp | ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑋 ) ⊆ ( 𝑇 × 𝐸 ) ) |
10 | 9 8 | sseldd | ⊢ ( 𝜑 → 〈 𝐹 , 𝑆 〉 ∈ ( 𝑇 × 𝐸 ) ) |
11 | opelxp | ⊢ ( 〈 𝐹 , 𝑆 〉 ∈ ( 𝑇 × 𝐸 ) ↔ ( 𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸 ) ) | |
12 | 10 11 | sylib | ⊢ ( 𝜑 → ( 𝐹 ∈ 𝑇 ∧ 𝑆 ∈ 𝐸 ) ) |