dia2dimlem5

Description: Lemma for dia2dim . The sum of vectors G and D belongs to the sum of the subspaces generated by them. Thus, F = ( G o. D ) belongs to the subspace sum. Part of proof of Lemma M in Crawley p. 121 line 5. (Contributed by NM, 8-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		dia2dimlem5.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		dia2dimlem5.j	$⊢ \underset{˙}{\lor} = join (K)$
3		dia2dimlem5.m	$⊢ \underset{˙}{\land} = meet (K)$
4		dia2dimlem5.a	$⊢ A = Atoms (K)$
5		dia2dimlem5.h	$⊢ H = LHyp (K)$
6		dia2dimlem5.t	$⊢ T = LTrn (K) (W)$
7		dia2dimlem5.r	$⊢ R = trL (K) (W)$
8		dia2dimlem5.y	$⊢ Y = DVecA (K) (W)$
9		dia2dimlem5.s	$⊢ S = LSubSp (Y)$
10		dia2dimlem5.pl	$⊢ \underset{˙}{\oplus} = LSSum (Y)$
11		dia2dimlem5.n	$⊢ N = LSpan (Y)$
12		dia2dimlem5.i	$⊢ I = DIsoA (K) (W)$
13		dia2dimlem5.q	$⊢ Q = (P \underset{˙}{\lor} U) \underset{˙}{\land} (F (P) \underset{˙}{\lor} V)$
14		dia2dimlem5.k	$⊢ φ \to (K \in HL \land W \in H)$
15		dia2dimlem5.u	$⊢ φ \to (U \in A \land U \underset{˙}{\leq} W)$
16		dia2dimlem5.v	$⊢ φ \to (V \in A \land V \underset{˙}{\leq} W)$
17		dia2dimlem5.p	$⊢ φ \to (P \in A \land \neg P \underset{˙}{\leq} W)$
18		dia2dimlem5.f	$⊢ φ \to (F \in T \land F (P) \neq P)$
19		dia2dimlem5.rf	$⊢ φ \to R (F) \underset{˙}{\leq} (U \underset{˙}{\lor} V)$
20		dia2dimlem5.uv	$⊢ φ \to U \neq V$
21		dia2dimlem5.ru	$⊢ φ \to R (F) \neq U$
22		dia2dimlem5.rv	$⊢ φ \to R (F) \neq V$
23		dia2dimlem5.g	$⊢ φ \to G \in T$
24		dia2dimlem5.gv	$⊢ φ \to G (P) = Q$
25		dia2dimlem5.d	$⊢ φ \to D \in T$
26		dia2dimlem5.dv	$⊢ φ \to D (Q) = F (P)$
27		eqid	$⊢ +_{Y} = +_{Y}$
28	5 6 8 27	dvavadd	$⊢ ((K \in HL \land W \in H) \land (D \in T \land G \in T)) \to D +_{Y} G = D \circ G$
29	14 25 23 28	syl12anc	$⊢ φ \to D +_{Y} G = D \circ G$
30	18	simpld	$⊢ φ \to F \in T$
31	1 4 5 6 14 17 30 23 24 25 26	dia2dimlem4	$⊢ φ \to D \circ G = F$
32	29 31	eqtr2d	$⊢ φ \to F = D +_{Y} G$
33	5 8	dvalvec	$⊢ (K \in HL \land W \in H) \to Y \in LVec$
34		lveclmod	$⊢ Y \in LVec \to Y \in LMod$
35	14 33 34	3syl	$⊢ φ \to Y \in LMod$
36	9	lsssssubg	$⊢ Y \in LMod \to S \subseteq SubGrp (Y)$
37	35 36	syl	$⊢ φ \to S \subseteq SubGrp (Y)$
38	16	simpld	$⊢ φ \to V \in A$
39		eqid	$⊢ {Base}_{K} = {Base}_{K}$
40	39 4	atbase	$⊢ V \in A \to V \in {Base}_{K}$
41	38 40	syl	$⊢ φ \to V \in {Base}_{K}$
42	16	simprd	$⊢ φ \to V \underset{˙}{\leq} W$
43	39 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$
44	14 41 42 43	syl12anc	$⊢ φ \to I (V) \in S$
45	37 44	sseldd	$⊢ φ \to I (V) \in SubGrp (Y)$
46	15	simpld	$⊢ φ \to U \in A$
47	39 4	atbase	$⊢ U \in A \to U \in {Base}_{K}$
48	46 47	syl	$⊢ φ \to U \in {Base}_{K}$
49	15	simprd	$⊢ φ \to U \underset{˙}{\leq} W$
50	39 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$
51	14 48 49 50	syl12anc	$⊢ φ \to I (U) \in S$
52	37 51	sseldd	$⊢ φ \to I (U) \in SubGrp (Y)$
53	5 6 7 8 12 11	dia1dim2	$⊢ ((K \in HL \land W \in H) \land D \in T) \to I (R (D)) = N (\{D\})$
54	14 25 53	syl2anc	$⊢ φ \to I (R (D)) = N (\{D\})$
55	1 2 3 4 5 6 7 13 14 15 16 17 18 19 20 21 22 25 26	dia2dimlem3	$⊢ φ \to R (D) = V$
56	55	fveq2d	$⊢ φ \to I (R (D)) = I (V)$
57		eqss	$⊢ I (R (D)) = I (V) \leftrightarrow (I (R (D)) \subseteq I (V) \land I (V) \subseteq I (R (D)))$
58	56 57	sylib	$⊢ φ \to (I (R (D)) \subseteq I (V) \land I (V) \subseteq I (R (D)))$
59	58	simpld	$⊢ φ \to I (R (D)) \subseteq I (V)$
60	54 59	eqsstrrd	$⊢ φ \to N (\{D\}) \subseteq I (V)$
61		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
62	5 6 8 61	dvavbase	$⊢ (K \in HL \land W \in H) \to {Base}_{Y} = T$
63	14 62	syl	$⊢ φ \to {Base}_{Y} = T$
64	25 63	eleqtrrd	$⊢ φ \to D \in {Base}_{Y}$
65	61 9 11 35 44 64	ellspsn5b	$⊢ φ \to (D \in I (V) \leftrightarrow N (\{D\}) \subseteq I (V))$
66	60 65	mpbird	$⊢ φ \to D \in I (V)$
67	5 6 7 8 12 11	dia1dim2	$⊢ ((K \in HL \land W \in H) \land G \in T) \to I (R (G)) = N (\{G\})$
68	14 23 67	syl2anc	$⊢ φ \to I (R (G)) = N (\{G\})$
69	1 2 3 4 5 6 7 13 14 15 16 17 18 19 22 23 24	dia2dimlem2	$⊢ φ \to R (G) = U$
70	69	fveq2d	$⊢ φ \to I (R (G)) = I (U)$
71		eqss	$⊢ I (R (G)) = I (U) \leftrightarrow (I (R (G)) \subseteq I (U) \land I (U) \subseteq I (R (G)))$
72	70 71	sylib	$⊢ φ \to (I (R (G)) \subseteq I (U) \land I (U) \subseteq I (R (G)))$
73	72	simpld	$⊢ φ \to I (R (G)) \subseteq I (U)$
74	68 73	eqsstrrd	$⊢ φ \to N (\{G\}) \subseteq I (U)$
75	23 63	eleqtrrd	$⊢ φ \to G \in {Base}_{Y}$
76	61 9 11 35 51 75	ellspsn5b	$⊢ φ \to (G \in I (U) \leftrightarrow N (\{G\}) \subseteq I (U))$
77	74 76	mpbird	$⊢ φ \to G \in I (U)$
78	27 10	lsmelvali	$⊢ ((I (V) \in SubGrp (Y) \land I (U) \in SubGrp (Y)) \land (D \in I (V) \land G \in I (U))) \to D +_{Y} G \in (I (V) \underset{˙}{\oplus} I (U))$
79	45 52 66 77 78	syl22anc	$⊢ φ \to D +_{Y} G \in (I (V) \underset{˙}{\oplus} I (U))$
80	32 79	eqeltrd	$⊢ φ \to F \in (I (V) \underset{˙}{\oplus} I (U))$
81		lmodabl	$⊢ Y \in LMod \to Y \in Abel$
82	35 81	syl	$⊢ φ \to Y \in Abel$
83	10	lsmcom	$⊢ (Y \in Abel \land I (V) \in SubGrp (Y) \land I (U) \in SubGrp (Y)) \to I (V) \underset{˙}{\oplus} I (U) = I (U) \underset{˙}{\oplus} I (V)$
84	82 45 52 83	syl3anc	$⊢ φ \to I (V) \underset{˙}{\oplus} I (U) = I (U) \underset{˙}{\oplus} I (V)$
85	80 84	eleqtrd	$⊢ φ \to F \in (I (U) \underset{˙}{\oplus} I (V))$

Metamath Proof Explorer

Theorem dia2dimlem5

Proof