Theorem dia2dimlem13

Description: Lemma for dia2dim . Eliminate U =/= V condition. (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	⊢ ( 𝜑 → ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) )
Assertion	dia2dimlem13	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑈 ∨ 𝑉 ) ) ⊆ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )

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		oveq2	⊢ ( 𝑈 = 𝑉 → ( 𝑈 ∨ 𝑈 ) = ( 𝑈 ∨ 𝑉 ) )
17	16	adantl	⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝑈 ∨ 𝑈 ) = ( 𝑈 ∨ 𝑉 ) )
18	13	simpld	⊢ ( 𝜑 → 𝐾 ∈ HL )
19	14	simpld	⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
20	2 4	hlatjidm	⊢ ( ( 𝐾 ∈ HL ∧ 𝑈 ∈ 𝐴 ) → ( 𝑈 ∨ 𝑈 ) = 𝑈 )
21	18 19 20	syl2anc	⊢ ( 𝜑 → ( 𝑈 ∨ 𝑈 ) = 𝑈 )
22	21	adantr	⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝑈 ∨ 𝑈 ) = 𝑈 )
23	17 22	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝑈 ∨ 𝑉 ) = 𝑈 )
24	23	fveq2d	⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐼 ‘ ( 𝑈 ∨ 𝑉 ) ) = ( 𝐼 ‘ 𝑈 ) )
25		ssid	⊢ ( 𝐼 ‘ 𝑈 ) ⊆ ( 𝐼 ‘ 𝑈 )
26	24 25	eqsstrdi	⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐼 ‘ ( 𝑈 ∨ 𝑉 ) ) ⊆ ( 𝐼 ‘ 𝑈 ) )
27	5 8	dvalvec	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑌 ∈ LVec )
28		lveclmod	⊢ ( 𝑌 ∈ LVec → 𝑌 ∈ LMod )
29	13 27 28	3syl	⊢ ( 𝜑 → 𝑌 ∈ LMod )
30		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
31	30 4	atbase	⊢ ( 𝑈 ∈ 𝐴 → 𝑈 ∈ ( Base ‘ 𝐾 ) )
32	19 31	syl	⊢ ( 𝜑 → 𝑈 ∈ ( Base ‘ 𝐾 ) )
33	14	simprd	⊢ ( 𝜑 → 𝑈 ≤ 𝑊 )
34	30 1 5 8 12 9	dialss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑈 ) ∈ 𝑆 )
35	13 32 33 34	syl12anc	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑈 ) ∈ 𝑆 )
36	9	lsssubg	⊢ ( ( 𝑌 ∈ LMod ∧ ( 𝐼 ‘ 𝑈 ) ∈ 𝑆 ) → ( 𝐼 ‘ 𝑈 ) ∈ ( SubGrp ‘ 𝑌 ) )
37	29 35 36	syl2anc	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑈 ) ∈ ( SubGrp ‘ 𝑌 ) )
38	10	lsmidm	⊢ ( ( 𝐼 ‘ 𝑈 ) ∈ ( SubGrp ‘ 𝑌 ) → ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑈 ) ) = ( 𝐼 ‘ 𝑈 ) )
39	37 38	syl	⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑈 ) ) = ( 𝐼 ‘ 𝑈 ) )
40		fveq2	⊢ ( 𝑈 = 𝑉 → ( 𝐼 ‘ 𝑈 ) = ( 𝐼 ‘ 𝑉 ) )
41	40	oveq2d	⊢ ( 𝑈 = 𝑉 → ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑈 ) ) = ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )
42	39 41	sylan9req	⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐼 ‘ 𝑈 ) = ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )
43	26 42	sseqtrd	⊢ ( ( 𝜑 ∧ 𝑈 = 𝑉 ) → ( 𝐼 ‘ ( 𝑈 ∨ 𝑉 ) ) ⊆ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )
44	13	adantr	⊢ ( ( 𝜑 ∧ 𝑈 ≠ 𝑉 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
45	14	adantr	⊢ ( ( 𝜑 ∧ 𝑈 ≠ 𝑉 ) → ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) )
46	15	adantr	⊢ ( ( 𝜑 ∧ 𝑈 ≠ 𝑉 ) → ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) )
47		simpr	⊢ ( ( 𝜑 ∧ 𝑈 ≠ 𝑉 ) → 𝑈 ≠ 𝑉 )
48	1 2 3 4 5 6 7 8 9 10 11 12 44 45 46 47	dia2dimlem12	⊢ ( ( 𝜑 ∧ 𝑈 ≠ 𝑉 ) → ( 𝐼 ‘ ( 𝑈 ∨ 𝑉 ) ) ⊆ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )
49	43 48	pm2.61dane	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑈 ∨ 𝑉 ) ) ⊆ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )