Theorem dia2dimlem9

Description: Lemma for dia2dim . Eliminate ( RF ) =/= U , V conditions. (Contributed by NM, 8-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		dia2dimlem9.l	⊢ ≤ = ( le ‘ 𝐾 )
2		dia2dimlem9.j	⊢ ∨ = ( join ‘ 𝐾 )
3		dia2dimlem9.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		dia2dimlem9.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		dia2dimlem9.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6		dia2dimlem9.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
7		dia2dimlem9.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
8		dia2dimlem9.y	⊢ 𝑌 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
9		dia2dimlem9.s	⊢ 𝑆 = ( LSubSp ‘ 𝑌 )
10		dia2dimlem9.pl	⊢ ⊕ = ( LSSum ‘ 𝑌 )
11		dia2dimlem9.n	⊢ 𝑁 = ( LSpan ‘ 𝑌 )
12		dia2dimlem9.i	⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
13		dia2dimlem9.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
14		dia2dimlem9.u	⊢ ( 𝜑 → ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) )
15		dia2dimlem9.v	⊢ ( 𝜑 → ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) )
16		dia2dimlem9.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑇 )
17		dia2dimlem9.rf	⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑈 ∨ 𝑉 ) )
18		dia2dimlem9.uv	⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
19	5 8	dvalvec	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑌 ∈ LVec )
20		lveclmod	⊢ ( 𝑌 ∈ LVec → 𝑌 ∈ LMod )
21	9	lsssssubg	⊢ ( 𝑌 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑌 ) )
22	13 19 20 21	4syl	⊢ ( 𝜑 → 𝑆 ⊆ ( SubGrp ‘ 𝑌 ) )
23	14	simpld	⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
24		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
25	24 4	atbase	⊢ ( 𝑈 ∈ 𝐴 → 𝑈 ∈ ( Base ‘ 𝐾 ) )
26	23 25	syl	⊢ ( 𝜑 → 𝑈 ∈ ( Base ‘ 𝐾 ) )
27	14	simprd	⊢ ( 𝜑 → 𝑈 ≤ 𝑊 )
28	24 1 5 8 12 9	dialss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑈 ) ∈ 𝑆 )
29	13 26 27 28	syl12anc	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑈 ) ∈ 𝑆 )
30	22 29	sseldd	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑈 ) ∈ ( SubGrp ‘ 𝑌 ) )
31	15	simpld	⊢ ( 𝜑 → 𝑉 ∈ 𝐴 )
32	24 4	atbase	⊢ ( 𝑉 ∈ 𝐴 → 𝑉 ∈ ( Base ‘ 𝐾 ) )
33	31 32	syl	⊢ ( 𝜑 → 𝑉 ∈ ( Base ‘ 𝐾 ) )
34	15	simprd	⊢ ( 𝜑 → 𝑉 ≤ 𝑊 )
35	24 1 5 8 12 9	dialss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑉 ∈ ( Base ‘ 𝐾 ) ∧ 𝑉 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑉 ) ∈ 𝑆 )
36	13 33 34 35	syl12anc	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑉 ) ∈ 𝑆 )
37	22 36	sseldd	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑉 ) ∈ ( SubGrp ‘ 𝑌 ) )
38	10	lsmub1	⊢ ( ( ( 𝐼 ‘ 𝑈 ) ∈ ( SubGrp ‘ 𝑌 ) ∧ ( 𝐼 ‘ 𝑉 ) ∈ ( SubGrp ‘ 𝑌 ) ) → ( 𝐼 ‘ 𝑈 ) ⊆ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )
39	30 37 38	syl2anc	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑈 ) ⊆ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )
40	39	adantr	⊢ ( ( 𝜑 ∧ ( 𝑅 ‘ 𝐹 ) = 𝑈 ) → ( 𝐼 ‘ 𝑈 ) ⊆ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )
41	5 6 7 12	dia1dimid	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝐹 ∈ ( 𝐼 ‘ ( 𝑅 ‘ 𝐹 ) ) )
42	13 16 41	syl2anc	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐼 ‘ ( 𝑅 ‘ 𝐹 ) ) )
43	42	adantr	⊢ ( ( 𝜑 ∧ ( 𝑅 ‘ 𝐹 ) = 𝑈 ) → 𝐹 ∈ ( 𝐼 ‘ ( 𝑅 ‘ 𝐹 ) ) )
44		fveq2	⊢ ( ( 𝑅 ‘ 𝐹 ) = 𝑈 → ( 𝐼 ‘ ( 𝑅 ‘ 𝐹 ) ) = ( 𝐼 ‘ 𝑈 ) )
45	44	adantl	⊢ ( ( 𝜑 ∧ ( 𝑅 ‘ 𝐹 ) = 𝑈 ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝐹 ) ) = ( 𝐼 ‘ 𝑈 ) )
46	43 45	eleqtrd	⊢ ( ( 𝜑 ∧ ( 𝑅 ‘ 𝐹 ) = 𝑈 ) → 𝐹 ∈ ( 𝐼 ‘ 𝑈 ) )
47	40 46	sseldd	⊢ ( ( 𝜑 ∧ ( 𝑅 ‘ 𝐹 ) = 𝑈 ) → 𝐹 ∈ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )
48	30	adantr	⊢ ( ( 𝜑 ∧ ( 𝑅 ‘ 𝐹 ) = 𝑉 ) → ( 𝐼 ‘ 𝑈 ) ∈ ( SubGrp ‘ 𝑌 ) )
49	37	adantr	⊢ ( ( 𝜑 ∧ ( 𝑅 ‘ 𝐹 ) = 𝑉 ) → ( 𝐼 ‘ 𝑉 ) ∈ ( SubGrp ‘ 𝑌 ) )
50	10	lsmub2	⊢ ( ( ( 𝐼 ‘ 𝑈 ) ∈ ( SubGrp ‘ 𝑌 ) ∧ ( 𝐼 ‘ 𝑉 ) ∈ ( SubGrp ‘ 𝑌 ) ) → ( 𝐼 ‘ 𝑉 ) ⊆ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )
51	48 49 50	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑅 ‘ 𝐹 ) = 𝑉 ) → ( 𝐼 ‘ 𝑉 ) ⊆ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )
52	42	adantr	⊢ ( ( 𝜑 ∧ ( 𝑅 ‘ 𝐹 ) = 𝑉 ) → 𝐹 ∈ ( 𝐼 ‘ ( 𝑅 ‘ 𝐹 ) ) )
53		fveq2	⊢ ( ( 𝑅 ‘ 𝐹 ) = 𝑉 → ( 𝐼 ‘ ( 𝑅 ‘ 𝐹 ) ) = ( 𝐼 ‘ 𝑉 ) )
54	53	adantl	⊢ ( ( 𝜑 ∧ ( 𝑅 ‘ 𝐹 ) = 𝑉 ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝐹 ) ) = ( 𝐼 ‘ 𝑉 ) )
55	52 54	eleqtrd	⊢ ( ( 𝜑 ∧ ( 𝑅 ‘ 𝐹 ) = 𝑉 ) → 𝐹 ∈ ( 𝐼 ‘ 𝑉 ) )
56	51 55	sseldd	⊢ ( ( 𝜑 ∧ ( 𝑅 ‘ 𝐹 ) = 𝑉 ) → 𝐹 ∈ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )
57	13	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ 𝑈 ∧ ( 𝑅 ‘ 𝐹 ) ≠ 𝑉 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
58	14	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ 𝑈 ∧ ( 𝑅 ‘ 𝐹 ) ≠ 𝑉 ) ) → ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) )
59	15	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ 𝑈 ∧ ( 𝑅 ‘ 𝐹 ) ≠ 𝑉 ) ) → ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) )
60	16	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ 𝑈 ∧ ( 𝑅 ‘ 𝐹 ) ≠ 𝑉 ) ) → 𝐹 ∈ 𝑇 )
61	17	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ 𝑈 ∧ ( 𝑅 ‘ 𝐹 ) ≠ 𝑉 ) ) → ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑈 ∨ 𝑉 ) )
62	18	adantr	⊢ ( ( 𝜑 ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ 𝑈 ∧ ( 𝑅 ‘ 𝐹 ) ≠ 𝑉 ) ) → 𝑈 ≠ 𝑉 )
63		simprl	⊢ ( ( 𝜑 ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ 𝑈 ∧ ( 𝑅 ‘ 𝐹 ) ≠ 𝑉 ) ) → ( 𝑅 ‘ 𝐹 ) ≠ 𝑈 )
64		simprr	⊢ ( ( 𝜑 ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ 𝑈 ∧ ( 𝑅 ‘ 𝐹 ) ≠ 𝑉 ) ) → ( 𝑅 ‘ 𝐹 ) ≠ 𝑉 )
65	1 2 3 4 5 6 7 8 9 10 11 12 57 58 59 60 61 62 63 64	dia2dimlem8	⊢ ( ( 𝜑 ∧ ( ( 𝑅 ‘ 𝐹 ) ≠ 𝑈 ∧ ( 𝑅 ‘ 𝐹 ) ≠ 𝑉 ) ) → 𝐹 ∈ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )
66	47 56 65	pm2.61da2ne	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )