plngrotlem3

	Ref	Expression
Hypotheses	plngval.p	$⊢ P = {Base}_{G}$
	plngval.i	$⊢ I = Itv (G)$
	plngval.1	$⊢ L = {Line}_{𝒢} (G)$
	plngval.e	No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
	plngval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	plngrot.x	$⊢ φ \to X \in (P ∖ (Z L Y))$
	plngrot.y	$⊢ φ \to Y \in P$
	plngrot.z	$⊢ φ \to Z \in (P ∖ (X L Y))$
	plngrot.1	$⊢ φ \to X \neq Y$
	plngrotlem3.1	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ (X L Y)) \land b \in (P ∖ (X L Y))) \land \exists t \in (X L Y) t \in (a I b))\}$
Assertion	plngrotlem3	$⊢ φ \to (X L Y) E Z \subseteq (Z L Y) E X$

Proof

Step	Hyp	Ref	Expression
1		plngval.p	$⊢ P = {Base}_{G}$
2		plngval.i	$⊢ I = Itv (G)$
3		plngval.1	$⊢ L = {Line}_{𝒢} (G)$
4		plngval.e	Could not format E = ( PlnG ` G ) : No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
5		plngval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		plngrot.x	$⊢ φ \to X \in (P ∖ (Z L Y))$
7		plngrot.y	$⊢ φ \to Y \in P$
8		plngrot.z	$⊢ φ \to Z \in (P ∖ (X L Y))$
9		plngrot.1	$⊢ φ \to X \neq Y$
10		plngrotlem3.1	$⊢ O = \{⟨a, b⟩ \| ((a \in (P ∖ (X L Y)) \land b \in (P ∖ (X L Y))) \land \exists t \in (X L Y) t \in (a I b))\}$
11	5	ad3antrrr	$⊢ (((φ \land w \in P) \land Y \in (Z I w)) \land Y \neq w) \to G \in 𝒢_{Tarski}$
12	6	ad3antrrr	$⊢ (((φ \land w \in P) \land Y \in (Z I w)) \land Y \neq w) \to X \in (P ∖ (Z L Y))$
13	7	ad3antrrr	$⊢ (((φ \land w \in P) \land Y \in (Z I w)) \land Y \neq w) \to Y \in P$
14	8	ad3antrrr	$⊢ (((φ \land w \in P) \land Y \in (Z I w)) \land Y \neq w) \to Z \in (P ∖ (X L Y))$
15	9	ad3antrrr	$⊢ (((φ \land w \in P) \land Y \in (Z I w)) \land Y \neq w) \to X \neq Y$
16		simpllr	$⊢ (((φ \land w \in P) \land Y \in (Z I w)) \land Y \neq w) \to w \in P$
17		simplr	$⊢ (((φ \land w \in P) \land Y \in (Z I w)) \land Y \neq w) \to Y \in (Z I w)$
18		simpr	$⊢ (((φ \land w \in P) \land Y \in (Z I w)) \land Y \neq w) \to Y \neq w$
19	1 2 3 4 11 12 13 14 15 10 16 17 18	plngrotlem2	$⊢ (((φ \land w \in P) \land Y \in (Z I w)) \land Y \neq w) \to (X L Y) E Z \subseteq (Z L Y) E X$
20	19	anasss	$⊢ ((φ \land w \in P) \land (Y \in (Z I w) \land Y \neq w)) \to (X L Y) E Z \subseteq (Z L Y) E X$
21		eqid	$⊢ dist (G) = dist (G)$
22	8	eldifad	$⊢ φ \to Z \in P$
23	1	fvexi	$⊢ P \in V$
24	23	a1i	$⊢ φ \to P \in V$
25	6	eldifad	$⊢ φ \to X \in P$
26	24 25 7 9	nehash2	$⊢ φ \to 2 \leq \|P\|$
27	1 21 2 5 22 7 26	tgbtwndiff	$⊢ φ \to \exists w \in P (Y \in (Z I w) \land Y \neq w)$
28	20 27	r19.29a	$⊢ φ \to (X L Y) E Z \subseteq (Z L Y) E X$

Metamath Proof Explorer

Theorem plngrotlem3

Proof