dia2dimlem8

Description: Lemma for dia2dim . Eliminate no-longer used auxiliary atoms P and Q . (Contributed by NM, 8-Sep-2014)

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

Step	Hyp	Ref	Expression
1		dia2dimlem8.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		dia2dimlem8.j	$⊢ \underset{˙}{\lor} = join (K)$
3		dia2dimlem8.m	$⊢ \underset{˙}{\land} = meet (K)$
4		dia2dimlem8.a	$⊢ A = Atoms (K)$
5		dia2dimlem8.h	$⊢ H = LHyp (K)$
6		dia2dimlem8.t	$⊢ T = LTrn (K) (W)$
7		dia2dimlem8.r	$⊢ R = trL (K) (W)$
8		dia2dimlem8.y	$⊢ Y = DVecA (K) (W)$
9		dia2dimlem8.s	$⊢ S = LSubSp (Y)$
10		dia2dimlem8.pl	$⊢ \underset{˙}{\oplus} = LSSum (Y)$
11		dia2dimlem8.n	$⊢ N = LSpan (Y)$
12		dia2dimlem8.i	$⊢ I = DIsoA (K) (W)$
13		dia2dimlem8.k	$⊢ φ \to (K \in HL \land W \in H)$
14		dia2dimlem8.u	$⊢ φ \to (U \in A \land U \underset{˙}{\leq} W)$
15		dia2dimlem8.v	$⊢ φ \to (V \in A \land V \underset{˙}{\leq} W)$
16		dia2dimlem8.f	$⊢ φ \to F \in T$
17		dia2dimlem8.rf	$⊢ φ \to R (F) \underset{˙}{\leq} (U \underset{˙}{\lor} V)$
18		dia2dimlem8.uv	$⊢ φ \to U \neq V$
19		dia2dimlem8.ru	$⊢ φ \to R (F) \neq U$
20		dia2dimlem8.rv	$⊢ φ \to R (F) \neq V$
21		eqid	$⊢ (oc (K) (W) \underset{˙}{\lor} U) \underset{˙}{\land} (F (oc (K) (W)) \underset{˙}{\lor} V) = (oc (K) (W) \underset{˙}{\lor} U) \underset{˙}{\land} (F (oc (K) (W)) \underset{˙}{\lor} V)$
22		eqid	$⊢ oc (K) = oc (K)$
23	1 22 4 5	lhpocnel	$⊢ (K \in HL \land W \in H) \to (oc (K) (W) \in A \land \neg oc (K) (W) \underset{˙}{\leq} W)$
24	13 23	syl	$⊢ φ \to (oc (K) (W) \in A \land \neg oc (K) (W) \underset{˙}{\leq} W)$
25	1 2 3 4 5 6 7 8 9 10 11 12 21 13 14 15 24 16 17 18 19 20	dia2dimlem7	$⊢ φ \to F \in (I (U) \underset{˙}{\oplus} I (V))$

Metamath Proof Explorer