Theorem dia2dimlem12

Description: Lemma for dia2dim . Obtain subset relation. (Contributed by NM, 8-Sep-2014)

	Ref	Expression
Hypotheses	dia2dimlem12.l	⊢ ≤ = ( le ‘ 𝐾 )
	dia2dimlem12.j	⊢ ∨ = ( join ‘ 𝐾 )
	dia2dimlem12.m	⊢ ∧ = ( meet ‘ 𝐾 )
	dia2dimlem12.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	dia2dimlem12.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dia2dimlem12.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	dia2dimlem12.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
	dia2dimlem12.y	⊢ 𝑌 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
	dia2dimlem12.s	⊢ 𝑆 = ( LSubSp ‘ 𝑌 )
	dia2dimlem12.pl	⊢ ⊕ = ( LSSum ‘ 𝑌 )
	dia2dimlem12.n	⊢ 𝑁 = ( LSpan ‘ 𝑌 )
	dia2dimlem12.i	⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
	dia2dimlem12.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	dia2dimlem12.u	⊢ ( 𝜑 → ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) )
	dia2dimlem12.v	⊢ ( 𝜑 → ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) )
	dia2dimlem12.uv	⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
Assertion	dia2dimlem12	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑈 ∨ 𝑉 ) ) ⊆ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dia2dimlem12.l	⊢ ≤ = ( le ‘ 𝐾 )
2		dia2dimlem12.j	⊢ ∨ = ( join ‘ 𝐾 )
3		dia2dimlem12.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		dia2dimlem12.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		dia2dimlem12.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6		dia2dimlem12.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
7		dia2dimlem12.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
8		dia2dimlem12.y	⊢ 𝑌 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
9		dia2dimlem12.s	⊢ 𝑆 = ( LSubSp ‘ 𝑌 )
10		dia2dimlem12.pl	⊢ ⊕ = ( LSSum ‘ 𝑌 )
11		dia2dimlem12.n	⊢ 𝑁 = ( LSpan ‘ 𝑌 )
12		dia2dimlem12.i	⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
13		dia2dimlem12.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
14		dia2dimlem12.u	⊢ ( 𝜑 → ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) )
15		dia2dimlem12.v	⊢ ( 𝜑 → ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) )
16		dia2dimlem12.uv	⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
17	13	simpld	⊢ ( 𝜑 → 𝐾 ∈ HL )
18	14	simpld	⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
19	15	simpld	⊢ ( 𝜑 → 𝑉 ∈ 𝐴 )
20		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
21	20 2 4	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) → ( 𝑈 ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) )
22	17 18 19 21	syl3anc	⊢ ( 𝜑 → ( 𝑈 ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) )
23	14	simprd	⊢ ( 𝜑 → 𝑈 ≤ 𝑊 )
24	15	simprd	⊢ ( 𝜑 → 𝑉 ≤ 𝑊 )
25	17	hllatd	⊢ ( 𝜑 → 𝐾 ∈ Lat )
26	20 4	atbase	⊢ ( 𝑈 ∈ 𝐴 → 𝑈 ∈ ( Base ‘ 𝐾 ) )
27	18 26	syl	⊢ ( 𝜑 → 𝑈 ∈ ( Base ‘ 𝐾 ) )
28	20 4	atbase	⊢ ( 𝑉 ∈ 𝐴 → 𝑉 ∈ ( Base ‘ 𝐾 ) )
29	19 28	syl	⊢ ( 𝜑 → 𝑉 ∈ ( Base ‘ 𝐾 ) )
30	13	simprd	⊢ ( 𝜑 → 𝑊 ∈ 𝐻 )
31	20 5	lhpbase	⊢ ( 𝑊 ∈ 𝐻 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
32	30 31	syl	⊢ ( 𝜑 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
33	20 1 2	latjle12	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ 𝑉 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑈 ≤ 𝑊 ∧ 𝑉 ≤ 𝑊 ) ↔ ( 𝑈 ∨ 𝑉 ) ≤ 𝑊 ) )
34	25 27 29 32 33	syl13anc	⊢ ( 𝜑 → ( ( 𝑈 ≤ 𝑊 ∧ 𝑉 ≤ 𝑊 ) ↔ ( 𝑈 ∨ 𝑉 ) ≤ 𝑊 ) )
35	23 24 34	mpbi2and	⊢ ( 𝜑 → ( 𝑈 ∨ 𝑉 ) ≤ 𝑊 )
36	20 1 5 6 12	diass	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( 𝑈 ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑈 ∨ 𝑉 ) ≤ 𝑊 ) ) → ( 𝐼 ‘ ( 𝑈 ∨ 𝑉 ) ) ⊆ 𝑇 )
37	13 22 35 36	syl12anc	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑈 ∨ 𝑉 ) ) ⊆ 𝑇 )
38	37	sseld	⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐼 ‘ ( 𝑈 ∨ 𝑉 ) ) → 𝑓 ∈ 𝑇 ) )
39	13	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐼 ‘ ( 𝑈 ∨ 𝑉 ) ) ∧ 𝑓 ∈ 𝑇 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
40	14	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐼 ‘ ( 𝑈 ∨ 𝑉 ) ) ∧ 𝑓 ∈ 𝑇 ) → ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) )
41	15	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐼 ‘ ( 𝑈 ∨ 𝑉 ) ) ∧ 𝑓 ∈ 𝑇 ) → ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) )
42		simp3	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐼 ‘ ( 𝑈 ∨ 𝑉 ) ) ∧ 𝑓 ∈ 𝑇 ) → 𝑓 ∈ 𝑇 )
43	16	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐼 ‘ ( 𝑈 ∨ 𝑉 ) ) ∧ 𝑓 ∈ 𝑇 ) → 𝑈 ≠ 𝑉 )
44		simp2	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐼 ‘ ( 𝑈 ∨ 𝑉 ) ) ∧ 𝑓 ∈ 𝑇 ) → 𝑓 ∈ ( 𝐼 ‘ ( 𝑈 ∨ 𝑉 ) ) )
45	1 2 3 4 5 6 7 8 9 10 11 12 39 40 41 42 43 44	dia2dimlem11	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐼 ‘ ( 𝑈 ∨ 𝑉 ) ) ∧ 𝑓 ∈ 𝑇 ) → 𝑓 ∈ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )
46	45	3exp	⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐼 ‘ ( 𝑈 ∨ 𝑉 ) ) → ( 𝑓 ∈ 𝑇 → 𝑓 ∈ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) ) ) )
47	38 46	mpdd	⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐼 ‘ ( 𝑈 ∨ 𝑉 ) ) → 𝑓 ∈ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) ) )
48	47	ssrdv	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑈 ∨ 𝑉 ) ) ⊆ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )