Theorem dialss 41798

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.)

Hypotheses

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

Assertion

Ref	Expression
dialss	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) ∈ 𝑆)

Proof of Theorem dialss

Dummy variables 𝑎 𝑏 𝑥 are mutually distinct and distinct from all other variables.

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143   class class class wbr 5110   ∘ ccom 5667  ‘cfv 6538  (class class class)co 7412  Basecbs 17270  +_gcplusg 17311  Scalarcsca 17314   ·_𝑠 cvsca 17315  lecple 17318  joincjn 18368  Latclat 18488  LSubSpclss 21033  HLchlt 40102  LHypclh 40736  LTrncltrn 40853  trLctrl 40910  TEndoctendo 41504  DVecAcdveca 41754  DIsoAcdia 41780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5239  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-cnex 11157  ax-resscn 11158  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-addrcl 11162  ax-mulcl 11163  ax-mulrcl 11164  ax-mulcom 11165  ax-addass 11166  ax-mulass 11167  ax-distr 11168  ax-i2m1 11169  ax-1ne0 11170  ax-1rid 11171  ax-rnegex 11172  ax-rrecex 11173  ax-cnre 11174  ax-pre-lttri 11175  ax-pre-lttrn 11176  ax-pre-ltadd 11177  ax-pre-mulgt0 11178  ax-riotaBAD 39705

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-tp 4595  df-op 4597  df-uni 4874  df-iun 4959  df-iin 4960  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7864  df-1st 7987  df-2nd 7988  df-undef 8270  df-frecs 8279  df-wrecs 8310  df-recs 8359  df-rdg 8398  df-1o 8454  df-er 8695  df-map 8827  df-en 8945  df-dom 8946  df-sdom 8947  df-fin 8948  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11444  df-neg 11445  df-nn 12235  df-2 12304  df-3 12305  df-4 12306  df-5 12307  df-6 12308  df-n0 12506  df-z 12593  df-uz 12864  df-fz 13537  df-struct 17208  df-slot 17243  df-ndx 17255  df-base 17271  df-plusg 17324  df-mulr 17325  df-sca 17327  df-vsca 17328  df-proset 18351  df-poset 18370  df-plt 18385  df-lub 18401  df-glb 18402  df-join 18403  df-meet 18404  df-p0 18480  df-p1 18481  df-lat 18489  df-clat 18556  df-lss 21034  df-oposet 39928  df-ol 39930  df-oml 39931  df-covers 40018  df-ats 40019  df-atl 40050  df-cvlat 40074  df-hlat 40103  df-llines 40250  df-lplanes 40251  df-lvols 40252  df-lines 40253  df-psubsp 40255  df-pmap 40256  df-padd 40548  df-lhyp 40740  df-laut 40741  df-ldil 40856  df-ltrn 40857  df-trl 40911  df-tendo 41507  df-edring 41509  df-dveca 41755  df-disoa 41781

This theorem is referenced by:  diasslssN  41811  dia2dimlem5  41820  dia2dimlem7  41822  dia2dimlem9  41824  dia2dimlem10  41825  dia2dimlem13  41828  diblsmopel  41923