Metamath Proof Explorer

Theorem dialss

Description: The value of partial isomorphism A is a subspace of partial vector space A. Part of Lemma M of Crawley p. 120 line 26. (Contributed by NM, 17-Jan-2014) (Revised by Mario Carneiro, 23-Jun-2014)

Ref Expression
Hypotheses dialss.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dialss.l ⊢ ≤ = ( le ‘ 𝐾 )
dialss.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dialss.u ⊢ 𝑈 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
dialss.i ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
dialss.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
Assertion dialss ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 dialss.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dialss.l ⊢ ≤ = ( le ‘ 𝐾 )
3 dialss.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4 dialss.u ⊢ 𝑈 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
5 dialss.i ⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
6 dialss.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
7 eqidd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 ) )
8 eqid ⊢ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
9 eqid ⊢ ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
10 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑈 ) ) = ( Base ‘ ( Scalar ‘ 𝑈 ) )
11 3 8 4 9 10 dvabase ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ ( Scalar ‘ 𝑈 ) ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
12 11 eqcomd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( Base ‘ ( Scalar ‘ 𝑈 ) ) )
13 12 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( Base ‘ ( Scalar ‘ 𝑈 ) ) )
14 eqid ⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
15 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
16 3 14 4 15 dvavbase ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ 𝑈 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
17 16 eqcomd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( Base ‘ 𝑈 ) )
18 17 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( Base ‘ 𝑈 ) )
19 eqidd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 ) )
20 eqidd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( ·𝑠 ‘ 𝑈 ) = ( ·𝑠 ‘ 𝑈 ) )
21 6 a1i ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → 𝑆 = ( LSubSp ‘ 𝑈 ) )
22 1 2 3 14 5 diass ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑋 ) ⊆ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
23 1 2 3 5 dian0 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑋 ) ≠ ∅ )
24 simpll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
25 simpr1 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
26 simplr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) )
27 simpr2 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) )
28 1 2 3 14 5 diael ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ) → 𝑎 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
29 24 26 27 28 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → 𝑎 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
30 eqid ⊢ ( ·𝑠 ‘ 𝑈 ) = ( ·𝑠 ‘ 𝑈 )
31 3 14 8 4 30 dvavsca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑈 ) 𝑎 ) = ( 𝑥 ‘ 𝑎 ) )
32 24 25 29 31 syl12anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( 𝑥 ( ·𝑠 ‘ 𝑈 ) 𝑎 ) = ( 𝑥 ‘ 𝑎 ) )
33 32 oveq1d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑈 ) 𝑎 ) ( +g ‘ 𝑈 ) 𝑏 ) = ( ( 𝑥 ‘ 𝑎 ) ( +g ‘ 𝑈 ) 𝑏 ) )
34 3 14 8 tendocl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑥 ‘ 𝑎 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
35 24 25 29 34 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( 𝑥 ‘ 𝑎 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
36 simpr3 ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) )
37 1 2 3 14 5 diael ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) → 𝑏 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
38 24 26 36 37 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → 𝑏 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
39 eqid ⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
40 3 14 4 39 dvavadd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑥 ‘ 𝑎 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑏 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( ( 𝑥 ‘ 𝑎 ) ( +g ‘ 𝑈 ) 𝑏 ) = ( ( 𝑥 ‘ 𝑎 ) ∘ 𝑏 ) )
41 24 35 38 40 syl12anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( 𝑥 ‘ 𝑎 ) ( +g ‘ 𝑈 ) 𝑏 ) = ( ( 𝑥 ‘ 𝑎 ) ∘ 𝑏 ) )
42 33 41 eqtrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑈 ) 𝑎 ) ( +g ‘ 𝑈 ) 𝑏 ) = ( ( 𝑥 ‘ 𝑎 ) ∘ 𝑏 ) )
43 3 14 ltrnco ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑥 ‘ 𝑎 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑏 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( 𝑥 ‘ 𝑎 ) ∘ 𝑏 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
44 24 35 38 43 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( 𝑥 ‘ 𝑎 ) ∘ 𝑏 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) )
45 hllat ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
46 45 ad3antrrr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → 𝐾 ∈ Lat )
47 eqid ⊢ ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
48 1 3 14 47 trlcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑥 ‘ 𝑎 ) ∘ 𝑏 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( 𝑥 ‘ 𝑎 ) ∘ 𝑏 ) ) ∈ 𝐵 )
49 24 44 48 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( 𝑥 ‘ 𝑎 ) ∘ 𝑏 ) ) ∈ 𝐵 )
50 1 3 14 47 trlcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑥 ‘ 𝑎 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ‘ 𝑎 ) ) ∈ 𝐵 )
51 24 35 50 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ‘ 𝑎 ) ) ∈ 𝐵 )
52 1 3 14 47 trlcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑏 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑏 ) ∈ 𝐵 )
53 24 38 52 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑏 ) ∈ 𝐵 )
54 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
55 1 54 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ‘ 𝑎 ) ) ∈ 𝐵 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑏 ) ∈ 𝐵 ) → ( ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ‘ 𝑎 ) ) ( join ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑏 ) ) ∈ 𝐵 )
56 46 51 53 55 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ‘ 𝑎 ) ) ( join ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑏 ) ) ∈ 𝐵 )
57 simplrl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → 𝑋 ∈ 𝐵 )
58 2 54 3 14 47 trlco ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑥 ‘ 𝑎 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑏 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( 𝑥 ‘ 𝑎 ) ∘ 𝑏 ) ) ≤ ( ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ‘ 𝑎 ) ) ( join ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑏 ) ) )
59 24 35 38 58 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( 𝑥 ‘ 𝑎 ) ∘ 𝑏 ) ) ≤ ( ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ‘ 𝑎 ) ) ( join ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑏 ) ) )
60 1 3 14 47 trlcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑎 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑎 ) ∈ 𝐵 )
61 24 29 60 syl2anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑎 ) ∈ 𝐵 )
62 2 3 14 47 8 tendotp ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ‘ 𝑎 ) ) ≤ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑎 ) )
63 24 25 29 62 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ‘ 𝑎 ) ) ≤ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑎 ) )
64 1 2 3 14 47 5 diatrl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑎 ) ≤ 𝑋 )
65 24 26 27 64 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑎 ) ≤ 𝑋 )
66 1 2 46 51 61 57 63 65 lattrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ‘ 𝑎 ) ) ≤ 𝑋 )
67 1 2 3 14 47 5 diatrl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑏 ) ≤ 𝑋 )
68 24 26 36 67 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑏 ) ≤ 𝑋 )
69 1 2 54 latjle12 ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ‘ 𝑎 ) ) ∈ 𝐵 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑏 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ) → ( ( ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ‘ 𝑎 ) ) ≤ 𝑋 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑏 ) ≤ 𝑋 ) ↔ ( ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ‘ 𝑎 ) ) ( join ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑏 ) ) ≤ 𝑋 ) )
70 46 51 53 57 69 syl13anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ‘ 𝑎 ) ) ≤ 𝑋 ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑏 ) ≤ 𝑋 ) ↔ ( ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ‘ 𝑎 ) ) ( join ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑏 ) ) ≤ 𝑋 ) )
71 66 68 70 mpbi2and ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ‘ 𝑎 ) ) ( join ‘ 𝐾 ) ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑏 ) ) ≤ 𝑋 )
72 1 2 46 49 56 57 59 71 lattrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( 𝑥 ‘ 𝑎 ) ∘ 𝑏 ) ) ≤ 𝑋 )
73 1 2 3 14 47 5 diaelval ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( ( ( 𝑥 ‘ 𝑎 ) ∘ 𝑏 ) ∈ ( 𝐼 ‘ 𝑋 ) ↔ ( ( ( 𝑥 ‘ 𝑎 ) ∘ 𝑏 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( 𝑥 ‘ 𝑎 ) ∘ 𝑏 ) ) ≤ 𝑋 ) ) )
74 73 adantr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( ( 𝑥 ‘ 𝑎 ) ∘ 𝑏 ) ∈ ( 𝐼 ‘ 𝑋 ) ↔ ( ( ( 𝑥 ‘ 𝑎 ) ∘ 𝑏 ) ∈ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( ( ( trL ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( 𝑥 ‘ 𝑎 ) ∘ 𝑏 ) ) ≤ 𝑋 ) ) )
75 44 72 74 mpbir2and ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( 𝑥 ‘ 𝑎 ) ∘ 𝑏 ) ∈ ( 𝐼 ‘ 𝑋 ) )
76 42 75 eqeltrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) ∧ ( 𝑥 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝑎 ∈ ( 𝐼 ‘ 𝑋 ) ∧ 𝑏 ∈ ( 𝐼 ‘ 𝑋 ) ) ) → ( ( 𝑥 ( ·𝑠 ‘ 𝑈 ) 𝑎 ) ( +g ‘ 𝑈 ) 𝑏 ) ∈ ( 𝐼 ‘ 𝑋 ) )
77 7 13 18 19 20 21 22 23 76 islssd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝑆 )