5oalem2

Description: Lemma for orthoarguesian law 5OA. (Contributed by NM, 2-Apr-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	5oalem2.1	$⊢ A \in S_{ℋ}$
	5oalem2.2	$⊢ B \in S_{ℋ}$
	5oalem2.3	$⊢ C \in S_{ℋ}$
	5oalem2.4	$⊢ D \in S_{ℋ}$
Assertion	5oalem2	$⊢ (((x \in A \land y \in B) \land (z \in C \land w \in D)) \land x +_{ℎ} y = z +_{ℎ} w) \to x -_{ℎ} z \in ((A +_{ℋ} C) \cap (B +_{ℋ} D))$

Proof

Step	Hyp	Ref	Expression
1		5oalem2.1	$⊢ A \in S_{ℋ}$
2		5oalem2.2	$⊢ B \in S_{ℋ}$
3		5oalem2.3	$⊢ C \in S_{ℋ}$
4		5oalem2.4	$⊢ D \in S_{ℋ}$
5	1 3	shsvsi	$⊢ (x \in A \land z \in C) \to x -_{ℎ} z \in (A +_{ℋ} C)$
6	5	ad2ant2r	$⊢ ((x \in A \land y \in B) \land (z \in C \land w \in D)) \to x -_{ℎ} z \in (A +_{ℋ} C)$
7	6	adantr	$⊢ (((x \in A \land y \in B) \land (z \in C \land w \in D)) \land x +_{ℎ} y = z +_{ℎ} w) \to x -_{ℎ} z \in (A +_{ℋ} C)$
8	4 2	shsvsi	$⊢ (w \in D \land y \in B) \to w -_{ℎ} y \in (D +_{ℋ} B)$
9	8	ancoms	$⊢ (y \in B \land w \in D) \to w -_{ℎ} y \in (D +_{ℋ} B)$
10	2 4	shscomi	$⊢ B +_{ℋ} D = D +_{ℋ} B$
11	9 10	eleqtrrdi	$⊢ (y \in B \land w \in D) \to w -_{ℎ} y \in (B +_{ℋ} D)$
12	11	ad2ant2l	$⊢ ((x \in A \land y \in B) \land (z \in C \land w \in D)) \to w -_{ℎ} y \in (B +_{ℋ} D)$
13	12	adantr	$⊢ (((x \in A \land y \in B) \land (z \in C \land w \in D)) \land x +_{ℎ} y = z +_{ℎ} w) \to w -_{ℎ} y \in (B +_{ℋ} D)$
14	1	sheli	$⊢ x \in A \to x \in ℋ$
15	2	sheli	$⊢ y \in B \to y \in ℋ$
16	14 15	anim12i	$⊢ (x \in A \land y \in B) \to (x \in ℋ \land y \in ℋ)$
17	3	sheli	$⊢ z \in C \to z \in ℋ$
18	4	sheli	$⊢ w \in D \to w \in ℋ$
19	17 18	anim12i	$⊢ (z \in C \land w \in D) \to (z \in ℋ \land w \in ℋ)$
20	16 19	anim12i	$⊢ ((x \in A \land y \in B) \land (z \in C \land w \in D)) \to ((x \in ℋ \land y \in ℋ) \land (z \in ℋ \land w \in ℋ))$
21		oveq1	$⊢ x +_{ℎ} y = z +_{ℎ} w \to (x +_{ℎ} y) -_{ℎ} (z +_{ℎ} y) = (z +_{ℎ} w) -_{ℎ} (z +_{ℎ} y)$
22	21	adantl	$⊢ (((x \in ℋ \land y \in ℋ) \land (z \in ℋ \land w \in ℋ)) \land x +_{ℎ} y = z +_{ℎ} w) \to (x +_{ℎ} y) -_{ℎ} (z +_{ℎ} y) = (z +_{ℎ} w) -_{ℎ} (z +_{ℎ} y)$
23		simpr	$⊢ (x \in ℋ \land y \in ℋ) \to y \in ℋ$
24	23	anim2i	$⊢ (z \in ℋ \land (x \in ℋ \land y \in ℋ)) \to (z \in ℋ \land y \in ℋ)$
25	24	ancoms	$⊢ ((x \in ℋ \land y \in ℋ) \land z \in ℋ) \to (z \in ℋ \land y \in ℋ)$
26		hvsub4	$⊢ ((x \in ℋ \land y \in ℋ) \land (z \in ℋ \land y \in ℋ)) \to (x +_{ℎ} y) -_{ℎ} (z +_{ℎ} y) = (x -_{ℎ} z) +_{ℎ} (y -_{ℎ} y)$
27	25 26	syldan	$⊢ ((x \in ℋ \land y \in ℋ) \land z \in ℋ) \to (x +_{ℎ} y) -_{ℎ} (z +_{ℎ} y) = (x -_{ℎ} z) +_{ℎ} (y -_{ℎ} y)$
28		hvsubid	$⊢ y \in ℋ \to y -_{ℎ} y = 0_{ℎ}$
29	28	oveq2d	$⊢ y \in ℋ \to (x -_{ℎ} z) +_{ℎ} (y -_{ℎ} y) = (x -_{ℎ} z) +_{ℎ} 0_{ℎ}$
30	29	ad2antlr	$⊢ ((x \in ℋ \land y \in ℋ) \land z \in ℋ) \to (x -_{ℎ} z) +_{ℎ} (y -_{ℎ} y) = (x -_{ℎ} z) +_{ℎ} 0_{ℎ}$
31		hvsubcl	$⊢ (x \in ℋ \land z \in ℋ) \to x -_{ℎ} z \in ℋ$
32		ax-hvaddid	$⊢ x -_{ℎ} z \in ℋ \to (x -_{ℎ} z) +_{ℎ} 0_{ℎ} = x -_{ℎ} z$
33	31 32	syl	$⊢ (x \in ℋ \land z \in ℋ) \to (x -_{ℎ} z) +_{ℎ} 0_{ℎ} = x -_{ℎ} z$
34	33	adantlr	$⊢ ((x \in ℋ \land y \in ℋ) \land z \in ℋ) \to (x -_{ℎ} z) +_{ℎ} 0_{ℎ} = x -_{ℎ} z$
35	27 30 34	3eqtrd	$⊢ ((x \in ℋ \land y \in ℋ) \land z \in ℋ) \to (x +_{ℎ} y) -_{ℎ} (z +_{ℎ} y) = x -_{ℎ} z$
36	35	adantrr	$⊢ ((x \in ℋ \land y \in ℋ) \land (z \in ℋ \land w \in ℋ)) \to (x +_{ℎ} y) -_{ℎ} (z +_{ℎ} y) = x -_{ℎ} z$
37	36	adantr	$⊢ (((x \in ℋ \land y \in ℋ) \land (z \in ℋ \land w \in ℋ)) \land x +_{ℎ} y = z +_{ℎ} w) \to (x +_{ℎ} y) -_{ℎ} (z +_{ℎ} y) = x -_{ℎ} z$
38		simpr	$⊢ (y \in ℋ \land (z \in ℋ \land w \in ℋ)) \to (z \in ℋ \land w \in ℋ)$
39		simpl	$⊢ (z \in ℋ \land w \in ℋ) \to z \in ℋ$
40	39	anim1i	$⊢ ((z \in ℋ \land w \in ℋ) \land y \in ℋ) \to (z \in ℋ \land y \in ℋ)$
41	40	ancoms	$⊢ (y \in ℋ \land (z \in ℋ \land w \in ℋ)) \to (z \in ℋ \land y \in ℋ)$
42		hvsub4	$⊢ ((z \in ℋ \land w \in ℋ) \land (z \in ℋ \land y \in ℋ)) \to (z +_{ℎ} w) -_{ℎ} (z +_{ℎ} y) = (z -_{ℎ} z) +_{ℎ} (w -_{ℎ} y)$
43	38 41 42	syl2anc	$⊢ (y \in ℋ \land (z \in ℋ \land w \in ℋ)) \to (z +_{ℎ} w) -_{ℎ} (z +_{ℎ} y) = (z -_{ℎ} z) +_{ℎ} (w -_{ℎ} y)$
44		hvsubid	$⊢ z \in ℋ \to z -_{ℎ} z = 0_{ℎ}$
45	44	oveq1d	$⊢ z \in ℋ \to (z -_{ℎ} z) +_{ℎ} (w -_{ℎ} y) = 0_{ℎ} +_{ℎ} (w -_{ℎ} y)$
46	45	ad2antrl	$⊢ (y \in ℋ \land (z \in ℋ \land w \in ℋ)) \to (z -_{ℎ} z) +_{ℎ} (w -_{ℎ} y) = 0_{ℎ} +_{ℎ} (w -_{ℎ} y)$
47		hvsubcl	$⊢ (w \in ℋ \land y \in ℋ) \to w -_{ℎ} y \in ℋ$
48		hvaddid2	$⊢ w -_{ℎ} y \in ℋ \to 0_{ℎ} +_{ℎ} (w -_{ℎ} y) = w -_{ℎ} y$
49	47 48	syl	$⊢ (w \in ℋ \land y \in ℋ) \to 0_{ℎ} +_{ℎ} (w -_{ℎ} y) = w -_{ℎ} y$
50	49	ancoms	$⊢ (y \in ℋ \land w \in ℋ) \to 0_{ℎ} +_{ℎ} (w -_{ℎ} y) = w -_{ℎ} y$
51	50	adantrl	$⊢ (y \in ℋ \land (z \in ℋ \land w \in ℋ)) \to 0_{ℎ} +_{ℎ} (w -_{ℎ} y) = w -_{ℎ} y$
52	43 46 51	3eqtrd	$⊢ (y \in ℋ \land (z \in ℋ \land w \in ℋ)) \to (z +_{ℎ} w) -_{ℎ} (z +_{ℎ} y) = w -_{ℎ} y$
53	52	adantll	$⊢ ((x \in ℋ \land y \in ℋ) \land (z \in ℋ \land w \in ℋ)) \to (z +_{ℎ} w) -_{ℎ} (z +_{ℎ} y) = w -_{ℎ} y$
54	53	adantr	$⊢ (((x \in ℋ \land y \in ℋ) \land (z \in ℋ \land w \in ℋ)) \land x +_{ℎ} y = z +_{ℎ} w) \to (z +_{ℎ} w) -_{ℎ} (z +_{ℎ} y) = w -_{ℎ} y$
55	22 37 54	3eqtr3d	$⊢ (((x \in ℋ \land y \in ℋ) \land (z \in ℋ \land w \in ℋ)) \land x +_{ℎ} y = z +_{ℎ} w) \to x -_{ℎ} z = w -_{ℎ} y$
56	55	eleq1d	$⊢ (((x \in ℋ \land y \in ℋ) \land (z \in ℋ \land w \in ℋ)) \land x +_{ℎ} y = z +_{ℎ} w) \to (x -_{ℎ} z \in (B +_{ℋ} D) \leftrightarrow w -_{ℎ} y \in (B +_{ℋ} D))$
57	20 56	sylan	$⊢ (((x \in A \land y \in B) \land (z \in C \land w \in D)) \land x +_{ℎ} y = z +_{ℎ} w) \to (x -_{ℎ} z \in (B +_{ℋ} D) \leftrightarrow w -_{ℎ} y \in (B +_{ℋ} D))$
58	13 57	mpbird	$⊢ (((x \in A \land y \in B) \land (z \in C \land w \in D)) \land x +_{ℎ} y = z +_{ℎ} w) \to x -_{ℎ} z \in (B +_{ℋ} D)$
59	7 58	elind	$⊢ (((x \in A \land y \in B) \land (z \in C \land w \in D)) \land x +_{ℎ} y = z +_{ℎ} w) \to x -_{ℎ} z \in ((A +_{ℋ} C) \cap (B +_{ℋ} D))$

Metamath Proof Explorer

Theorem 5oalem2

Proof