sumdmdii

Description: If the subspace sum of two Hilbert lattice elements is closed, then the elements are a dual modular pair. Remark in MaedaMaeda p. 139. (Contributed by NM, 12-Jul-2004) (New usage is discouraged.)

	Ref	Expression
Hypotheses	sumdmdi.1	$⊢ A \in C_{ℋ}$
	sumdmdi.2	$⊢ B \in C_{ℋ}$
Assertion	sumdmdii	$⊢ A +_{ℋ} B = A \lor_{ℋ} B \to A 𝑀_{ℋ}^{*} B$

Proof

Step	Hyp	Ref	Expression
1		sumdmdi.1	$⊢ A \in C_{ℋ}$
2		sumdmdi.2	$⊢ B \in C_{ℋ}$
3		ineq2	$⊢ A +_{ℋ} B = A \lor_{ℋ} B \to x \cap (A +_{ℋ} B) = x \cap (A \lor_{ℋ} B)$
4	3	adantr	$⊢ (A +_{ℋ} B = A \lor_{ℋ} B \land (x \in C_{ℋ} \land B \subseteq x)) \to x \cap (A +_{ℋ} B) = x \cap (A \lor_{ℋ} B)$
5		elin	$⊢ y \in (x \cap (A +_{ℋ} B)) \leftrightarrow (y \in x \land y \in (A +_{ℋ} B))$
6	1 2	chseli	$⊢ y \in (A +_{ℋ} B) \leftrightarrow \exists z \in A \exists w \in B y = z +_{ℎ} w$
7		ssel2	$⊢ (B \subseteq x \land w \in B) \to w \in x$
8		chsh	$⊢ x \in C_{ℋ} \to x \in S_{ℋ}$
9		shsubcl	$⊢ (x \in S_{ℋ} \land y \in x \land w \in x) \to y -_{ℎ} w \in x$
10	9	3exp	$⊢ x \in S_{ℋ} \to (y \in x \to (w \in x \to y -_{ℎ} w \in x))$
11	8 10	syl	$⊢ x \in C_{ℋ} \to (y \in x \to (w \in x \to y -_{ℎ} w \in x))$
12	7 11	syl7	$⊢ x \in C_{ℋ} \to (y \in x \to ((B \subseteq x \land w \in B) \to y -_{ℎ} w \in x))$
13	12	exp4a	$⊢ x \in C_{ℋ} \to (y \in x \to (B \subseteq x \to (w \in B \to y -_{ℎ} w \in x)))$
14	13	com23	$⊢ x \in C_{ℋ} \to (B \subseteq x \to (y \in x \to (w \in B \to y -_{ℎ} w \in x)))$
15	14	imp41	$⊢ (((x \in C_{ℋ} \land B \subseteq x) \land y \in x) \land w \in B) \to y -_{ℎ} w \in x$
16	15	adantlr	$⊢ ((((x \in C_{ℋ} \land B \subseteq x) \land y \in x) \land z \in A) \land w \in B) \to y -_{ℎ} w \in x$
17	16	adantr	$⊢ (((((x \in C_{ℋ} \land B \subseteq x) \land y \in x) \land z \in A) \land w \in B) \land y = z +_{ℎ} w) \to y -_{ℎ} w \in x$
18		chel	$⊢ (x \in C_{ℋ} \land y \in x) \to y \in ℋ$
19	18	adantlr	$⊢ ((x \in C_{ℋ} \land B \subseteq x) \land y \in x) \to y \in ℋ$
20	1	cheli	$⊢ z \in A \to z \in ℋ$
21	2	cheli	$⊢ w \in B \to w \in ℋ$
22		hvsubadd	$⊢ (y \in ℋ \land w \in ℋ \land z \in ℋ) \to (y -_{ℎ} w = z \leftrightarrow w +_{ℎ} z = y)$
23		ax-hvcom	$⊢ (w \in ℋ \land z \in ℋ) \to w +_{ℎ} z = z +_{ℎ} w$
24	23	eqeq1d	$⊢ (w \in ℋ \land z \in ℋ) \to (w +_{ℎ} z = y \leftrightarrow z +_{ℎ} w = y)$
25		eqcom	$⊢ z +_{ℎ} w = y \leftrightarrow y = z +_{ℎ} w$
26	24 25	bitrdi	$⊢ (w \in ℋ \land z \in ℋ) \to (w +_{ℎ} z = y \leftrightarrow y = z +_{ℎ} w)$
27	26	3adant1	$⊢ (y \in ℋ \land w \in ℋ \land z \in ℋ) \to (w +_{ℎ} z = y \leftrightarrow y = z +_{ℎ} w)$
28	22 27	bitrd	$⊢ (y \in ℋ \land w \in ℋ \land z \in ℋ) \to (y -_{ℎ} w = z \leftrightarrow y = z +_{ℎ} w)$
29	28	3com23	$⊢ (y \in ℋ \land z \in ℋ \land w \in ℋ) \to (y -_{ℎ} w = z \leftrightarrow y = z +_{ℎ} w)$
30	19 20 21 29	syl3an	$⊢ (((x \in C_{ℋ} \land B \subseteq x) \land y \in x) \land z \in A \land w \in B) \to (y -_{ℎ} w = z \leftrightarrow y = z +_{ℎ} w)$
31	30	3expa	$⊢ ((((x \in C_{ℋ} \land B \subseteq x) \land y \in x) \land z \in A) \land w \in B) \to (y -_{ℎ} w = z \leftrightarrow y = z +_{ℎ} w)$
32		eleq1	$⊢ y -_{ℎ} w = z \to (y -_{ℎ} w \in x \leftrightarrow z \in x)$
33	31 32	biimtrrdi	$⊢ ((((x \in C_{ℋ} \land B \subseteq x) \land y \in x) \land z \in A) \land w \in B) \to (y = z +_{ℎ} w \to (y -_{ℎ} w \in x \leftrightarrow z \in x))$
34	33	imp	$⊢ (((((x \in C_{ℋ} \land B \subseteq x) \land y \in x) \land z \in A) \land w \in B) \land y = z +_{ℎ} w) \to (y -_{ℎ} w \in x \leftrightarrow z \in x)$
35	17 34	mpbid	$⊢ (((((x \in C_{ℋ} \land B \subseteq x) \land y \in x) \land z \in A) \land w \in B) \land y = z +_{ℎ} w) \to z \in x$
36		simpr	$⊢ (((((x \in C_{ℋ} \land B \subseteq x) \land y \in x) \land z \in A) \land w \in B) \land y = z +_{ℎ} w) \to y = z +_{ℎ} w$
37	35 36	jca	$⊢ (((((x \in C_{ℋ} \land B \subseteq x) \land y \in x) \land z \in A) \land w \in B) \land y = z +_{ℎ} w) \to (z \in x \land y = z +_{ℎ} w)$
38	37	exp31	$⊢ (((x \in C_{ℋ} \land B \subseteq x) \land y \in x) \land z \in A) \to (w \in B \to (y = z +_{ℎ} w \to (z \in x \land y = z +_{ℎ} w)))$
39	38	reximdvai	$⊢ (((x \in C_{ℋ} \land B \subseteq x) \land y \in x) \land z \in A) \to (\exists w \in B y = z +_{ℎ} w \to \exists w \in B (z \in x \land y = z +_{ℎ} w))$
40		r19.42v	$⊢ \exists w \in B (z \in x \land y = z +_{ℎ} w) \leftrightarrow (z \in x \land \exists w \in B y = z +_{ℎ} w)$
41	39 40	imbitrdi	$⊢ (((x \in C_{ℋ} \land B \subseteq x) \land y \in x) \land z \in A) \to (\exists w \in B y = z +_{ℎ} w \to (z \in x \land \exists w \in B y = z +_{ℎ} w))$
42	41	reximdva	$⊢ ((x \in C_{ℋ} \land B \subseteq x) \land y \in x) \to (\exists z \in A \exists w \in B y = z +_{ℎ} w \to \exists z \in A (z \in x \land \exists w \in B y = z +_{ℎ} w))$
43		elin	$⊢ z \in (x \cap A) \leftrightarrow (z \in x \land z \in A)$
44		ancom	$⊢ (z \in x \land z \in A) \leftrightarrow (z \in A \land z \in x)$
45	43 44	bitri	$⊢ z \in (x \cap A) \leftrightarrow (z \in A \land z \in x)$
46	45	anbi1i	$⊢ (z \in (x \cap A) \land \exists w \in B y = z +_{ℎ} w) \leftrightarrow ((z \in A \land z \in x) \land \exists w \in B y = z +_{ℎ} w)$
47		anass	$⊢ ((z \in A \land z \in x) \land \exists w \in B y = z +_{ℎ} w) \leftrightarrow (z \in A \land (z \in x \land \exists w \in B y = z +_{ℎ} w))$
48	46 47	bitri	$⊢ (z \in (x \cap A) \land \exists w \in B y = z +_{ℎ} w) \leftrightarrow (z \in A \land (z \in x \land \exists w \in B y = z +_{ℎ} w))$
49	48	rexbii2	$⊢ \exists z \in (x \cap A) \exists w \in B y = z +_{ℎ} w \leftrightarrow \exists z \in A (z \in x \land \exists w \in B y = z +_{ℎ} w)$
50	42 49	imbitrrdi	$⊢ ((x \in C_{ℋ} \land B \subseteq x) \land y \in x) \to (\exists z \in A \exists w \in B y = z +_{ℎ} w \to \exists z \in (x \cap A) \exists w \in B y = z +_{ℎ} w)$
51	1	chshii	$⊢ A \in S_{ℋ}$
52		shincl	$⊢ (x \in S_{ℋ} \land A \in S_{ℋ}) \to x \cap A \in S_{ℋ}$
53	8 51 52	sylancl	$⊢ x \in C_{ℋ} \to x \cap A \in S_{ℋ}$
54	53	ad2antrr	$⊢ ((x \in C_{ℋ} \land B \subseteq x) \land y \in x) \to x \cap A \in S_{ℋ}$
55	2	chshii	$⊢ B \in S_{ℋ}$
56		shsel	$⊢ (x \cap A \in S_{ℋ} \land B \in S_{ℋ}) \to (y \in ((x \cap A) +_{ℋ} B) \leftrightarrow \exists z \in (x \cap A) \exists w \in B y = z +_{ℎ} w)$
57	54 55 56	sylancl	$⊢ ((x \in C_{ℋ} \land B \subseteq x) \land y \in x) \to (y \in ((x \cap A) +_{ℋ} B) \leftrightarrow \exists z \in (x \cap A) \exists w \in B y = z +_{ℎ} w)$
58	50 57	sylibrd	$⊢ ((x \in C_{ℋ} \land B \subseteq x) \land y \in x) \to (\exists z \in A \exists w \in B y = z +_{ℎ} w \to y \in ((x \cap A) +_{ℋ} B))$
59	6 58	biimtrid	$⊢ ((x \in C_{ℋ} \land B \subseteq x) \land y \in x) \to (y \in (A +_{ℋ} B) \to y \in ((x \cap A) +_{ℋ} B))$
60	59	expimpd	$⊢ (x \in C_{ℋ} \land B \subseteq x) \to ((y \in x \land y \in (A +_{ℋ} B)) \to y \in ((x \cap A) +_{ℋ} B))$
61	5 60	biimtrid	$⊢ (x \in C_{ℋ} \land B \subseteq x) \to (y \in (x \cap (A +_{ℋ} B)) \to y \in ((x \cap A) +_{ℋ} B))$
62	61	ssrdv	$⊢ (x \in C_{ℋ} \land B \subseteq x) \to x \cap (A +_{ℋ} B) \subseteq (x \cap A) +_{ℋ} B$
63	62	adantl	$⊢ (A +_{ℋ} B = A \lor_{ℋ} B \land (x \in C_{ℋ} \land B \subseteq x)) \to x \cap (A +_{ℋ} B) \subseteq (x \cap A) +_{ℋ} B$
64	4 63	eqsstrrd	$⊢ (A +_{ℋ} B = A \lor_{ℋ} B \land (x \in C_{ℋ} \land B \subseteq x)) \to x \cap (A \lor_{ℋ} B) \subseteq (x \cap A) +_{ℋ} B$
65		chincl	$⊢ (x \in C_{ℋ} \land A \in C_{ℋ}) \to x \cap A \in C_{ℋ}$
66	1 65	mpan2	$⊢ x \in C_{ℋ} \to x \cap A \in C_{ℋ}$
67		chslej	$⊢ (x \cap A \in C_{ℋ} \land B \in C_{ℋ}) \to (x \cap A) +_{ℋ} B \subseteq (x \cap A) \lor_{ℋ} B$
68	66 2 67	sylancl	$⊢ x \in C_{ℋ} \to (x \cap A) +_{ℋ} B \subseteq (x \cap A) \lor_{ℋ} B$
69	68	ad2antrl	$⊢ (A +_{ℋ} B = A \lor_{ℋ} B \land (x \in C_{ℋ} \land B \subseteq x)) \to (x \cap A) +_{ℋ} B \subseteq (x \cap A) \lor_{ℋ} B$
70	64 69	sstrd	$⊢ (A +_{ℋ} B = A \lor_{ℋ} B \land (x \in C_{ℋ} \land B \subseteq x)) \to x \cap (A \lor_{ℋ} B) \subseteq (x \cap A) \lor_{ℋ} B$
71	70	exp32	$⊢ A +_{ℋ} B = A \lor_{ℋ} B \to (x \in C_{ℋ} \to (B \subseteq x \to x \cap (A \lor_{ℋ} B) \subseteq (x \cap A) \lor_{ℋ} B))$
72	71	ralrimiv	$⊢ A +_{ℋ} B = A \lor_{ℋ} B \to \forall x \in C_{ℋ} (B \subseteq x \to x \cap (A \lor_{ℋ} B) \subseteq (x \cap A) \lor_{ℋ} B)$
73		dmdbr2	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A 𝑀_{ℋ}^{*} B \leftrightarrow \forall x \in C_{ℋ} (B \subseteq x \to x \cap (A \lor_{ℋ} B) \subseteq (x \cap A) \lor_{ℋ} B))$
74	1 2 73	mp2an	$⊢ A 𝑀_{ℋ}^{*} B \leftrightarrow \forall x \in C_{ℋ} (B \subseteq x \to x \cap (A \lor_{ℋ} B) \subseteq (x \cap A) \lor_{ℋ} B)$
75	72 74	sylibr	$⊢ A +_{ℋ} B = A \lor_{ℋ} B \to A 𝑀_{ℋ}^{*} B$

Metamath Proof Explorer

Theorem sumdmdii

Proof