dihprrnlem1N

Description: Lemma for dihprrn , showing one of 4 cases. (Contributed by NM, 30-Aug-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dihprrn.h	$⊢ H = LHyp (K)$
	dihprrn.u	$⊢ U = DVecH (K) (W)$
	dihprrn.v	$⊢ V = {Base}_{U}$
	dihprrn.n	$⊢ N = LSpan (U)$
	dihprrn.i	$⊢ I = DIsoH (K) (W)$
	dihprrn.k	$⊢ φ \to (K \in HL \land W \in H)$
	dihprrn.x	$⊢ φ \to X \in V$
	dihprrn.y	$⊢ φ \to Y \in V$
	dihprrnlem1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dihprrnlem1.o	$⊢ \underset{˙}{0} = 0_{U}$
	dihprrnlem1.nz	$⊢ φ \to Y \neq \underset{˙}{0}$
	dihprrnlem1.x	$⊢ φ \to I^{-1} (N (\{X\})) \underset{˙}{\leq} W$
	dihprrnlem1.y	$⊢ φ \to \neg I^{-1} (N (\{Y\})) \underset{˙}{\leq} W$
Assertion	dihprrnlem1N	$⊢ φ \to N (\{X, Y\}) \in ran I$

Proof

Step	Hyp	Ref	Expression
1		dihprrn.h	$⊢ H = LHyp (K)$
2		dihprrn.u	$⊢ U = DVecH (K) (W)$
3		dihprrn.v	$⊢ V = {Base}_{U}$
4		dihprrn.n	$⊢ N = LSpan (U)$
5		dihprrn.i	$⊢ I = DIsoH (K) (W)$
6		dihprrn.k	$⊢ φ \to (K \in HL \land W \in H)$
7		dihprrn.x	$⊢ φ \to X \in V$
8		dihprrn.y	$⊢ φ \to Y \in V$
9		dihprrnlem1.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
10		dihprrnlem1.o	$⊢ \underset{˙}{0} = 0_{U}$
11		dihprrnlem1.nz	$⊢ φ \to Y \neq \underset{˙}{0}$
12		dihprrnlem1.x	$⊢ φ \to I^{-1} (N (\{X\})) \underset{˙}{\leq} W$
13		dihprrnlem1.y	$⊢ φ \to \neg I^{-1} (N (\{Y\})) \underset{˙}{\leq} W$
14		df-pr	$⊢ \{X, Y\} = \{X\} \cup \{Y\}$
15	14	fveq2i	$⊢ N (\{X, Y\}) = N (\{X\} \cup \{Y\})$
16		eqid	$⊢ {Base}_{K} = {Base}_{K}$
17		eqid	$⊢ join (K) = join (K)$
18		eqid	$⊢ Atoms (K) = Atoms (K)$
19		eqid	$⊢ LSSum (U) = LSSum (U)$
20	1 2 3 4 5	dihlsprn	$⊢ ((K \in HL \land W \in H) \land X \in V) \to N (\{X\}) \in ran I$
21	6 7 20	syl2anc	$⊢ φ \to N (\{X\}) \in ran I$
22	16 1 5	dihcnvcl	$⊢ ((K \in HL \land W \in H) \land N (\{X\}) \in ran I) \to I^{-1} (N (\{X\})) \in {Base}_{K}$
23	6 21 22	syl2anc	$⊢ φ \to I^{-1} (N (\{X\})) \in {Base}_{K}$
24	23 12	jca	$⊢ φ \to (I^{-1} (N (\{X\})) \in {Base}_{K} \land I^{-1} (N (\{X\})) \underset{˙}{\leq} W)$
25	18 1 2 3 10 4 5	dihlspsnat	$⊢ ((K \in HL \land W \in H) \land Y \in V \land Y \neq \underset{˙}{0}) \to I^{-1} (N (\{Y\})) \in Atoms (K)$
26	6 8 11 25	syl3anc	$⊢ φ \to I^{-1} (N (\{Y\})) \in Atoms (K)$
27	26 13	jca	$⊢ φ \to (I^{-1} (N (\{Y\})) \in Atoms (K) \land \neg I^{-1} (N (\{Y\})) \underset{˙}{\leq} W)$
28	16 9 1 17 18 2 19 5 6 24 27	dihjatc	$⊢ φ \to I (I^{-1} (N (\{X\})) join (K) I^{-1} (N (\{Y\}))) = I (I^{-1} (N (\{X\}))) LSSum (U) I (I^{-1} (N (\{Y\})))$
29	1 5	dihcnvid2	$⊢ ((K \in HL \land W \in H) \land N (\{X\}) \in ran I) \to I (I^{-1} (N (\{X\}))) = N (\{X\})$
30	6 21 29	syl2anc	$⊢ φ \to I (I^{-1} (N (\{X\}))) = N (\{X\})$
31	1 2 3 4 5	dihlsprn	$⊢ ((K \in HL \land W \in H) \land Y \in V) \to N (\{Y\}) \in ran I$
32	6 8 31	syl2anc	$⊢ φ \to N (\{Y\}) \in ran I$
33	1 5	dihcnvid2	$⊢ ((K \in HL \land W \in H) \land N (\{Y\}) \in ran I) \to I (I^{-1} (N (\{Y\}))) = N (\{Y\})$
34	6 32 33	syl2anc	$⊢ φ \to I (I^{-1} (N (\{Y\}))) = N (\{Y\})$
35	30 34	oveq12d	$⊢ φ \to I (I^{-1} (N (\{X\}))) LSSum (U) I (I^{-1} (N (\{Y\}))) = N (\{X\}) LSSum (U) N (\{Y\})$
36	1 2 6	dvhlmod	$⊢ φ \to U \in LMod$
37	7	snssd	$⊢ φ \to \{X\} \subseteq V$
38	8	snssd	$⊢ φ \to \{Y\} \subseteq V$
39	3 4 19	lsmsp2	$⊢ (U \in LMod \land \{X\} \subseteq V \land \{Y\} \subseteq V) \to N (\{X\}) LSSum (U) N (\{Y\}) = N (\{X\} \cup \{Y\})$
40	36 37 38 39	syl3anc	$⊢ φ \to N (\{X\}) LSSum (U) N (\{Y\}) = N (\{X\} \cup \{Y\})$
41	28 35 40	3eqtrrd	$⊢ φ \to N (\{X\} \cup \{Y\}) = I (I^{-1} (N (\{X\})) join (K) I^{-1} (N (\{Y\})))$
42	15 41	eqtrid	$⊢ φ \to N (\{X, Y\}) = I (I^{-1} (N (\{X\})) join (K) I^{-1} (N (\{Y\})))$
43	6	simpld	$⊢ φ \to K \in HL$
44	43	hllatd	$⊢ φ \to K \in Lat$
45	16 1 5	dihcnvcl	$⊢ ((K \in HL \land W \in H) \land N (\{Y\}) \in ran I) \to I^{-1} (N (\{Y\})) \in {Base}_{K}$
46	6 32 45	syl2anc	$⊢ φ \to I^{-1} (N (\{Y\})) \in {Base}_{K}$
47	16 17	latjcl	$⊢ (K \in Lat \land I^{-1} (N (\{X\})) \in {Base}_{K} \land I^{-1} (N (\{Y\})) \in {Base}_{K}) \to I^{-1} (N (\{X\})) join (K) I^{-1} (N (\{Y\})) \in {Base}_{K}$
48	44 23 46 47	syl3anc	$⊢ φ \to I^{-1} (N (\{X\})) join (K) I^{-1} (N (\{Y\})) \in {Base}_{K}$
49	16 1 5	dihcl	$⊢ ((K \in HL \land W \in H) \land I^{-1} (N (\{X\})) join (K) I^{-1} (N (\{Y\})) \in {Base}_{K}) \to I (I^{-1} (N (\{X\})) join (K) I^{-1} (N (\{Y\}))) \in ran I$
50	6 48 49	syl2anc	$⊢ φ \to I (I^{-1} (N (\{X\})) join (K) I^{-1} (N (\{Y\}))) \in ran I$
51	42 50	eqeltrd	$⊢ φ \to N (\{X, Y\}) \in ran I$

Metamath Proof Explorer

Theorem dihprrnlem1N

Proof