dia2dimlem9

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

	Ref	Expression
Hypotheses	dia2dimlem9.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dia2dimlem9.j	$⊢ \underset{˙}{\lor} = join (K)$
	dia2dimlem9.m	$⊢ \underset{˙}{\land} = meet (K)$
	dia2dimlem9.a	$⊢ A = Atoms (K)$
	dia2dimlem9.h	$⊢ H = LHyp (K)$
	dia2dimlem9.t	$⊢ T = LTrn (K) (W)$
	dia2dimlem9.r	$⊢ R = trL (K) (W)$
	dia2dimlem9.y	$⊢ Y = DVecA (K) (W)$
	dia2dimlem9.s	$⊢ S = LSubSp (Y)$
	dia2dimlem9.pl	$⊢ \underset{˙}{\oplus} = LSSum (Y)$
	dia2dimlem9.n	$⊢ N = LSpan (Y)$
	dia2dimlem9.i	$⊢ I = DIsoA (K) (W)$
	dia2dimlem9.k	$⊢ φ \to (K \in HL \land W \in H)$
	dia2dimlem9.u	$⊢ φ \to (U \in A \land U \underset{˙}{\leq} W)$
	dia2dimlem9.v	$⊢ φ \to (V \in A \land V \underset{˙}{\leq} W)$
	dia2dimlem9.f	$⊢ φ \to F \in T$
	dia2dimlem9.rf	$⊢ φ \to R (F) \underset{˙}{\leq} (U \underset{˙}{\lor} V)$
	dia2dimlem9.uv	$⊢ φ \to U \neq V$
Assertion	dia2dimlem9	$⊢ φ \to F \in (I (U) \underset{˙}{\oplus} I (V))$

Proof

Step	Hyp	Ref	Expression
1		dia2dimlem9.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		dia2dimlem9.j	$⊢ \underset{˙}{\lor} = join (K)$
3		dia2dimlem9.m	$⊢ \underset{˙}{\land} = meet (K)$
4		dia2dimlem9.a	$⊢ A = Atoms (K)$
5		dia2dimlem9.h	$⊢ H = LHyp (K)$
6		dia2dimlem9.t	$⊢ T = LTrn (K) (W)$
7		dia2dimlem9.r	$⊢ R = trL (K) (W)$
8		dia2dimlem9.y	$⊢ Y = DVecA (K) (W)$
9		dia2dimlem9.s	$⊢ S = LSubSp (Y)$
10		dia2dimlem9.pl	$⊢ \underset{˙}{\oplus} = LSSum (Y)$
11		dia2dimlem9.n	$⊢ N = LSpan (Y)$
12		dia2dimlem9.i	$⊢ I = DIsoA (K) (W)$
13		dia2dimlem9.k	$⊢ φ \to (K \in HL \land W \in H)$
14		dia2dimlem9.u	$⊢ φ \to (U \in A \land U \underset{˙}{\leq} W)$
15		dia2dimlem9.v	$⊢ φ \to (V \in A \land V \underset{˙}{\leq} W)$
16		dia2dimlem9.f	$⊢ φ \to F \in T$
17		dia2dimlem9.rf	$⊢ φ \to R (F) \underset{˙}{\leq} (U \underset{˙}{\lor} V)$
18		dia2dimlem9.uv	$⊢ φ \to U \neq V$
19	5 8	dvalvec	$⊢ (K \in HL \land W \in H) \to Y \in LVec$
20		lveclmod	$⊢ Y \in LVec \to Y \in LMod$
21	9	lsssssubg	$⊢ Y \in LMod \to S \subseteq SubGrp (Y)$
22	13 19 20 21	4syl	$⊢ φ \to S \subseteq SubGrp (Y)$
23	14	simpld	$⊢ φ \to U \in A$
24		eqid	$⊢ {Base}_{K} = {Base}_{K}$
25	24 4	atbase	$⊢ U \in A \to U \in {Base}_{K}$
26	23 25	syl	$⊢ φ \to U \in {Base}_{K}$
27	14	simprd	$⊢ φ \to U \underset{˙}{\leq} W$
28	24 1 5 8 12 9	dialss	$⊢ ((K \in HL \land W \in H) \land (U \in {Base}_{K} \land U \underset{˙}{\leq} W)) \to I (U) \in S$
29	13 26 27 28	syl12anc	$⊢ φ \to I (U) \in S$
30	22 29	sseldd	$⊢ φ \to I (U) \in SubGrp (Y)$
31	15	simpld	$⊢ φ \to V \in A$
32	24 4	atbase	$⊢ V \in A \to V \in {Base}_{K}$
33	31 32	syl	$⊢ φ \to V \in {Base}_{K}$
34	15	simprd	$⊢ φ \to V \underset{˙}{\leq} W$
35	24 1 5 8 12 9	dialss	$⊢ ((K \in HL \land W \in H) \land (V \in {Base}_{K} \land V \underset{˙}{\leq} W)) \to I (V) \in S$
36	13 33 34 35	syl12anc	$⊢ φ \to I (V) \in S$
37	22 36	sseldd	$⊢ φ \to I (V) \in SubGrp (Y)$
38	10	lsmub1	$⊢ (I (U) \in SubGrp (Y) \land I (V) \in SubGrp (Y)) \to I (U) \subseteq I (U) \underset{˙}{\oplus} I (V)$
39	30 37 38	syl2anc	$⊢ φ \to I (U) \subseteq I (U) \underset{˙}{\oplus} I (V)$
40	39	adantr	$⊢ (φ \land R (F) = U) \to I (U) \subseteq I (U) \underset{˙}{\oplus} I (V)$
41	5 6 7 12	dia1dimid	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F \in I (R (F))$
42	13 16 41	syl2anc	$⊢ φ \to F \in I (R (F))$
43	42	adantr	$⊢ (φ \land R (F) = U) \to F \in I (R (F))$
44		fveq2	$⊢ R (F) = U \to I (R (F)) = I (U)$
45	44	adantl	$⊢ (φ \land R (F) = U) \to I (R (F)) = I (U)$
46	43 45	eleqtrd	$⊢ (φ \land R (F) = U) \to F \in I (U)$
47	40 46	sseldd	$⊢ (φ \land R (F) = U) \to F \in (I (U) \underset{˙}{\oplus} I (V))$
48	30	adantr	$⊢ (φ \land R (F) = V) \to I (U) \in SubGrp (Y)$
49	37	adantr	$⊢ (φ \land R (F) = V) \to I (V) \in SubGrp (Y)$
50	10	lsmub2	$⊢ (I (U) \in SubGrp (Y) \land I (V) \in SubGrp (Y)) \to I (V) \subseteq I (U) \underset{˙}{\oplus} I (V)$
51	48 49 50	syl2anc	$⊢ (φ \land R (F) = V) \to I (V) \subseteq I (U) \underset{˙}{\oplus} I (V)$
52	42	adantr	$⊢ (φ \land R (F) = V) \to F \in I (R (F))$
53		fveq2	$⊢ R (F) = V \to I (R (F)) = I (V)$
54	53	adantl	$⊢ (φ \land R (F) = V) \to I (R (F)) = I (V)$
55	52 54	eleqtrd	$⊢ (φ \land R (F) = V) \to F \in I (V)$
56	51 55	sseldd	$⊢ (φ \land R (F) = V) \to F \in (I (U) \underset{˙}{\oplus} I (V))$
57	13	adantr	$⊢ (φ \land (R (F) \neq U \land R (F) \neq V)) \to (K \in HL \land W \in H)$
58	14	adantr	$⊢ (φ \land (R (F) \neq U \land R (F) \neq V)) \to (U \in A \land U \underset{˙}{\leq} W)$
59	15	adantr	$⊢ (φ \land (R (F) \neq U \land R (F) \neq V)) \to (V \in A \land V \underset{˙}{\leq} W)$
60	16	adantr	$⊢ (φ \land (R (F) \neq U \land R (F) \neq V)) \to F \in T$
61	17	adantr	$⊢ (φ \land (R (F) \neq U \land R (F) \neq V)) \to R (F) \underset{˙}{\leq} (U \underset{˙}{\lor} V)$
62	18	adantr	$⊢ (φ \land (R (F) \neq U \land R (F) \neq V)) \to U \neq V$
63		simprl	$⊢ (φ \land (R (F) \neq U \land R (F) \neq V)) \to R (F) \neq U$
64		simprr	$⊢ (φ \land (R (F) \neq U \land R (F) \neq V)) \to R (F) \neq V$
65	1 2 3 4 5 6 7 8 9 10 11 12 57 58 59 60 61 62 63 64	dia2dimlem8	$⊢ (φ \land (R (F) \neq U \land R (F) \neq V)) \to F \in (I (U) \underset{˙}{\oplus} I (V))$
66	47 56 65	pm2.61da2ne	$⊢ φ \to F \in (I (U) \underset{˙}{\oplus} I (V))$

Metamath Proof Explorer

Theorem dia2dimlem9

Proof