superpos

Description: Superposition Principle. If A and B are distinct atoms, there exists a third atom, distinct from A and B , that is the superposition of A and B . Definition 3.4-3(a) in MegPav2000 p. 2345 (PDF p. 8). (Contributed by NM, 9-Jun-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	superpos	$⊢ (A \in HAtoms \land B \in HAtoms \land A \neq B) \to \exists x \in HAtoms (x \neq A \land x \neq B \land x \subseteq A \lor_{ℋ} B)$

Proof

Step	Hyp	Ref	Expression
1		atom1d	$⊢ A \in HAtoms \leftrightarrow \exists y \in ℋ (y \neq 0_{ℎ} \land A = span (\{y\}))$
2		atom1d	$⊢ B \in HAtoms \leftrightarrow \exists z \in ℋ (z \neq 0_{ℎ} \land B = span (\{z\}))$
3		reeanv	$⊢ \exists y \in ℋ \exists z \in ℋ ((y \neq 0_{ℎ} \land A = span (\{y\})) \land (z \neq 0_{ℎ} \land B = span (\{z\}))) \leftrightarrow (\exists y \in ℋ (y \neq 0_{ℎ} \land A = span (\{y\})) \land \exists z \in ℋ (z \neq 0_{ℎ} \land B = span (\{z\})))$
4		an4	$⊢ ((y \neq 0_{ℎ} \land A = span (\{y\})) \land (z \neq 0_{ℎ} \land B = span (\{z\}))) \leftrightarrow ((y \neq 0_{ℎ} \land z \neq 0_{ℎ}) \land (A = span (\{y\}) \land B = span (\{z\})))$
5		neeq1	$⊢ A = span (\{y\}) \to (A \neq B \leftrightarrow span (\{y\}) \neq B)$
6		neeq2	$⊢ B = span (\{z\}) \to (span (\{y\}) \neq B \leftrightarrow span (\{y\}) \neq span (\{z\}))$
7	5 6	sylan9bb	$⊢ (A = span (\{y\}) \land B = span (\{z\})) \to (A \neq B \leftrightarrow span (\{y\}) \neq span (\{z\}))$
8	7	adantl	$⊢ (((y \in ℋ \land z \in ℋ) \land (y \neq 0_{ℎ} \land z \neq 0_{ℎ})) \land (A = span (\{y\}) \land B = span (\{z\}))) \to (A \neq B \leftrightarrow span (\{y\}) \neq span (\{z\}))$
9		hvaddcl	$⊢ (y \in ℋ \land z \in ℋ) \to y +_{ℎ} z \in ℋ$
10	9	adantr	$⊢ ((y \in ℋ \land z \in ℋ) \land span (\{y\}) \neq span (\{z\})) \to y +_{ℎ} z \in ℋ$
11		hvaddeq0	$⊢ (y \in ℋ \land z \in ℋ) \to (y +_{ℎ} z = 0_{ℎ} \leftrightarrow y = -1 \cdot_{ℎ} z)$
12		sneq	$⊢ y = -1 \cdot_{ℎ} z \to \{y\} = \{-1 \cdot_{ℎ} z\}$
13	12	fveq2d	$⊢ y = -1 \cdot_{ℎ} z \to span (\{y\}) = span (\{-1 \cdot_{ℎ} z\})$
14		neg1cn	$⊢ - 1 \in ℂ$
15		neg1ne0	$⊢ - 1 \neq 0$
16		spansncol	$⊢ (z \in ℋ \land - 1 \in ℂ \land - 1 \neq 0) \to span (\{-1 \cdot_{ℎ} z\}) = span (\{z\})$
17	14 15 16	mp3an23	$⊢ z \in ℋ \to span (\{-1 \cdot_{ℎ} z\}) = span (\{z\})$
18	13 17	sylan9eqr	$⊢ (z \in ℋ \land y = -1 \cdot_{ℎ} z) \to span (\{y\}) = span (\{z\})$
19	18	ex	$⊢ z \in ℋ \to (y = -1 \cdot_{ℎ} z \to span (\{y\}) = span (\{z\}))$
20	19	adantl	$⊢ (y \in ℋ \land z \in ℋ) \to (y = -1 \cdot_{ℎ} z \to span (\{y\}) = span (\{z\}))$
21	11 20	sylbid	$⊢ (y \in ℋ \land z \in ℋ) \to (y +_{ℎ} z = 0_{ℎ} \to span (\{y\}) = span (\{z\}))$
22	21	necon3d	$⊢ (y \in ℋ \land z \in ℋ) \to (span (\{y\}) \neq span (\{z\}) \to y +_{ℎ} z \neq 0_{ℎ})$
23	22	imp	$⊢ ((y \in ℋ \land z \in ℋ) \land span (\{y\}) \neq span (\{z\})) \to y +_{ℎ} z \neq 0_{ℎ}$
24		spansna	$⊢ (y +_{ℎ} z \in ℋ \land y +_{ℎ} z \neq 0_{ℎ}) \to span (\{y +_{ℎ} z\}) \in HAtoms$
25	10 23 24	syl2anc	$⊢ ((y \in ℋ \land z \in ℋ) \land span (\{y\}) \neq span (\{z\})) \to span (\{y +_{ℎ} z\}) \in HAtoms$
26	25	adantlr	$⊢ (((y \in ℋ \land z \in ℋ) \land (y \neq 0_{ℎ} \land z \neq 0_{ℎ})) \land span (\{y\}) \neq span (\{z\})) \to span (\{y +_{ℎ} z\}) \in HAtoms$
27	26	adantlr	$⊢ ((((y \in ℋ \land z \in ℋ) \land (y \neq 0_{ℎ} \land z \neq 0_{ℎ})) \land (A = span (\{y\}) \land B = span (\{z\}))) \land span (\{y\}) \neq span (\{z\})) \to span (\{y +_{ℎ} z\}) \in HAtoms$
28		eqeq2	$⊢ A = span (\{y\}) \to (span (\{y +_{ℎ} z\}) = A \leftrightarrow span (\{y +_{ℎ} z\}) = span (\{y\}))$
29	28	biimpd	$⊢ A = span (\{y\}) \to (span (\{y +_{ℎ} z\}) = A \to span (\{y +_{ℎ} z\}) = span (\{y\}))$
30		spansneleqi	$⊢ y +_{ℎ} z \in ℋ \to (span (\{y +_{ℎ} z\}) = span (\{y\}) \to y +_{ℎ} z \in span (\{y\}))$
31	9 30	syl	$⊢ (y \in ℋ \land z \in ℋ) \to (span (\{y +_{ℎ} z\}) = span (\{y\}) \to y +_{ℎ} z \in span (\{y\}))$
32		elspansn	$⊢ y \in ℋ \to (y +_{ℎ} z \in span (\{y\}) \leftrightarrow \exists v \in ℂ y +_{ℎ} z = v \cdot_{ℎ} y)$
33	32	adantr	$⊢ (y \in ℋ \land z \in ℋ) \to (y +_{ℎ} z \in span (\{y\}) \leftrightarrow \exists v \in ℂ y +_{ℎ} z = v \cdot_{ℎ} y)$
34		addcl	$⊢ (v \in ℂ \land - 1 \in ℂ) \to v + -1 \in ℂ$
35	14 34	mpan2	$⊢ v \in ℂ \to v + -1 \in ℂ$
36	35	ad2antlr	$⊢ (((y \in ℋ \land z \in ℋ) \land v \in ℂ) \land y +_{ℎ} z = v \cdot_{ℎ} y) \to v + -1 \in ℂ$
37		hvmulcl	$⊢ (v \in ℂ \land y \in ℋ) \to v \cdot_{ℎ} y \in ℋ$
38	37	ancoms	$⊢ (y \in ℋ \land v \in ℂ) \to v \cdot_{ℎ} y \in ℋ$
39	38	adantlr	$⊢ ((y \in ℋ \land z \in ℋ) \land v \in ℂ) \to v \cdot_{ℎ} y \in ℋ$
40		simpll	$⊢ ((y \in ℋ \land z \in ℋ) \land v \in ℂ) \to y \in ℋ$
41		simplr	$⊢ ((y \in ℋ \land z \in ℋ) \land v \in ℂ) \to z \in ℋ$
42		hvsubadd	$⊢ (v \cdot_{ℎ} y \in ℋ \land y \in ℋ \land z \in ℋ) \to ((v \cdot_{ℎ} y) -_{ℎ} y = z \leftrightarrow y +_{ℎ} z = v \cdot_{ℎ} y)$
43	39 40 41 42	syl3anc	$⊢ ((y \in ℋ \land z \in ℋ) \land v \in ℂ) \to ((v \cdot_{ℎ} y) -_{ℎ} y = z \leftrightarrow y +_{ℎ} z = v \cdot_{ℎ} y)$
44	43	biimpar	$⊢ (((y \in ℋ \land z \in ℋ) \land v \in ℂ) \land y +_{ℎ} z = v \cdot_{ℎ} y) \to (v \cdot_{ℎ} y) -_{ℎ} y = z$
45		hvsubval	$⊢ (v \cdot_{ℎ} y \in ℋ \land y \in ℋ) \to (v \cdot_{ℎ} y) -_{ℎ} y = (v \cdot_{ℎ} y) +_{ℎ} (-1 \cdot_{ℎ} y)$
46	37 45	sylancom	$⊢ (v \in ℂ \land y \in ℋ) \to (v \cdot_{ℎ} y) -_{ℎ} y = (v \cdot_{ℎ} y) +_{ℎ} (-1 \cdot_{ℎ} y)$
47		ax-hvdistr2	$⊢ (v \in ℂ \land - 1 \in ℂ \land y \in ℋ) \to (v + -1) \cdot_{ℎ} y = (v \cdot_{ℎ} y) +_{ℎ} (-1 \cdot_{ℎ} y)$
48	14 47	mp3an2	$⊢ (v \in ℂ \land y \in ℋ) \to (v + -1) \cdot_{ℎ} y = (v \cdot_{ℎ} y) +_{ℎ} (-1 \cdot_{ℎ} y)$
49	46 48	eqtr4d	$⊢ (v \in ℂ \land y \in ℋ) \to (v \cdot_{ℎ} y) -_{ℎ} y = (v + -1) \cdot_{ℎ} y$
50	49	ancoms	$⊢ (y \in ℋ \land v \in ℂ) \to (v \cdot_{ℎ} y) -_{ℎ} y = (v + -1) \cdot_{ℎ} y$
51	50	adantlr	$⊢ ((y \in ℋ \land z \in ℋ) \land v \in ℂ) \to (v \cdot_{ℎ} y) -_{ℎ} y = (v + -1) \cdot_{ℎ} y$
52	51	adantr	$⊢ (((y \in ℋ \land z \in ℋ) \land v \in ℂ) \land y +_{ℎ} z = v \cdot_{ℎ} y) \to (v \cdot_{ℎ} y) -_{ℎ} y = (v + -1) \cdot_{ℎ} y$
53	44 52	eqtr3d	$⊢ (((y \in ℋ \land z \in ℋ) \land v \in ℂ) \land y +_{ℎ} z = v \cdot_{ℎ} y) \to z = (v + -1) \cdot_{ℎ} y$
54		oveq1	$⊢ w = v + -1 \to w \cdot_{ℎ} y = (v + -1) \cdot_{ℎ} y$
55	54	rspceeqv	$⊢ (v + -1 \in ℂ \land z = (v + -1) \cdot_{ℎ} y) \to \exists w \in ℂ z = w \cdot_{ℎ} y$
56	36 53 55	syl2anc	$⊢ (((y \in ℋ \land z \in ℋ) \land v \in ℂ) \land y +_{ℎ} z = v \cdot_{ℎ} y) \to \exists w \in ℂ z = w \cdot_{ℎ} y$
57	56	rexlimdva2	$⊢ (y \in ℋ \land z \in ℋ) \to (\exists v \in ℂ y +_{ℎ} z = v \cdot_{ℎ} y \to \exists w \in ℂ z = w \cdot_{ℎ} y)$
58	33 57	sylbid	$⊢ (y \in ℋ \land z \in ℋ) \to (y +_{ℎ} z \in span (\{y\}) \to \exists w \in ℂ z = w \cdot_{ℎ} y)$
59	31 58	syld	$⊢ (y \in ℋ \land z \in ℋ) \to (span (\{y +_{ℎ} z\}) = span (\{y\}) \to \exists w \in ℂ z = w \cdot_{ℎ} y)$
60		elspansn	$⊢ y \in ℋ \to (z \in span (\{y\}) \leftrightarrow \exists w \in ℂ z = w \cdot_{ℎ} y)$
61	60	adantr	$⊢ (y \in ℋ \land z \in ℋ) \to (z \in span (\{y\}) \leftrightarrow \exists w \in ℂ z = w \cdot_{ℎ} y)$
62	59 61	sylibrd	$⊢ (y \in ℋ \land z \in ℋ) \to (span (\{y +_{ℎ} z\}) = span (\{y\}) \to z \in span (\{y\}))$
63	62	adantr	$⊢ ((y \in ℋ \land z \in ℋ) \land z \neq 0_{ℎ}) \to (span (\{y +_{ℎ} z\}) = span (\{y\}) \to z \in span (\{y\}))$
64		spansneleq	$⊢ (y \in ℋ \land z \neq 0_{ℎ}) \to (z \in span (\{y\}) \to span (\{z\}) = span (\{y\}))$
65		eqcom	$⊢ span (\{z\}) = span (\{y\}) \leftrightarrow span (\{y\}) = span (\{z\})$
66	64 65	imbitrdi	$⊢ (y \in ℋ \land z \neq 0_{ℎ}) \to (z \in span (\{y\}) \to span (\{y\}) = span (\{z\}))$
67	66	adantlr	$⊢ ((y \in ℋ \land z \in ℋ) \land z \neq 0_{ℎ}) \to (z \in span (\{y\}) \to span (\{y\}) = span (\{z\}))$
68	63 67	syld	$⊢ ((y \in ℋ \land z \in ℋ) \land z \neq 0_{ℎ}) \to (span (\{y +_{ℎ} z\}) = span (\{y\}) \to span (\{y\}) = span (\{z\}))$
69	29 68	sylan9r	$⊢ (((y \in ℋ \land z \in ℋ) \land z \neq 0_{ℎ}) \land A = span (\{y\})) \to (span (\{y +_{ℎ} z\}) = A \to span (\{y\}) = span (\{z\}))$
70	69	necon3d	$⊢ (((y \in ℋ \land z \in ℋ) \land z \neq 0_{ℎ}) \land A = span (\{y\})) \to (span (\{y\}) \neq span (\{z\}) \to span (\{y +_{ℎ} z\}) \neq A)$
71	70	adantlrl	$⊢ (((y \in ℋ \land z \in ℋ) \land (y \neq 0_{ℎ} \land z \neq 0_{ℎ})) \land A = span (\{y\})) \to (span (\{y\}) \neq span (\{z\}) \to span (\{y +_{ℎ} z\}) \neq A)$
72	71	adantrr	$⊢ (((y \in ℋ \land z \in ℋ) \land (y \neq 0_{ℎ} \land z \neq 0_{ℎ})) \land (A = span (\{y\}) \land B = span (\{z\}))) \to (span (\{y\}) \neq span (\{z\}) \to span (\{y +_{ℎ} z\}) \neq A)$
73	72	imp	$⊢ ((((y \in ℋ \land z \in ℋ) \land (y \neq 0_{ℎ} \land z \neq 0_{ℎ})) \land (A = span (\{y\}) \land B = span (\{z\}))) \land span (\{y\}) \neq span (\{z\})) \to span (\{y +_{ℎ} z\}) \neq A$
74		eqeq2	$⊢ B = span (\{z\}) \to (span (\{y +_{ℎ} z\}) = B \leftrightarrow span (\{y +_{ℎ} z\}) = span (\{z\}))$
75	74	biimpd	$⊢ B = span (\{z\}) \to (span (\{y +_{ℎ} z\}) = B \to span (\{y +_{ℎ} z\}) = span (\{z\}))$
76		spansneleqi	$⊢ y +_{ℎ} z \in ℋ \to (span (\{y +_{ℎ} z\}) = span (\{z\}) \to y +_{ℎ} z \in span (\{z\}))$
77	9 76	syl	$⊢ (y \in ℋ \land z \in ℋ) \to (span (\{y +_{ℎ} z\}) = span (\{z\}) \to y +_{ℎ} z \in span (\{z\}))$
78		elspansn	$⊢ z \in ℋ \to (y +_{ℎ} z \in span (\{z\}) \leftrightarrow \exists v \in ℂ y +_{ℎ} z = v \cdot_{ℎ} z)$
79	78	adantl	$⊢ (y \in ℋ \land z \in ℋ) \to (y +_{ℎ} z \in span (\{z\}) \leftrightarrow \exists v \in ℂ y +_{ℎ} z = v \cdot_{ℎ} z)$
80	35	ad2antlr	$⊢ (((y \in ℋ \land z \in ℋ) \land v \in ℂ) \land y +_{ℎ} z = v \cdot_{ℎ} z) \to v + -1 \in ℂ$
81		hvmulcl	$⊢ (v \in ℂ \land z \in ℋ) \to v \cdot_{ℎ} z \in ℋ$
82	81	ancoms	$⊢ (z \in ℋ \land v \in ℂ) \to v \cdot_{ℎ} z \in ℋ$
83	82	adantll	$⊢ ((y \in ℋ \land z \in ℋ) \land v \in ℂ) \to v \cdot_{ℎ} z \in ℋ$
84		hvsubadd	$⊢ (v \cdot_{ℎ} z \in ℋ \land z \in ℋ \land y \in ℋ) \to ((v \cdot_{ℎ} z) -_{ℎ} z = y \leftrightarrow z +_{ℎ} y = v \cdot_{ℎ} z)$
85	83 41 40 84	syl3anc	$⊢ ((y \in ℋ \land z \in ℋ) \land v \in ℂ) \to ((v \cdot_{ℎ} z) -_{ℎ} z = y \leftrightarrow z +_{ℎ} y = v \cdot_{ℎ} z)$
86		ax-hvcom	$⊢ (y \in ℋ \land z \in ℋ) \to y +_{ℎ} z = z +_{ℎ} y$
87	86	adantr	$⊢ ((y \in ℋ \land z \in ℋ) \land v \in ℂ) \to y +_{ℎ} z = z +_{ℎ} y$
88	87	eqeq1d	$⊢ ((y \in ℋ \land z \in ℋ) \land v \in ℂ) \to (y +_{ℎ} z = v \cdot_{ℎ} z \leftrightarrow z +_{ℎ} y = v \cdot_{ℎ} z)$
89	85 88	bitr4d	$⊢ ((y \in ℋ \land z \in ℋ) \land v \in ℂ) \to ((v \cdot_{ℎ} z) -_{ℎ} z = y \leftrightarrow y +_{ℎ} z = v \cdot_{ℎ} z)$
90	89	biimpar	$⊢ (((y \in ℋ \land z \in ℋ) \land v \in ℂ) \land y +_{ℎ} z = v \cdot_{ℎ} z) \to (v \cdot_{ℎ} z) -_{ℎ} z = y$
91		hvsubval	$⊢ (v \cdot_{ℎ} z \in ℋ \land z \in ℋ) \to (v \cdot_{ℎ} z) -_{ℎ} z = (v \cdot_{ℎ} z) +_{ℎ} (-1 \cdot_{ℎ} z)$
92	81 91	sylancom	$⊢ (v \in ℂ \land z \in ℋ) \to (v \cdot_{ℎ} z) -_{ℎ} z = (v \cdot_{ℎ} z) +_{ℎ} (-1 \cdot_{ℎ} z)$
93		ax-hvdistr2	$⊢ (v \in ℂ \land - 1 \in ℂ \land z \in ℋ) \to (v + -1) \cdot_{ℎ} z = (v \cdot_{ℎ} z) +_{ℎ} (-1 \cdot_{ℎ} z)$
94	14 93	mp3an2	$⊢ (v \in ℂ \land z \in ℋ) \to (v + -1) \cdot_{ℎ} z = (v \cdot_{ℎ} z) +_{ℎ} (-1 \cdot_{ℎ} z)$
95	92 94	eqtr4d	$⊢ (v \in ℂ \land z \in ℋ) \to (v \cdot_{ℎ} z) -_{ℎ} z = (v + -1) \cdot_{ℎ} z$
96	95	ancoms	$⊢ (z \in ℋ \land v \in ℂ) \to (v \cdot_{ℎ} z) -_{ℎ} z = (v + -1) \cdot_{ℎ} z$
97	96	adantll	$⊢ ((y \in ℋ \land z \in ℋ) \land v \in ℂ) \to (v \cdot_{ℎ} z) -_{ℎ} z = (v + -1) \cdot_{ℎ} z$
98	97	adantr	$⊢ (((y \in ℋ \land z \in ℋ) \land v \in ℂ) \land y +_{ℎ} z = v \cdot_{ℎ} z) \to (v \cdot_{ℎ} z) -_{ℎ} z = (v + -1) \cdot_{ℎ} z$
99	90 98	eqtr3d	$⊢ (((y \in ℋ \land z \in ℋ) \land v \in ℂ) \land y +_{ℎ} z = v \cdot_{ℎ} z) \to y = (v + -1) \cdot_{ℎ} z$
100		oveq1	$⊢ w = v + -1 \to w \cdot_{ℎ} z = (v + -1) \cdot_{ℎ} z$
101	100	rspceeqv	$⊢ (v + -1 \in ℂ \land y = (v + -1) \cdot_{ℎ} z) \to \exists w \in ℂ y = w \cdot_{ℎ} z$
102	80 99 101	syl2anc	$⊢ (((y \in ℋ \land z \in ℋ) \land v \in ℂ) \land y +_{ℎ} z = v \cdot_{ℎ} z) \to \exists w \in ℂ y = w \cdot_{ℎ} z$
103	102	rexlimdva2	$⊢ (y \in ℋ \land z \in ℋ) \to (\exists v \in ℂ y +_{ℎ} z = v \cdot_{ℎ} z \to \exists w \in ℂ y = w \cdot_{ℎ} z)$
104	79 103	sylbid	$⊢ (y \in ℋ \land z \in ℋ) \to (y +_{ℎ} z \in span (\{z\}) \to \exists w \in ℂ y = w \cdot_{ℎ} z)$
105	77 104	syld	$⊢ (y \in ℋ \land z \in ℋ) \to (span (\{y +_{ℎ} z\}) = span (\{z\}) \to \exists w \in ℂ y = w \cdot_{ℎ} z)$
106		elspansn	$⊢ z \in ℋ \to (y \in span (\{z\}) \leftrightarrow \exists w \in ℂ y = w \cdot_{ℎ} z)$
107	106	adantl	$⊢ (y \in ℋ \land z \in ℋ) \to (y \in span (\{z\}) \leftrightarrow \exists w \in ℂ y = w \cdot_{ℎ} z)$
108	105 107	sylibrd	$⊢ (y \in ℋ \land z \in ℋ) \to (span (\{y +_{ℎ} z\}) = span (\{z\}) \to y \in span (\{z\}))$
109	108	adantr	$⊢ ((y \in ℋ \land z \in ℋ) \land y \neq 0_{ℎ}) \to (span (\{y +_{ℎ} z\}) = span (\{z\}) \to y \in span (\{z\}))$
110		spansneleq	$⊢ (z \in ℋ \land y \neq 0_{ℎ}) \to (y \in span (\{z\}) \to span (\{y\}) = span (\{z\}))$
111	110	adantll	$⊢ ((y \in ℋ \land z \in ℋ) \land y \neq 0_{ℎ}) \to (y \in span (\{z\}) \to span (\{y\}) = span (\{z\}))$
112	109 111	syld	$⊢ ((y \in ℋ \land z \in ℋ) \land y \neq 0_{ℎ}) \to (span (\{y +_{ℎ} z\}) = span (\{z\}) \to span (\{y\}) = span (\{z\}))$
113	75 112	sylan9r	$⊢ (((y \in ℋ \land z \in ℋ) \land y \neq 0_{ℎ}) \land B = span (\{z\})) \to (span (\{y +_{ℎ} z\}) = B \to span (\{y\}) = span (\{z\}))$
114	113	necon3d	$⊢ (((y \in ℋ \land z \in ℋ) \land y \neq 0_{ℎ}) \land B = span (\{z\})) \to (span (\{y\}) \neq span (\{z\}) \to span (\{y +_{ℎ} z\}) \neq B)$
115	114	adantlrr	$⊢ (((y \in ℋ \land z \in ℋ) \land (y \neq 0_{ℎ} \land z \neq 0_{ℎ})) \land B = span (\{z\})) \to (span (\{y\}) \neq span (\{z\}) \to span (\{y +_{ℎ} z\}) \neq B)$
116	115	adantrl	$⊢ (((y \in ℋ \land z \in ℋ) \land (y \neq 0_{ℎ} \land z \neq 0_{ℎ})) \land (A = span (\{y\}) \land B = span (\{z\}))) \to (span (\{y\}) \neq span (\{z\}) \to span (\{y +_{ℎ} z\}) \neq B)$
117	116	imp	$⊢ ((((y \in ℋ \land z \in ℋ) \land (y \neq 0_{ℎ} \land z \neq 0_{ℎ})) \land (A = span (\{y\}) \land B = span (\{z\}))) \land span (\{y\}) \neq span (\{z\})) \to span (\{y +_{ℎ} z\}) \neq B$
118		spanpr	$⊢ (y \in ℋ \land z \in ℋ) \to span (\{y +_{ℎ} z\}) \subseteq span (\{y, z\})$
119	118	adantr	$⊢ ((y \in ℋ \land z \in ℋ) \land (A = span (\{y\}) \land B = span (\{z\}))) \to span (\{y +_{ℎ} z\}) \subseteq span (\{y, z\})$
120		oveq12	$⊢ (A = span (\{y\}) \land B = span (\{z\})) \to A \lor_{ℋ} B = span (\{y\}) \lor_{ℋ} span (\{z\})$
121		df-pr	$⊢ \{y, z\} = \{y\} \cup \{z\}$
122	121	fveq2i	$⊢ span (\{y, z\}) = span (\{y\} \cup \{z\})$
123		snssi	$⊢ y \in ℋ \to \{y\} \subseteq ℋ$
124		snssi	$⊢ z \in ℋ \to \{z\} \subseteq ℋ$
125		spanun	$⊢ (\{y\} \subseteq ℋ \land \{z\} \subseteq ℋ) \to span (\{y\} \cup \{z\}) = span (\{y\}) +_{ℋ} span (\{z\})$
126	123 124 125	syl2an	$⊢ (y \in ℋ \land z \in ℋ) \to span (\{y\} \cup \{z\}) = span (\{y\}) +_{ℋ} span (\{z\})$
127	122 126	eqtrid	$⊢ (y \in ℋ \land z \in ℋ) \to span (\{y, z\}) = span (\{y\}) +_{ℋ} span (\{z\})$
128		spansnch	$⊢ y \in ℋ \to span (\{y\}) \in C_{ℋ}$
129		spansnj	$⊢ (span (\{y\}) \in C_{ℋ} \land z \in ℋ) \to span (\{y\}) +_{ℋ} span (\{z\}) = span (\{y\}) \lor_{ℋ} span (\{z\})$
130	128 129	sylan	$⊢ (y \in ℋ \land z \in ℋ) \to span (\{y\}) +_{ℋ} span (\{z\}) = span (\{y\}) \lor_{ℋ} span (\{z\})$
131	127 130	eqtr2d	$⊢ (y \in ℋ \land z \in ℋ) \to span (\{y\}) \lor_{ℋ} span (\{z\}) = span (\{y, z\})$
132	120 131	sylan9eqr	$⊢ ((y \in ℋ \land z \in ℋ) \land (A = span (\{y\}) \land B = span (\{z\}))) \to A \lor_{ℋ} B = span (\{y, z\})$
133	119 132	sseqtrrd	$⊢ ((y \in ℋ \land z \in ℋ) \land (A = span (\{y\}) \land B = span (\{z\}))) \to span (\{y +_{ℎ} z\}) \subseteq A \lor_{ℋ} B$
134	133	adantlr	$⊢ (((y \in ℋ \land z \in ℋ) \land (y \neq 0_{ℎ} \land z \neq 0_{ℎ})) \land (A = span (\{y\}) \land B = span (\{z\}))) \to span (\{y +_{ℎ} z\}) \subseteq A \lor_{ℋ} B$
135	134	adantr	$⊢ ((((y \in ℋ \land z \in ℋ) \land (y \neq 0_{ℎ} \land z \neq 0_{ℎ})) \land (A = span (\{y\}) \land B = span (\{z\}))) \land span (\{y\}) \neq span (\{z\})) \to span (\{y +_{ℎ} z\}) \subseteq A \lor_{ℋ} B$
136		neeq1	$⊢ x = span (\{y +_{ℎ} z\}) \to (x \neq A \leftrightarrow span (\{y +_{ℎ} z\}) \neq A)$
137		neeq1	$⊢ x = span (\{y +_{ℎ} z\}) \to (x \neq B \leftrightarrow span (\{y +_{ℎ} z\}) \neq B)$
138		sseq1	$⊢ x = span (\{y +_{ℎ} z\}) \to (x \subseteq A \lor_{ℋ} B \leftrightarrow span (\{y +_{ℎ} z\}) \subseteq A \lor_{ℋ} B)$
139	136 137 138	3anbi123d	$⊢ x = span (\{y +_{ℎ} z\}) \to ((x \neq A \land x \neq B \land x \subseteq A \lor_{ℋ} B) \leftrightarrow (span (\{y +_{ℎ} z\}) \neq A \land span (\{y +_{ℎ} z\}) \neq B \land span (\{y +_{ℎ} z\}) \subseteq A \lor_{ℋ} B))$
140	139	rspcev	$⊢ (span (\{y +_{ℎ} z\}) \in HAtoms \land (span (\{y +_{ℎ} z\}) \neq A \land span (\{y +_{ℎ} z\}) \neq B \land span (\{y +_{ℎ} z\}) \subseteq A \lor_{ℋ} B)) \to \exists x \in HAtoms (x \neq A \land x \neq B \land x \subseteq A \lor_{ℋ} B)$
141	27 73 117 135 140	syl13anc	$⊢ ((((y \in ℋ \land z \in ℋ) \land (y \neq 0_{ℎ} \land z \neq 0_{ℎ})) \land (A = span (\{y\}) \land B = span (\{z\}))) \land span (\{y\}) \neq span (\{z\})) \to \exists x \in HAtoms (x \neq A \land x \neq B \land x \subseteq A \lor_{ℋ} B)$
142	141	ex	$⊢ (((y \in ℋ \land z \in ℋ) \land (y \neq 0_{ℎ} \land z \neq 0_{ℎ})) \land (A = span (\{y\}) \land B = span (\{z\}))) \to (span (\{y\}) \neq span (\{z\}) \to \exists x \in HAtoms (x \neq A \land x \neq B \land x \subseteq A \lor_{ℋ} B))$
143	8 142	sylbid	$⊢ (((y \in ℋ \land z \in ℋ) \land (y \neq 0_{ℎ} \land z \neq 0_{ℎ})) \land (A = span (\{y\}) \land B = span (\{z\}))) \to (A \neq B \to \exists x \in HAtoms (x \neq A \land x \neq B \land x \subseteq A \lor_{ℋ} B))$
144	143	expl	$⊢ (y \in ℋ \land z \in ℋ) \to (((y \neq 0_{ℎ} \land z \neq 0_{ℎ}) \land (A = span (\{y\}) \land B = span (\{z\}))) \to (A \neq B \to \exists x \in HAtoms (x \neq A \land x \neq B \land x \subseteq A \lor_{ℋ} B)))$
145	4 144	biimtrid	$⊢ (y \in ℋ \land z \in ℋ) \to (((y \neq 0_{ℎ} \land A = span (\{y\})) \land (z \neq 0_{ℎ} \land B = span (\{z\}))) \to (A \neq B \to \exists x \in HAtoms (x \neq A \land x \neq B \land x \subseteq A \lor_{ℋ} B)))$
146	145	rexlimivv	$⊢ \exists y \in ℋ \exists z \in ℋ ((y \neq 0_{ℎ} \land A = span (\{y\})) \land (z \neq 0_{ℎ} \land B = span (\{z\}))) \to (A \neq B \to \exists x \in HAtoms (x \neq A \land x \neq B \land x \subseteq A \lor_{ℋ} B))$
147	3 146	sylbir	$⊢ (\exists y \in ℋ (y \neq 0_{ℎ} \land A = span (\{y\})) \land \exists z \in ℋ (z \neq 0_{ℎ} \land B = span (\{z\}))) \to (A \neq B \to \exists x \in HAtoms (x \neq A \land x \neq B \land x \subseteq A \lor_{ℋ} B))$
148	1 2 147	syl2anb	$⊢ (A \in HAtoms \land B \in HAtoms) \to (A \neq B \to \exists x \in HAtoms (x \neq A \land x \neq B \land x \subseteq A \lor_{ℋ} B))$
149	148	3impia	$⊢ (A \in HAtoms \land B \in HAtoms \land A \neq B) \to \exists x \in HAtoms (x \neq A \land x \neq B \land x \subseteq A \lor_{ℋ} B)$

Metamath Proof Explorer

Theorem superpos

Proof