lclkrlem2p

Description: Lemma for lclkr . When B is zero, X and Y must colinear, so their orthocomplements must be comparable. (Contributed by NM, 17-Jan-2015)

	Ref	Expression
Hypotheses	lclkrlem2m.v	$⊢ V = {Base}_{U}$
	lclkrlem2m.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
	lclkrlem2m.s	$⊢ S = Scalar (U)$
	lclkrlem2m.q	$⊢ \underset{˙}{\times} = \cdot_{S}$
	lclkrlem2m.z	$⊢ \underset{˙}{0} = 0_{S}$
	lclkrlem2m.i	$⊢ I = {inv}_{r} (S)$
	lclkrlem2m.m	$⊢ \underset{˙}{-} = -_{U}$
	lclkrlem2m.f	$⊢ F = LFnl (U)$
	lclkrlem2m.d	$⊢ D = LDual (U)$
	lclkrlem2m.p	$⊢ \underset{˙}{+} = +_{D}$
	lclkrlem2m.x	$⊢ φ \to X \in V$
	lclkrlem2m.y	$⊢ φ \to Y \in V$
	lclkrlem2m.e	$⊢ φ \to E \in F$
	lclkrlem2m.g	$⊢ φ \to G \in F$
	lclkrlem2n.n	$⊢ N = LSpan (U)$
	lclkrlem2n.l	$⊢ L = LKer (U)$
	lclkrlem2o.h	$⊢ H = LHyp (K)$
	lclkrlem2o.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	lclkrlem2o.u	$⊢ U = DVecH (K) (W)$
	lclkrlem2o.a	$⊢ \underset{˙}{\oplus} = LSSum (U)$
	lclkrlem2o.k	$⊢ φ \to (K \in HL \land W \in H)$
	lclkrlem2o.b	$⊢ B = X \underset{˙}{-} (((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y)$
	lclkrlem2o.n	$⊢ φ \to (E \underset{˙}{+} G) (Y) \neq \underset{˙}{0}$
	lclkrlem2p.bn	$⊢ φ \to B = 0_{U}$
Assertion	lclkrlem2p	$⊢ φ \to \underset{˙}{⊥} (\{Y\}) \subseteq \underset{˙}{⊥} (\{X\})$

Proof

Step	Hyp	Ref	Expression
1		lclkrlem2m.v	$⊢ V = {Base}_{U}$
2		lclkrlem2m.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
3		lclkrlem2m.s	$⊢ S = Scalar (U)$
4		lclkrlem2m.q	$⊢ \underset{˙}{\times} = \cdot_{S}$
5		lclkrlem2m.z	$⊢ \underset{˙}{0} = 0_{S}$
6		lclkrlem2m.i	$⊢ I = {inv}_{r} (S)$
7		lclkrlem2m.m	$⊢ \underset{˙}{-} = -_{U}$
8		lclkrlem2m.f	$⊢ F = LFnl (U)$
9		lclkrlem2m.d	$⊢ D = LDual (U)$
10		lclkrlem2m.p	$⊢ \underset{˙}{+} = +_{D}$
11		lclkrlem2m.x	$⊢ φ \to X \in V$
12		lclkrlem2m.y	$⊢ φ \to Y \in V$
13		lclkrlem2m.e	$⊢ φ \to E \in F$
14		lclkrlem2m.g	$⊢ φ \to G \in F$
15		lclkrlem2n.n	$⊢ N = LSpan (U)$
16		lclkrlem2n.l	$⊢ L = LKer (U)$
17		lclkrlem2o.h	$⊢ H = LHyp (K)$
18		lclkrlem2o.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
19		lclkrlem2o.u	$⊢ U = DVecH (K) (W)$
20		lclkrlem2o.a	$⊢ \underset{˙}{\oplus} = LSSum (U)$
21		lclkrlem2o.k	$⊢ φ \to (K \in HL \land W \in H)$
22		lclkrlem2o.b	$⊢ B = X \underset{˙}{-} (((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y)$
23		lclkrlem2o.n	$⊢ φ \to (E \underset{˙}{+} G) (Y) \neq \underset{˙}{0}$
24		lclkrlem2p.bn	$⊢ φ \to B = 0_{U}$
25	17 19 21	dvhlmod	$⊢ φ \to U \in LMod$
26		eqid	$⊢ LSubSp (U) = LSubSp (U)$
27	1 26 15	lspsncl	$⊢ (U \in LMod \land Y \in V) \to N (\{Y\}) \in LSubSp (U)$
28	25 12 27	syl2anc	$⊢ φ \to N (\{Y\}) \in LSubSp (U)$
29	1 26	lssss	$⊢ N (\{Y\}) \in LSubSp (U) \to N (\{Y\}) \subseteq V$
30	28 29	syl	$⊢ φ \to N (\{Y\}) \subseteq V$
31	22 24	eqtr3id	$⊢ φ \to X \underset{˙}{-} (((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y) = 0_{U}$
32	3	lmodring	$⊢ U \in LMod \to S \in Ring$
33	25 32	syl	$⊢ φ \to S \in Ring$
34	8 9 10 25 13 14	ldualvaddcl	$⊢ φ \to E \underset{˙}{+} G \in F$
35		eqid	$⊢ {Base}_{S} = {Base}_{S}$
36	3 35 1 8	lflcl	$⊢ (U \in LMod \land E \underset{˙}{+} G \in F \land X \in V) \to (E \underset{˙}{+} G) (X) \in {Base}_{S}$
37	25 34 11 36	syl3anc	$⊢ φ \to (E \underset{˙}{+} G) (X) \in {Base}_{S}$
38	17 19 21	dvhlvec	$⊢ φ \to U \in LVec$
39	3	lvecdrng	$⊢ U \in LVec \to S \in DivRing$
40	38 39	syl	$⊢ φ \to S \in DivRing$
41	3 35 1 8	lflcl	$⊢ (U \in LMod \land E \underset{˙}{+} G \in F \land Y \in V) \to (E \underset{˙}{+} G) (Y) \in {Base}_{S}$
42	25 34 12 41	syl3anc	$⊢ φ \to (E \underset{˙}{+} G) (Y) \in {Base}_{S}$
43	35 5 6	drnginvrcl	$⊢ (S \in DivRing \land (E \underset{˙}{+} G) (Y) \in {Base}_{S} \land (E \underset{˙}{+} G) (Y) \neq \underset{˙}{0}) \to I ((E \underset{˙}{+} G) (Y)) \in {Base}_{S}$
44	40 42 23 43	syl3anc	$⊢ φ \to I ((E \underset{˙}{+} G) (Y)) \in {Base}_{S}$
45	35 4	ringcl	$⊢ (S \in Ring \land (E \underset{˙}{+} G) (X) \in {Base}_{S} \land I ((E \underset{˙}{+} G) (Y)) \in {Base}_{S}) \to (E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y)) \in {Base}_{S}$
46	33 37 44 45	syl3anc	$⊢ φ \to (E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y)) \in {Base}_{S}$
47	1 3 2 35	lmodvscl	$⊢ (U \in LMod \land (E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y)) \in {Base}_{S} \land Y \in V) \to ((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y \in V$
48	25 46 12 47	syl3anc	$⊢ φ \to ((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y \in V$
49		eqid	$⊢ 0_{U} = 0_{U}$
50	1 49 7	lmodsubeq0	$⊢ (U \in LMod \land X \in V \land ((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y \in V) \to (X \underset{˙}{-} (((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y) = 0_{U} \leftrightarrow X = ((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y)$
51	25 11 48 50	syl3anc	$⊢ φ \to (X \underset{˙}{-} (((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y) = 0_{U} \leftrightarrow X = ((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y)$
52	31 51	mpbid	$⊢ φ \to X = ((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y$
53	52	sneqd	$⊢ φ \to \{X\} = \{((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y\}$
54	53	fveq2d	$⊢ φ \to N (\{X\}) = N (\{((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y\})$
55	3 35 1 2 15	lspsnvsi	$⊢ (U \in LMod \land (E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y)) \in {Base}_{S} \land Y \in V) \to N (\{((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y\}) \subseteq N (\{Y\})$
56	25 46 12 55	syl3anc	$⊢ φ \to N (\{((E \underset{˙}{+} G) (X) \underset{˙}{\times} I ((E \underset{˙}{+} G) (Y))) \underset{˙}{\cdot} Y\}) \subseteq N (\{Y\})$
57	54 56	eqsstrd	$⊢ φ \to N (\{X\}) \subseteq N (\{Y\})$
58	17 19 1 18	dochss	$⊢ ((K \in HL \land W \in H) \land N (\{Y\}) \subseteq V \land N (\{X\}) \subseteq N (\{Y\})) \to \underset{˙}{⊥} (N (\{Y\})) \subseteq \underset{˙}{⊥} (N (\{X\}))$
59	21 30 57 58	syl3anc	$⊢ φ \to \underset{˙}{⊥} (N (\{Y\})) \subseteq \underset{˙}{⊥} (N (\{X\}))$
60	12	snssd	$⊢ φ \to \{Y\} \subseteq V$
61	17 19 18 1 15 21 60	dochocsp	$⊢ φ \to \underset{˙}{⊥} (N (\{Y\})) = \underset{˙}{⊥} (\{Y\})$
62	11	snssd	$⊢ φ \to \{X\} \subseteq V$
63	17 19 18 1 15 21 62	dochocsp	$⊢ φ \to \underset{˙}{⊥} (N (\{X\})) = \underset{˙}{⊥} (\{X\})$
64	59 61 63	3sstr3d	$⊢ φ \to \underset{˙}{⊥} (\{Y\}) \subseteq \underset{˙}{⊥} (\{X\})$

Metamath Proof Explorer

Theorem lclkrlem2p

Proof