3oalem2

Description: Lemma for 3OA (weak) orthoarguesian law. (Contributed by NM, 19-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	3oalem1.1	$⊢ B \in C_{ℋ}$
	3oalem1.2	$⊢ C \in C_{ℋ}$
	3oalem1.3	$⊢ R \in C_{ℋ}$
	3oalem1.4	$⊢ S \in C_{ℋ}$
Assertion	3oalem2	$⊢ (((x \in B \land y \in R) \land v = x +_{ℎ} y) \land ((z \in C \land w \in S) \land v = z +_{ℎ} w)) \to v \in (B +_{ℋ} (R \cap (S +_{ℋ} ((B +_{ℋ} C) \cap (R +_{ℋ} S)))))$

Proof

Step	Hyp	Ref	Expression
1		3oalem1.1	$⊢ B \in C_{ℋ}$
2		3oalem1.2	$⊢ C \in C_{ℋ}$
3		3oalem1.3	$⊢ R \in C_{ℋ}$
4		3oalem1.4	$⊢ S \in C_{ℋ}$
5		simplll	$⊢ (((x \in B \land y \in R) \land v = x +_{ℎ} y) \land ((z \in C \land w \in S) \land v = z +_{ℎ} w)) \to x \in B$
6		simpllr	$⊢ (((x \in B \land y \in R) \land v = x +_{ℎ} y) \land ((z \in C \land w \in S) \land v = z +_{ℎ} w)) \to y \in R$
7	1 2 3 4	3oalem1	$⊢ (((x \in B \land y \in R) \land v = x +_{ℎ} y) \land ((z \in C \land w \in S) \land v = z +_{ℎ} w)) \to (((x \in ℋ \land y \in ℋ) \land v \in ℋ) \land (z \in ℋ \land w \in ℋ))$
8		hvaddsub12	$⊢ (y \in ℋ \land w \in ℋ \land w \in ℋ) \to y +_{ℎ} (w -_{ℎ} w) = w +_{ℎ} (y -_{ℎ} w)$
9	8	3anidm23	$⊢ (y \in ℋ \land w \in ℋ) \to y +_{ℎ} (w -_{ℎ} w) = w +_{ℎ} (y -_{ℎ} w)$
10		hvsubid	$⊢ w \in ℋ \to w -_{ℎ} w = 0_{ℎ}$
11	10	oveq2d	$⊢ w \in ℋ \to y +_{ℎ} (w -_{ℎ} w) = y +_{ℎ} 0_{ℎ}$
12		ax-hvaddid	$⊢ y \in ℋ \to y +_{ℎ} 0_{ℎ} = y$
13	11 12	sylan9eqr	$⊢ (y \in ℋ \land w \in ℋ) \to y +_{ℎ} (w -_{ℎ} w) = y$
14	9 13	eqtr3d	$⊢ (y \in ℋ \land w \in ℋ) \to w +_{ℎ} (y -_{ℎ} w) = y$
15	14	ad2ant2l	$⊢ ((x \in ℋ \land y \in ℋ) \land (z \in ℋ \land w \in ℋ)) \to w +_{ℎ} (y -_{ℎ} w) = y$
16	15	adantlr	$⊢ (((x \in ℋ \land y \in ℋ) \land v \in ℋ) \land (z \in ℋ \land w \in ℋ)) \to w +_{ℎ} (y -_{ℎ} w) = y$
17	7 16	syl	$⊢ (((x \in B \land y \in R) \land v = x +_{ℎ} y) \land ((z \in C \land w \in S) \land v = z +_{ℎ} w)) \to w +_{ℎ} (y -_{ℎ} w) = y$
18		simprlr	$⊢ (((x \in B \land y \in R) \land v = x +_{ℎ} y) \land ((z \in C \land w \in S) \land v = z +_{ℎ} w)) \to w \in S$
19		eqtr2	$⊢ (v = x +_{ℎ} y \land v = z +_{ℎ} w) \to x +_{ℎ} y = z +_{ℎ} w$
20	19	oveq1d	$⊢ (v = x +_{ℎ} y \land v = z +_{ℎ} w) \to (x +_{ℎ} y) -_{ℎ} (x +_{ℎ} w) = (z +_{ℎ} w) -_{ℎ} (x +_{ℎ} w)$
21	20	ad2ant2l	$⊢ (((x \in B \land y \in R) \land v = x +_{ℎ} y) \land ((z \in C \land w \in S) \land v = z +_{ℎ} w)) \to (x +_{ℎ} y) -_{ℎ} (x +_{ℎ} w) = (z +_{ℎ} w) -_{ℎ} (x +_{ℎ} w)$
22		simpl	$⊢ (x \in ℋ \land y \in ℋ) \to x \in ℋ$
23	22	anim1i	$⊢ ((x \in ℋ \land y \in ℋ) \land w \in ℋ) \to (x \in ℋ \land w \in ℋ)$
24		hvsub4	$⊢ ((x \in ℋ \land y \in ℋ) \land (x \in ℋ \land w \in ℋ)) \to (x +_{ℎ} y) -_{ℎ} (x +_{ℎ} w) = (x -_{ℎ} x) +_{ℎ} (y -_{ℎ} w)$
25	23 24	syldan	$⊢ ((x \in ℋ \land y \in ℋ) \land w \in ℋ) \to (x +_{ℎ} y) -_{ℎ} (x +_{ℎ} w) = (x -_{ℎ} x) +_{ℎ} (y -_{ℎ} w)$
26		hvsubid	$⊢ x \in ℋ \to x -_{ℎ} x = 0_{ℎ}$
27	26	ad2antrr	$⊢ ((x \in ℋ \land y \in ℋ) \land w \in ℋ) \to x -_{ℎ} x = 0_{ℎ}$
28	27	oveq1d	$⊢ ((x \in ℋ \land y \in ℋ) \land w \in ℋ) \to (x -_{ℎ} x) +_{ℎ} (y -_{ℎ} w) = 0_{ℎ} +_{ℎ} (y -_{ℎ} w)$
29		hvsubcl	$⊢ (y \in ℋ \land w \in ℋ) \to y -_{ℎ} w \in ℋ$
30		hvaddid2	$⊢ y -_{ℎ} w \in ℋ \to 0_{ℎ} +_{ℎ} (y -_{ℎ} w) = y -_{ℎ} w$
31	29 30	syl	$⊢ (y \in ℋ \land w \in ℋ) \to 0_{ℎ} +_{ℎ} (y -_{ℎ} w) = y -_{ℎ} w$
32	31	adantll	$⊢ ((x \in ℋ \land y \in ℋ) \land w \in ℋ) \to 0_{ℎ} +_{ℎ} (y -_{ℎ} w) = y -_{ℎ} w$
33	25 28 32	3eqtrd	$⊢ ((x \in ℋ \land y \in ℋ) \land w \in ℋ) \to (x +_{ℎ} y) -_{ℎ} (x +_{ℎ} w) = y -_{ℎ} w$
34	33	ad2ant2rl	$⊢ (((x \in ℋ \land y \in ℋ) \land v \in ℋ) \land (z \in ℋ \land w \in ℋ)) \to (x +_{ℎ} y) -_{ℎ} (x +_{ℎ} w) = y -_{ℎ} w$
35	7 34	syl	$⊢ (((x \in B \land y \in R) \land v = x +_{ℎ} y) \land ((z \in C \land w \in S) \land v = z +_{ℎ} w)) \to (x +_{ℎ} y) -_{ℎ} (x +_{ℎ} w) = y -_{ℎ} w$
36		simpr	$⊢ (x \in ℋ \land (z \in ℋ \land w \in ℋ)) \to (z \in ℋ \land w \in ℋ)$
37		simpr	$⊢ (z \in ℋ \land w \in ℋ) \to w \in ℋ$
38	37	anim2i	$⊢ (x \in ℋ \land (z \in ℋ \land w \in ℋ)) \to (x \in ℋ \land w \in ℋ)$
39		hvsub4	$⊢ ((z \in ℋ \land w \in ℋ) \land (x \in ℋ \land w \in ℋ)) \to (z +_{ℎ} w) -_{ℎ} (x +_{ℎ} w) = (z -_{ℎ} x) +_{ℎ} (w -_{ℎ} w)$
40	36 38 39	syl2anc	$⊢ (x \in ℋ \land (z \in ℋ \land w \in ℋ)) \to (z +_{ℎ} w) -_{ℎ} (x +_{ℎ} w) = (z -_{ℎ} x) +_{ℎ} (w -_{ℎ} w)$
41	10	ad2antll	$⊢ (x \in ℋ \land (z \in ℋ \land w \in ℋ)) \to w -_{ℎ} w = 0_{ℎ}$
42	41	oveq2d	$⊢ (x \in ℋ \land (z \in ℋ \land w \in ℋ)) \to (z -_{ℎ} x) +_{ℎ} (w -_{ℎ} w) = (z -_{ℎ} x) +_{ℎ} 0_{ℎ}$
43		hvsubcl	$⊢ (z \in ℋ \land x \in ℋ) \to z -_{ℎ} x \in ℋ$
44		ax-hvaddid	$⊢ z -_{ℎ} x \in ℋ \to (z -_{ℎ} x) +_{ℎ} 0_{ℎ} = z -_{ℎ} x$
45	43 44	syl	$⊢ (z \in ℋ \land x \in ℋ) \to (z -_{ℎ} x) +_{ℎ} 0_{ℎ} = z -_{ℎ} x$
46	45	ancoms	$⊢ (x \in ℋ \land z \in ℋ) \to (z -_{ℎ} x) +_{ℎ} 0_{ℎ} = z -_{ℎ} x$
47	46	adantrr	$⊢ (x \in ℋ \land (z \in ℋ \land w \in ℋ)) \to (z -_{ℎ} x) +_{ℎ} 0_{ℎ} = z -_{ℎ} x$
48	40 42 47	3eqtrd	$⊢ (x \in ℋ \land (z \in ℋ \land w \in ℋ)) \to (z +_{ℎ} w) -_{ℎ} (x +_{ℎ} w) = z -_{ℎ} x$
49	48	adantlr	$⊢ ((x \in ℋ \land y \in ℋ) \land (z \in ℋ \land w \in ℋ)) \to (z +_{ℎ} w) -_{ℎ} (x +_{ℎ} w) = z -_{ℎ} x$
50	49	adantlr	$⊢ (((x \in ℋ \land y \in ℋ) \land v \in ℋ) \land (z \in ℋ \land w \in ℋ)) \to (z +_{ℎ} w) -_{ℎ} (x +_{ℎ} w) = z -_{ℎ} x$
51	7 50	syl	$⊢ (((x \in B \land y \in R) \land v = x +_{ℎ} y) \land ((z \in C \land w \in S) \land v = z +_{ℎ} w)) \to (z +_{ℎ} w) -_{ℎ} (x +_{ℎ} w) = z -_{ℎ} x$
52	21 35 51	3eqtr3d	$⊢ (((x \in B \land y \in R) \land v = x +_{ℎ} y) \land ((z \in C \land w \in S) \land v = z +_{ℎ} w)) \to y -_{ℎ} w = z -_{ℎ} x$
53		simpll	$⊢ ((x \in B \land y \in R) \land v = x +_{ℎ} y) \to x \in B$
54		simpll	$⊢ ((z \in C \land w \in S) \land v = z +_{ℎ} w) \to z \in C$
55	2	chshii	$⊢ C \in S_{ℋ}$
56	1	chshii	$⊢ B \in S_{ℋ}$
57	55 56	shsvsi	$⊢ (z \in C \land x \in B) \to z -_{ℎ} x \in (C +_{ℋ} B)$
58	57	ancoms	$⊢ (x \in B \land z \in C) \to z -_{ℎ} x \in (C +_{ℋ} B)$
59	56 55	shscomi	$⊢ B +_{ℋ} C = C +_{ℋ} B$
60	58 59	eleqtrrdi	$⊢ (x \in B \land z \in C) \to z -_{ℎ} x \in (B +_{ℋ} C)$
61	53 54 60	syl2an	$⊢ (((x \in B \land y \in R) \land v = x +_{ℎ} y) \land ((z \in C \land w \in S) \land v = z +_{ℎ} w)) \to z -_{ℎ} x \in (B +_{ℋ} C)$
62	52 61	eqeltrd	$⊢ (((x \in B \land y \in R) \land v = x +_{ℎ} y) \land ((z \in C \land w \in S) \land v = z +_{ℎ} w)) \to y -_{ℎ} w \in (B +_{ℋ} C)$
63		simplr	$⊢ ((x \in B \land y \in R) \land v = x +_{ℎ} y) \to y \in R$
64		simplr	$⊢ ((z \in C \land w \in S) \land v = z +_{ℎ} w) \to w \in S$
65	3	chshii	$⊢ R \in S_{ℋ}$
66	4	chshii	$⊢ S \in S_{ℋ}$
67	65 66	shsvsi	$⊢ (y \in R \land w \in S) \to y -_{ℎ} w \in (R +_{ℋ} S)$
68	63 64 67	syl2an	$⊢ (((x \in B \land y \in R) \land v = x +_{ℎ} y) \land ((z \in C \land w \in S) \land v = z +_{ℎ} w)) \to y -_{ℎ} w \in (R +_{ℋ} S)$
69	62 68	elind	$⊢ (((x \in B \land y \in R) \land v = x +_{ℎ} y) \land ((z \in C \land w \in S) \land v = z +_{ℎ} w)) \to y -_{ℎ} w \in ((B +_{ℋ} C) \cap (R +_{ℋ} S))$
70	56 55	shscli	$⊢ B +_{ℋ} C \in S_{ℋ}$
71	65 66	shscli	$⊢ R +_{ℋ} S \in S_{ℋ}$
72	70 71	shincli	$⊢ (B +_{ℋ} C) \cap (R +_{ℋ} S) \in S_{ℋ}$
73	66 72	shsvai	$⊢ (w \in S \land y -_{ℎ} w \in ((B +_{ℋ} C) \cap (R +_{ℋ} S))) \to w +_{ℎ} (y -_{ℎ} w) \in (S +_{ℋ} ((B +_{ℋ} C) \cap (R +_{ℋ} S)))$
74	18 69 73	syl2anc	$⊢ (((x \in B \land y \in R) \land v = x +_{ℎ} y) \land ((z \in C \land w \in S) \land v = z +_{ℎ} w)) \to w +_{ℎ} (y -_{ℎ} w) \in (S +_{ℋ} ((B +_{ℋ} C) \cap (R +_{ℋ} S)))$
75	17 74	eqeltrrd	$⊢ (((x \in B \land y \in R) \land v = x +_{ℎ} y) \land ((z \in C \land w \in S) \land v = z +_{ℎ} w)) \to y \in (S +_{ℋ} ((B +_{ℋ} C) \cap (R +_{ℋ} S)))$
76	6 75	elind	$⊢ (((x \in B \land y \in R) \land v = x +_{ℎ} y) \land ((z \in C \land w \in S) \land v = z +_{ℎ} w)) \to y \in (R \cap (S +_{ℋ} ((B +_{ℋ} C) \cap (R +_{ℋ} S))))$
77	66 72	shscli	$⊢ S +_{ℋ} ((B +_{ℋ} C) \cap (R +_{ℋ} S)) \in S_{ℋ}$
78	65 77	shincli	$⊢ R \cap (S +_{ℋ} ((B +_{ℋ} C) \cap (R +_{ℋ} S))) \in S_{ℋ}$
79	56 78	shsvai	$⊢ (x \in B \land y \in (R \cap (S +_{ℋ} ((B +_{ℋ} C) \cap (R +_{ℋ} S))))) \to x +_{ℎ} y \in (B +_{ℋ} (R \cap (S +_{ℋ} ((B +_{ℋ} C) \cap (R +_{ℋ} S)))))$
80	5 76 79	syl2anc	$⊢ (((x \in B \land y \in R) \land v = x +_{ℎ} y) \land ((z \in C \land w \in S) \land v = z +_{ℎ} w)) \to x +_{ℎ} y \in (B +_{ℋ} (R \cap (S +_{ℋ} ((B +_{ℋ} C) \cap (R +_{ℋ} S)))))$
81		eleq1	$⊢ v = x +_{ℎ} y \to (v \in (B +_{ℋ} (R \cap (S +_{ℋ} ((B +_{ℋ} C) \cap (R +_{ℋ} S))))) \leftrightarrow x +_{ℎ} y \in (B +_{ℋ} (R \cap (S +_{ℋ} ((B +_{ℋ} C) \cap (R +_{ℋ} S))))))$
82	81	ad2antlr	$⊢ (((x \in B \land y \in R) \land v = x +_{ℎ} y) \land ((z \in C \land w \in S) \land v = z +_{ℎ} w)) \to (v \in (B +_{ℋ} (R \cap (S +_{ℋ} ((B +_{ℋ} C) \cap (R +_{ℋ} S))))) \leftrightarrow x +_{ℎ} y \in (B +_{ℋ} (R \cap (S +_{ℋ} ((B +_{ℋ} C) \cap (R +_{ℋ} S))))))$
83	80 82	mpbird	$⊢ (((x \in B \land y \in R) \land v = x +_{ℎ} y) \land ((z \in C \land w \in S) \land v = z +_{ℎ} w)) \to v \in (B +_{ℋ} (R \cap (S +_{ℋ} ((B +_{ℋ} C) \cap (R +_{ℋ} S)))))$

Metamath Proof Explorer

Theorem 3oalem2

Proof