dalem15

Description: Lemma for dath . The axis of perspectivity X is a line. (Contributed by NM, 21-Jul-2012)

	Ref	Expression
Hypotheses	dalema.ph	$⊢ φ \leftrightarrow (((K \in HL \land C \in {Base}_{K}) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \land (Y \in O \land Z \in O) \land ((\neg C \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg C \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land \neg C \underset{˙}{\leq} (R \underset{˙}{\lor} P)) \land (\neg C \underset{˙}{\leq} (S \underset{˙}{\lor} T) \land \neg C \underset{˙}{\leq} (T \underset{˙}{\lor} U) \land \neg C \underset{˙}{\leq} (U \underset{˙}{\lor} S)) \land (C \underset{˙}{\leq} (P \underset{˙}{\lor} S) \land C \underset{˙}{\leq} (Q \underset{˙}{\lor} T) \land C \underset{˙}{\leq} (R \underset{˙}{\lor} U))))$
	dalemc.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dalemc.j	$⊢ \underset{˙}{\lor} = join (K)$
	dalemc.a	$⊢ A = Atoms (K)$
	dalem15.m	$⊢ \underset{˙}{\land} = meet (K)$
	dalem15.n	$⊢ N = LLines (K)$
	dalem15.o	$⊢ O = LPlanes (K)$
	dalem15.y	$⊢ Y = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R$
	dalem15.z	$⊢ Z = (S \underset{˙}{\lor} T) \underset{˙}{\lor} U$
	dalem15.x	$⊢ X = Y \underset{˙}{\land} Z$
Assertion	dalem15	$⊢ (φ \land Y \neq Z) \to X \in N$

Proof

Step	Hyp	Ref	Expression
1		dalema.ph	$⊢ φ \leftrightarrow (((K \in HL \land C \in {Base}_{K}) \land (P \in A \land Q \in A \land R \in A) \land (S \in A \land T \in A \land U \in A)) \land (Y \in O \land Z \in O) \land ((\neg C \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg C \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land \neg C \underset{˙}{\leq} (R \underset{˙}{\lor} P)) \land (\neg C \underset{˙}{\leq} (S \underset{˙}{\lor} T) \land \neg C \underset{˙}{\leq} (T \underset{˙}{\lor} U) \land \neg C \underset{˙}{\leq} (U \underset{˙}{\lor} S)) \land (C \underset{˙}{\leq} (P \underset{˙}{\lor} S) \land C \underset{˙}{\leq} (Q \underset{˙}{\lor} T) \land C \underset{˙}{\leq} (R \underset{˙}{\lor} U))))$
2		dalemc.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dalemc.j	$⊢ \underset{˙}{\lor} = join (K)$
4		dalemc.a	$⊢ A = Atoms (K)$
5		dalem15.m	$⊢ \underset{˙}{\land} = meet (K)$
6		dalem15.n	$⊢ N = LLines (K)$
7		dalem15.o	$⊢ O = LPlanes (K)$
8		dalem15.y	$⊢ Y = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} R$
9		dalem15.z	$⊢ Z = (S \underset{˙}{\lor} T) \underset{˙}{\lor} U$
10		dalem15.x	$⊢ X = Y \underset{˙}{\land} Z$
11		eqid	$⊢ LVols (K) = LVols (K)$
12		eqid	$⊢ Y \underset{˙}{\lor} C = Y \underset{˙}{\lor} C$
13	1 2 3 4 7 11 8 9 12	dalem14	$⊢ (φ \land Y \neq Z) \to Y \underset{˙}{\lor} Z \in LVols (K)$
14	1	dalemkehl	$⊢ φ \to K \in HL$
15	1	dalemyeo	$⊢ φ \to Y \in O$
16	1	dalemzeo	$⊢ φ \to Z \in O$
17	3 5 6 7 11	2lplnmj	$⊢ (K \in HL \land Y \in O \land Z \in O) \to (Y \underset{˙}{\land} Z \in N \leftrightarrow Y \underset{˙}{\lor} Z \in LVols (K))$
18	14 15 16 17	syl3anc	$⊢ φ \to (Y \underset{˙}{\land} Z \in N \leftrightarrow Y \underset{˙}{\lor} Z \in LVols (K))$
19	18	adantr	$⊢ (φ \land Y \neq Z) \to (Y \underset{˙}{\land} Z \in N \leftrightarrow Y \underset{˙}{\lor} Z \in LVols (K))$
20	13 19	mpbird	$⊢ (φ \land Y \neq Z) \to Y \underset{˙}{\land} Z \in N$
21	10 20	eqeltrid	$⊢ (φ \land Y \neq Z) \to X \in N$

Metamath Proof Explorer

Theorem dalem15

Proof