lcfrlem23

Description: Lemma for lcfr . TODO: this proof was built from other proof pieces that may change N{ X , Y } into subspace sum and back unnecessarily, or similar things. (Contributed by NM, 1-Mar-2015)

	Ref	Expression
Hypotheses	lcfrlem17.h	$⊢ H = LHyp (K)$
	lcfrlem17.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	lcfrlem17.u	$⊢ U = DVecH (K) (W)$
	lcfrlem17.v	$⊢ V = {Base}_{U}$
	lcfrlem17.p	$⊢ \underset{˙}{+} = +_{U}$
	lcfrlem17.z	$⊢ \underset{˙}{0} = 0_{U}$
	lcfrlem17.n	$⊢ N = LSpan (U)$
	lcfrlem17.a	$⊢ A = LSAtoms (U)$
	lcfrlem17.k	$⊢ φ \to (K \in HL \land W \in H)$
	lcfrlem17.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
	lcfrlem17.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	lcfrlem17.ne	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
	lcfrlem22.b	$⊢ B = N (\{X, Y\}) \cap \underset{˙}{⊥} (\{X \underset{˙}{+} Y\})$
	lcfrlem23.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
Assertion	lcfrlem23	$⊢ φ \to \underset{˙}{⊥} (\{X, Y\}) \underset{˙}{\oplus} B = \underset{˙}{⊥} (\{X \underset{˙}{+} Y\})$

Proof

Step	Hyp	Ref	Expression
1		lcfrlem17.h	$⊢ H = LHyp (K)$
2		lcfrlem17.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
3		lcfrlem17.u	$⊢ U = DVecH (K) (W)$
4		lcfrlem17.v	$⊢ V = {Base}_{U}$
5		lcfrlem17.p	$⊢ \underset{˙}{+} = +_{U}$
6		lcfrlem17.z	$⊢ \underset{˙}{0} = 0_{U}$
7		lcfrlem17.n	$⊢ N = LSpan (U)$
8		lcfrlem17.a	$⊢ A = LSAtoms (U)$
9		lcfrlem17.k	$⊢ φ \to (K \in HL \land W \in H)$
10		lcfrlem17.x	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
11		lcfrlem17.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
12		lcfrlem17.ne	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
13		lcfrlem22.b	$⊢ B = N (\{X, Y\}) \cap \underset{˙}{⊥} (\{X \underset{˙}{+} Y\})$
14		lcfrlem23.s	$⊢ \underset{˙}{\oplus} = LSSum (U)$
15	13	fveq2i	$⊢ \underset{˙}{⊥} (B) = \underset{˙}{⊥} (N (\{X, Y\}) \cap \underset{˙}{⊥} (\{X \underset{˙}{+} Y\}))$
16		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
17		eqid	$⊢ joinH (K) (W) = joinH (K) (W)$
18	10	eldifad	$⊢ φ \to X \in V$
19	11	eldifad	$⊢ φ \to Y \in V$
20	1 3 4 7 16 9 18 19	dihprrn	$⊢ φ \to N (\{X, Y\}) \in ran DIsoH (K) (W)$
21	1 3 9	dvhlmod	$⊢ φ \to U \in LMod$
22	4 5	lmodvacl	$⊢ (U \in LMod \land X \in V \land Y \in V) \to X \underset{˙}{+} Y \in V$
23	21 18 19 22	syl3anc	$⊢ φ \to X \underset{˙}{+} Y \in V$
24	23	snssd	$⊢ φ \to \{X \underset{˙}{+} Y\} \subseteq V$
25	1 16 3 4 2	dochcl	$⊢ ((K \in HL \land W \in H) \land \{X \underset{˙}{+} Y\} \subseteq V) \to \underset{˙}{⊥} (\{X \underset{˙}{+} Y\}) \in ran DIsoH (K) (W)$
26	9 24 25	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\{X \underset{˙}{+} Y\}) \in ran DIsoH (K) (W)$
27	1 16 3 4 2 17 9 20 26	dochdmm1	$⊢ φ \to \underset{˙}{⊥} (N (\{X, Y\}) \cap \underset{˙}{⊥} (\{X \underset{˙}{+} Y\})) = \underset{˙}{⊥} (N (\{X, Y\})) joinH (K) (W) \underset{˙}{⊥} (\underset{˙}{⊥} (\{X \underset{˙}{+} Y\}))$
28	1 3 2 4 7 9 23	dochocsn	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (\{X \underset{˙}{+} Y\})) = N (\{X \underset{˙}{+} Y\})$
29	28	oveq2d	$⊢ φ \to \underset{˙}{⊥} (N (\{X, Y\})) joinH (K) (W) \underset{˙}{⊥} (\underset{˙}{⊥} (\{X \underset{˙}{+} Y\})) = \underset{˙}{⊥} (N (\{X, Y\})) joinH (K) (W) N (\{X \underset{˙}{+} Y\})$
30		prssi	$⊢ (X \in V \land Y \in V) \to \{X, Y\} \subseteq V$
31	18 19 30	syl2anc	$⊢ φ \to \{X, Y\} \subseteq V$
32	4 7	lspssv	$⊢ (U \in LMod \land \{X, Y\} \subseteq V) \to N (\{X, Y\}) \subseteq V$
33	21 31 32	syl2anc	$⊢ φ \to N (\{X, Y\}) \subseteq V$
34	1 16 3 4 2	dochcl	$⊢ ((K \in HL \land W \in H) \land N (\{X, Y\}) \subseteq V) \to \underset{˙}{⊥} (N (\{X, Y\})) \in ran DIsoH (K) (W)$
35	9 33 34	syl2anc	$⊢ φ \to \underset{˙}{⊥} (N (\{X, Y\})) \in ran DIsoH (K) (W)$
36	1 3 4 14 7 16 17 9 35 23	dihjat1	$⊢ φ \to \underset{˙}{⊥} (N (\{X, Y\})) joinH (K) (W) N (\{X \underset{˙}{+} Y\}) = \underset{˙}{⊥} (N (\{X, Y\})) \underset{˙}{\oplus} N (\{X \underset{˙}{+} Y\})$
37	27 29 36	3eqtrd	$⊢ φ \to \underset{˙}{⊥} (N (\{X, Y\}) \cap \underset{˙}{⊥} (\{X \underset{˙}{+} Y\})) = \underset{˙}{⊥} (N (\{X, Y\})) \underset{˙}{\oplus} N (\{X \underset{˙}{+} Y\})$
38	15 37	eqtrid	$⊢ φ \to \underset{˙}{⊥} (B) = \underset{˙}{⊥} (N (\{X, Y\})) \underset{˙}{\oplus} N (\{X \underset{˙}{+} Y\})$
39	38	ineq2d	$⊢ φ \to (N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) \cap \underset{˙}{⊥} (B) = (N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) \cap (\underset{˙}{⊥} (N (\{X, Y\})) \underset{˙}{\oplus} N (\{X \underset{˙}{+} Y\}))$
40		eqid	$⊢ LSubSp (U) = LSubSp (U)$
41	40	lsssssubg	$⊢ U \in LMod \to LSubSp (U) \subseteq SubGrp (U)$
42	21 41	syl	$⊢ φ \to LSubSp (U) \subseteq SubGrp (U)$
43	4 40 7	lspsncl	$⊢ (U \in LMod \land X \in V) \to N (\{X\}) \in LSubSp (U)$
44	21 18 43	syl2anc	$⊢ φ \to N (\{X\}) \in LSubSp (U)$
45	4 40 7	lspsncl	$⊢ (U \in LMod \land Y \in V) \to N (\{Y\}) \in LSubSp (U)$
46	21 19 45	syl2anc	$⊢ φ \to N (\{Y\}) \in LSubSp (U)$
47	40 14	lsmcl	$⊢ (U \in LMod \land N (\{X\}) \in LSubSp (U) \land N (\{Y\}) \in LSubSp (U)) \to N (\{X\}) \underset{˙}{\oplus} N (\{Y\}) \in LSubSp (U)$
48	21 44 46 47	syl3anc	$⊢ φ \to N (\{X\}) \underset{˙}{\oplus} N (\{Y\}) \in LSubSp (U)$
49	42 48	sseldd	$⊢ φ \to N (\{X\}) \underset{˙}{\oplus} N (\{Y\}) \in SubGrp (U)$
50	1 3 4 40 2	dochlss	$⊢ ((K \in HL \land W \in H) \land N (\{X, Y\}) \subseteq V) \to \underset{˙}{⊥} (N (\{X, Y\})) \in LSubSp (U)$
51	9 33 50	syl2anc	$⊢ φ \to \underset{˙}{⊥} (N (\{X, Y\})) \in LSubSp (U)$
52	42 51	sseldd	$⊢ φ \to \underset{˙}{⊥} (N (\{X, Y\})) \in SubGrp (U)$
53	4 40 7	lspsncl	$⊢ (U \in LMod \land X \underset{˙}{+} Y \in V) \to N (\{X \underset{˙}{+} Y\}) \in LSubSp (U)$
54	21 23 53	syl2anc	$⊢ φ \to N (\{X \underset{˙}{+} Y\}) \in LSubSp (U)$
55	42 54	sseldd	$⊢ φ \to N (\{X \underset{˙}{+} Y\}) \in SubGrp (U)$
56	4 5 7 14	lspsntri	$⊢ (U \in LMod \land X \in V \land Y \in V) \to N (\{X \underset{˙}{+} Y\}) \subseteq N (\{X\}) \underset{˙}{\oplus} N (\{Y\})$
57	21 18 19 56	syl3anc	$⊢ φ \to N (\{X \underset{˙}{+} Y\}) \subseteq N (\{X\}) \underset{˙}{\oplus} N (\{Y\})$
58	14	lsmmod2	$⊢ ((N (\{X\}) \underset{˙}{\oplus} N (\{Y\}) \in SubGrp (U) \land \underset{˙}{⊥} (N (\{X, Y\})) \in SubGrp (U) \land N (\{X \underset{˙}{+} Y\}) \in SubGrp (U)) \land N (\{X \underset{˙}{+} Y\}) \subseteq N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) \to (N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) \cap (\underset{˙}{⊥} (N (\{X, Y\})) \underset{˙}{\oplus} N (\{X \underset{˙}{+} Y\})) = ((N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) \cap \underset{˙}{⊥} (N (\{X, Y\}))) \underset{˙}{\oplus} N (\{X \underset{˙}{+} Y\})$
59	49 52 55 57 58	syl31anc	$⊢ φ \to (N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) \cap (\underset{˙}{⊥} (N (\{X, Y\})) \underset{˙}{\oplus} N (\{X \underset{˙}{+} Y\})) = ((N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) \cap \underset{˙}{⊥} (N (\{X, Y\}))) \underset{˙}{\oplus} N (\{X \underset{˙}{+} Y\})$
60	4 7 14 21 18 19	lsmpr	$⊢ φ \to N (\{X, Y\}) = N (\{X\}) \underset{˙}{\oplus} N (\{Y\})$
61	60	ineq1d	$⊢ φ \to N (\{X, Y\}) \cap \underset{˙}{⊥} (N (\{X, Y\})) = (N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) \cap \underset{˙}{⊥} (N (\{X, Y\}))$
62	4 40 7 21 18 19	lspprcl	$⊢ φ \to N (\{X, Y\}) \in LSubSp (U)$
63	1 3 40 6 2	dochnoncon	$⊢ ((K \in HL \land W \in H) \land N (\{X, Y\}) \in LSubSp (U)) \to N (\{X, Y\}) \cap \underset{˙}{⊥} (N (\{X, Y\})) = \{\underset{˙}{0}\}$
64	9 62 63	syl2anc	$⊢ φ \to N (\{X, Y\}) \cap \underset{˙}{⊥} (N (\{X, Y\})) = \{\underset{˙}{0}\}$
65	61 64	eqtr3d	$⊢ φ \to (N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) \cap \underset{˙}{⊥} (N (\{X, Y\})) = \{\underset{˙}{0}\}$
66	65	oveq1d	$⊢ φ \to ((N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) \cap \underset{˙}{⊥} (N (\{X, Y\}))) \underset{˙}{\oplus} N (\{X \underset{˙}{+} Y\}) = \{\underset{˙}{0}\} \underset{˙}{\oplus} N (\{X \underset{˙}{+} Y\})$
67	6 14	lsm02	$⊢ N (\{X \underset{˙}{+} Y\}) \in SubGrp (U) \to \{\underset{˙}{0}\} \underset{˙}{\oplus} N (\{X \underset{˙}{+} Y\}) = N (\{X \underset{˙}{+} Y\})$
68	55 67	syl	$⊢ φ \to \{\underset{˙}{0}\} \underset{˙}{\oplus} N (\{X \underset{˙}{+} Y\}) = N (\{X \underset{˙}{+} Y\})$
69	66 68	eqtrd	$⊢ φ \to ((N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) \cap \underset{˙}{⊥} (N (\{X, Y\}))) \underset{˙}{\oplus} N (\{X \underset{˙}{+} Y\}) = N (\{X \underset{˙}{+} Y\})$
70	39 59 69	3eqtrd	$⊢ φ \to (N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) \cap \underset{˙}{⊥} (B) = N (\{X \underset{˙}{+} Y\})$
71	70	fveq2d	$⊢ φ \to \underset{˙}{⊥} ((N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) \cap \underset{˙}{⊥} (B)) = \underset{˙}{⊥} (N (\{X \underset{˙}{+} Y\}))$
72	1 3 4 14 7 16 9 18 19	dihsmsnrn	$⊢ φ \to N (\{X\}) \underset{˙}{\oplus} N (\{Y\}) \in ran DIsoH (K) (W)$
73	1 2 3 4 5 6 7 8 9 10 11 12 13	lcfrlem22	$⊢ φ \to B \in A$
74	4 8 21 73	lsatssv	$⊢ φ \to B \subseteq V$
75	1 16 3 4 2	dochcl	$⊢ ((K \in HL \land W \in H) \land B \subseteq V) \to \underset{˙}{⊥} (B) \in ran DIsoH (K) (W)$
76	9 74 75	syl2anc	$⊢ φ \to \underset{˙}{⊥} (B) \in ran DIsoH (K) (W)$
77	1 16 3 4 2 17 9 72 76	dochdmm1	$⊢ φ \to \underset{˙}{⊥} ((N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) \cap \underset{˙}{⊥} (B)) = \underset{˙}{⊥} (N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) joinH (K) (W) \underset{˙}{⊥} (\underset{˙}{⊥} (B))$
78	60	fveq2d	$⊢ φ \to \underset{˙}{⊥} (N (\{X, Y\})) = \underset{˙}{⊥} (N (\{X\}) \underset{˙}{\oplus} N (\{Y\}))$
79	1 3 2 4 7 9 31	dochocsp	$⊢ φ \to \underset{˙}{⊥} (N (\{X, Y\})) = \underset{˙}{⊥} (\{X, Y\})$
80	78 79	eqtr3d	$⊢ φ \to \underset{˙}{⊥} (N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) = \underset{˙}{⊥} (\{X, Y\})$
81	1 3 16 8	dih1dimat	$⊢ ((K \in HL \land W \in H) \land B \in A) \to B \in ran DIsoH (K) (W)$
82	9 73 81	syl2anc	$⊢ φ \to B \in ran DIsoH (K) (W)$
83	1 16 2	dochoc	$⊢ ((K \in HL \land W \in H) \land B \in ran DIsoH (K) (W)) \to \underset{˙}{⊥} (\underset{˙}{⊥} (B)) = B$
84	9 82 83	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (B)) = B$
85	80 84	oveq12d	$⊢ φ \to \underset{˙}{⊥} (N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) joinH (K) (W) \underset{˙}{⊥} (\underset{˙}{⊥} (B)) = \underset{˙}{⊥} (\{X, Y\}) joinH (K) (W) B$
86	1 16 3 4 2	dochcl	$⊢ ((K \in HL \land W \in H) \land \{X, Y\} \subseteq V) \to \underset{˙}{⊥} (\{X, Y\}) \in ran DIsoH (K) (W)$
87	9 31 86	syl2anc	$⊢ φ \to \underset{˙}{⊥} (\{X, Y\}) \in ran DIsoH (K) (W)$
88	1 16 17 3 14 8 9 87 73	dihjat2	$⊢ φ \to \underset{˙}{⊥} (\{X, Y\}) joinH (K) (W) B = \underset{˙}{⊥} (\{X, Y\}) \underset{˙}{\oplus} B$
89	77 85 88	3eqtrd	$⊢ φ \to \underset{˙}{⊥} ((N (\{X\}) \underset{˙}{\oplus} N (\{Y\})) \cap \underset{˙}{⊥} (B)) = \underset{˙}{⊥} (\{X, Y\}) \underset{˙}{\oplus} B$
90	1 3 2 4 7 9 24	dochocsp	$⊢ φ \to \underset{˙}{⊥} (N (\{X \underset{˙}{+} Y\})) = \underset{˙}{⊥} (\{X \underset{˙}{+} Y\})$
91	71 89 90	3eqtr3d	$⊢ φ \to \underset{˙}{⊥} (\{X, Y\}) \underset{˙}{\oplus} B = \underset{˙}{⊥} (\{X \underset{˙}{+} Y\})$

Metamath Proof Explorer

Theorem lcfrlem23

Proof