dia2dimlem7

Description: Lemma for dia2dim . Eliminate ( FP ) =/= P condition. (Contributed by NM, 8-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		dia2dimlem7.l	⊢ ≤ = ( le ‘ 𝐾 )
2		dia2dimlem7.j	⊢ ∨ = ( join ‘ 𝐾 )
3		dia2dimlem7.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		dia2dimlem7.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
5		dia2dimlem7.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
6		dia2dimlem7.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
7		dia2dimlem7.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
8		dia2dimlem7.y	⊢ 𝑌 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
9		dia2dimlem7.s	⊢ 𝑆 = ( LSubSp ‘ 𝑌 )
10		dia2dimlem7.pl	⊢ ⊕ = ( LSSum ‘ 𝑌 )
11		dia2dimlem7.n	⊢ 𝑁 = ( LSpan ‘ 𝑌 )
12		dia2dimlem7.i	⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
13		dia2dimlem7.q	⊢ 𝑄 = ( ( 𝑃 ∨ 𝑈 ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∨ 𝑉 ) )
14		dia2dimlem7.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
15		dia2dimlem7.u	⊢ ( 𝜑 → ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) )
16		dia2dimlem7.v	⊢ ( 𝜑 → ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) )
17		dia2dimlem7.p	⊢ ( 𝜑 → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
18		dia2dimlem7.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑇 )
19		dia2dimlem7.rf	⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑈 ∨ 𝑉 ) )
20		dia2dimlem7.uv	⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
21		dia2dimlem7.ru	⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ≠ 𝑈 )
22		dia2dimlem7.rv	⊢ ( 𝜑 → ( 𝑅 ‘ 𝐹 ) ≠ 𝑉 )
23		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
24	23 1 4 5 6	ltrnideq	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) → ( 𝐹 = ( I ↾ ( Base ‘ 𝐾 ) ) ↔ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) )
25	14 18 17 24	syl3anc	⊢ ( 𝜑 → ( 𝐹 = ( I ↾ ( Base ‘ 𝐾 ) ) ↔ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) )
26		eqid	⊢ ( 0_g ‘ 𝑌 ) = ( 0_g ‘ 𝑌 )
27	23 5 6 8 26	dva0g	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 0_g ‘ 𝑌 ) = ( I ↾ ( Base ‘ 𝐾 ) ) )
28	14 27	syl	⊢ ( 𝜑 → ( 0_g ‘ 𝑌 ) = ( I ↾ ( Base ‘ 𝐾 ) ) )
29	5 8	dvalvec	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑌 ∈ LVec )
30		lveclmod	⊢ ( 𝑌 ∈ LVec → 𝑌 ∈ LMod )
31	14 29 30	3syl	⊢ ( 𝜑 → 𝑌 ∈ LMod )
32	15	simpld	⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
33	23 4	atbase	⊢ ( 𝑈 ∈ 𝐴 → 𝑈 ∈ ( Base ‘ 𝐾 ) )
34	32 33	syl	⊢ ( 𝜑 → 𝑈 ∈ ( Base ‘ 𝐾 ) )
35	15	simprd	⊢ ( 𝜑 → 𝑈 ≤ 𝑊 )
36	23 1 5 8 12 9	dialss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ 𝑈 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑈 ) ∈ 𝑆 )
37	14 34 35 36	syl12anc	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑈 ) ∈ 𝑆 )
38	16	simpld	⊢ ( 𝜑 → 𝑉 ∈ 𝐴 )
39	23 4	atbase	⊢ ( 𝑉 ∈ 𝐴 → 𝑉 ∈ ( Base ‘ 𝐾 ) )
40	38 39	syl	⊢ ( 𝜑 → 𝑉 ∈ ( Base ‘ 𝐾 ) )
41	16	simprd	⊢ ( 𝜑 → 𝑉 ≤ 𝑊 )
42	23 1 5 8 12 9	dialss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑉 ∈ ( Base ‘ 𝐾 ) ∧ 𝑉 ≤ 𝑊 ) ) → ( 𝐼 ‘ 𝑉 ) ∈ 𝑆 )
43	14 40 41 42	syl12anc	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑉 ) ∈ 𝑆 )
44	9 10	lsmcl	⊢ ( ( 𝑌 ∈ LMod ∧ ( 𝐼 ‘ 𝑈 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑉 ) ∈ 𝑆 ) → ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) ∈ 𝑆 )
45	31 37 43 44	syl3anc	⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) ∈ 𝑆 )
46	26 9	lss0cl	⊢ ( ( 𝑌 ∈ LMod ∧ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) ∈ 𝑆 ) → ( 0_g ‘ 𝑌 ) ∈ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )
47	31 45 46	syl2anc	⊢ ( 𝜑 → ( 0_g ‘ 𝑌 ) ∈ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )
48	28 47	eqeltrrd	⊢ ( 𝜑 → ( I ↾ ( Base ‘ 𝐾 ) ) ∈ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )
49		eleq1a	⊢ ( ( I ↾ ( Base ‘ 𝐾 ) ) ∈ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) → ( 𝐹 = ( I ↾ ( Base ‘ 𝐾 ) ) → 𝐹 ∈ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) ) )
50	48 49	syl	⊢ ( 𝜑 → ( 𝐹 = ( I ↾ ( Base ‘ 𝐾 ) ) → 𝐹 ∈ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) ) )
51	25 50	sylbird	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑃 ) = 𝑃 → 𝐹 ∈ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) ) )
52	51	imp	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑃 ) = 𝑃 ) → 𝐹 ∈ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )
53	14	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
54	15	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) → ( 𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊 ) )
55	16	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) → ( 𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊 ) )
56	17	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
57	18	anim1i	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) → ( 𝐹 ∈ 𝑇 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) )
58	19	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) → ( 𝑅 ‘ 𝐹 ) ≤ ( 𝑈 ∨ 𝑉 ) )
59	20	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) → 𝑈 ≠ 𝑉 )
60	21	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) → ( 𝑅 ‘ 𝐹 ) ≠ 𝑈 )
61	22	adantr	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) → ( 𝑅 ‘ 𝐹 ) ≠ 𝑉 )
62	1 2 3 4 5 6 7 8 9 10 11 12 13 53 54 55 56 57 58 59 60 61	dia2dimlem6	⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑃 ) ≠ 𝑃 ) → 𝐹 ∈ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )
63	52 62	pm2.61dane	⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐼 ‘ 𝑈 ) ⊕ ( 𝐼 ‘ 𝑉 ) ) )

Metamath Proof Explorer

Theorem dia2dimlem7

Proof