dia2dimlem6

Description: Lemma for dia2dim . Eliminate auxiliary translations G and D . (Contributed by NM, 8-Sep-2014)

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

Proof

Step	Hyp	Ref	Expression
1		dia2dimlem6.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		dia2dimlem6.j	$⊢ \underset{˙}{\lor} = join (K)$
3		dia2dimlem6.m	$⊢ \underset{˙}{\land} = meet (K)$
4		dia2dimlem6.a	$⊢ A = Atoms (K)$
5		dia2dimlem6.h	$⊢ H = LHyp (K)$
6		dia2dimlem6.t	$⊢ T = LTrn (K) (W)$
7		dia2dimlem6.r	$⊢ R = trL (K) (W)$
8		dia2dimlem6.y	$⊢ Y = DVecA (K) (W)$
9		dia2dimlem6.s	$⊢ S = LSubSp (Y)$
10		dia2dimlem6.pl	$⊢ \underset{˙}{\oplus} = LSSum (Y)$
11		dia2dimlem6.n	$⊢ N = LSpan (Y)$
12		dia2dimlem6.i	$⊢ I = DIsoA (K) (W)$
13		dia2dimlem6.q	$⊢ Q = (P \underset{˙}{\lor} U) \underset{˙}{\land} (F (P) \underset{˙}{\lor} V)$
14		dia2dimlem6.k	$⊢ φ \to (K \in HL \land W \in H)$
15		dia2dimlem6.u	$⊢ φ \to (U \in A \land U \underset{˙}{\leq} W)$
16		dia2dimlem6.v	$⊢ φ \to (V \in A \land V \underset{˙}{\leq} W)$
17		dia2dimlem6.p	$⊢ φ \to (P \in A \land \neg P \underset{˙}{\leq} W)$
18		dia2dimlem6.f	$⊢ φ \to (F \in T \land F (P) \neq P)$
19		dia2dimlem6.rf	$⊢ φ \to R (F) \underset{˙}{\leq} (U \underset{˙}{\lor} V)$
20		dia2dimlem6.uv	$⊢ φ \to U \neq V$
21		dia2dimlem6.ru	$⊢ φ \to R (F) \neq U$
22		dia2dimlem6.rv	$⊢ φ \to R (F) \neq V$
23	1 2 3 4 5 6 7 13 14 15 16 17 18 19 20 21	dia2dimlem1	$⊢ φ \to (Q \in A \land \neg Q \underset{˙}{\leq} W)$
24	18	simpld	$⊢ φ \to F \in T$
25	1 4 5 6	ltrnel	$⊢ ((K \in HL \land W \in H) \land F \in T \land (P \in A \land \neg P \underset{˙}{\leq} W)) \to (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)$
26	14 24 17 25	syl3anc	$⊢ φ \to (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)$
27	1 4 5 6	cdleme50ex	$⊢ ((K \in HL \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W) \land (F (P) \in A \land \neg F (P) \underset{˙}{\leq} W)) \to \exists d \in T d (Q) = F (P)$
28	14 23 26 27	syl3anc	$⊢ φ \to \exists d \in T d (Q) = F (P)$
29	1 4 5 6	cdleme50ex	$⊢ ((K \in HL \land W \in H) \land (P \in A \land \neg P \underset{˙}{\leq} W) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to \exists g \in T g (P) = Q$
30	14 17 23 29	syl3anc	$⊢ φ \to \exists g \in T g (P) = Q$
31	14	3ad2ant1	$⊢ (φ \land (g \in T \land g (P) = Q \land d \in T) \land d (Q) = F (P)) \to (K \in HL \land W \in H)$
32	15	3ad2ant1	$⊢ (φ \land (g \in T \land g (P) = Q \land d \in T) \land d (Q) = F (P)) \to (U \in A \land U \underset{˙}{\leq} W)$
33	16	3ad2ant1	$⊢ (φ \land (g \in T \land g (P) = Q \land d \in T) \land d (Q) = F (P)) \to (V \in A \land V \underset{˙}{\leq} W)$
34	17	3ad2ant1	$⊢ (φ \land (g \in T \land g (P) = Q \land d \in T) \land d (Q) = F (P)) \to (P \in A \land \neg P \underset{˙}{\leq} W)$
35	18	3ad2ant1	$⊢ (φ \land (g \in T \land g (P) = Q \land d \in T) \land d (Q) = F (P)) \to (F \in T \land F (P) \neq P)$
36	19	3ad2ant1	$⊢ (φ \land (g \in T \land g (P) = Q \land d \in T) \land d (Q) = F (P)) \to R (F) \underset{˙}{\leq} (U \underset{˙}{\lor} V)$
37	20	3ad2ant1	$⊢ (φ \land (g \in T \land g (P) = Q \land d \in T) \land d (Q) = F (P)) \to U \neq V$
38	21	3ad2ant1	$⊢ (φ \land (g \in T \land g (P) = Q \land d \in T) \land d (Q) = F (P)) \to R (F) \neq U$
39	22	3ad2ant1	$⊢ (φ \land (g \in T \land g (P) = Q \land d \in T) \land d (Q) = F (P)) \to R (F) \neq V$
40		simp21	$⊢ (φ \land (g \in T \land g (P) = Q \land d \in T) \land d (Q) = F (P)) \to g \in T$
41		simp22	$⊢ (φ \land (g \in T \land g (P) = Q \land d \in T) \land d (Q) = F (P)) \to g (P) = Q$
42		simp23	$⊢ (φ \land (g \in T \land g (P) = Q \land d \in T) \land d (Q) = F (P)) \to d \in T$
43		simp3	$⊢ (φ \land (g \in T \land g (P) = Q \land d \in T) \land d (Q) = F (P)) \to d (Q) = F (P)$
44	1 2 3 4 5 6 7 8 9 10 11 12 13 31 32 33 34 35 36 37 38 39 40 41 42 43	dia2dimlem5	$⊢ (φ \land (g \in T \land g (P) = Q \land d \in T) \land d (Q) = F (P)) \to F \in (I (U) \underset{˙}{\oplus} I (V))$
45	44	3exp	$⊢ φ \to ((g \in T \land g (P) = Q \land d \in T) \to (d (Q) = F (P) \to F \in (I (U) \underset{˙}{\oplus} I (V))))$
46	45	3expd	$⊢ φ \to (g \in T \to (g (P) = Q \to (d \in T \to (d (Q) = F (P) \to F \in (I (U) \underset{˙}{\oplus} I (V))))))$
47	46	rexlimdv	$⊢ φ \to (\exists g \in T g (P) = Q \to (d \in T \to (d (Q) = F (P) \to F \in (I (U) \underset{˙}{\oplus} I (V)))))$
48	30 47	mpd	$⊢ φ \to (d \in T \to (d (Q) = F (P) \to F \in (I (U) \underset{˙}{\oplus} I (V))))$
49	48	rexlimdv	$⊢ φ \to (\exists d \in T d (Q) = F (P) \to F \in (I (U) \underset{˙}{\oplus} I (V)))$
50	28 49	mpd	$⊢ φ \to F \in (I (U) \underset{˙}{\oplus} I (V))$

Metamath Proof Explorer

Theorem dia2dimlem6

Proof