Theorem dmdbr5at 10349

Description: Dual modular pair property in terms of atoms.

Hypotheses

Ref	Expression
sumdmdi.1	|- A e. CH
sumdmdi.2	|- B e. CH

Assertion

Ref	Expression
dmdbr5at	|- (A MH* B <-> A.x e. Atoms (x (_ (A vH B) -> x (_ (((x vH B) i^i A) vH B)))

Distinct variable groups:   x,A   x,B

Proof of Theorem dmdbr5at

Step	Hyp	Ref	Expression
1		sumdmdi.1	. . . . . . . 8 |- A e. CH
2		sumdmdi.2	. . . . . . . 8 |- B e. CH
3		dmdi4 10234	. . . . . . . 8 |- ((A e. CH /\ B e. CH /\ x e. CH) -> (A MH* B -> ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B)))
4	1, 2, 3	mp3an12 906	. . . . . . 7 |- (x e. CH -> (A MH* B -> ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B)))
5	4	com12 11	. . . . . 6 |- (A MH* B -> (x e. CH -> ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B)))
6		atelch 10271	. . . . . 6 |- (x e. Atoms -> x e. CH)
7	5, 6	syl5 21	. . . . 5 |- (A MH* B -> (x e. Atoms -> ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B)))
8	7	a1dd 42	. . . 4 |- (A MH* B -> (x e. Atoms -> (x (_ (A vH B) -> ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B))))
9	8	r19.21aiv 1713	. . 3 |- (A MH* B -> A.x e. Atoms (x (_ (A vH B) -> ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B)))
10		chjcomt 9429	. . . . . . . . . . . . . . . 16 |- ((B e. CH /\ x e. CH) -> (B vH x) = (x vH B))
11	2, 10	mpan 695	. . . . . . . . . . . . . . 15 |- (x e. CH -> (B vH x) = (x vH B))
12	6, 11	syl 10	. . . . . . . . . . . . . 14 |- (x e. Atoms -> (B vH x) = (x vH B))
13	12	ineq1d 2216	. . . . . . . . . . . . 13 |- (x e. Atoms -> ((B vH x) i^i (B vH A)) = ((x vH B) i^i (B vH A)))
14	1, 2	chjcom 9391	. . . . . . . . . . . . . 14 |- (A vH B) = (B vH A)
15	14	ineq2i 2214	. . . . . . . . . . . . 13 |- ((x vH B) i^i (A vH B)) = ((x vH B) i^i (B vH A))
16	13, 15	syl6eqr 1525	. . . . . . . . . . . 12 |- (x e. Atoms -> ((B vH x) i^i (B vH A)) = ((x vH B) i^i (A vH B)))
17	16	adantr 389	. . . . . . . . . . 11 |- ((x e. Atoms /\ -. x (_ (A vH B)) -> ((B vH x) i^i (B vH A)) = ((x vH B) i^i (A vH B)))
18	2, 1	atabs2 10329	. . . . . . . . . . . . 13 |- (x e. Atoms -> (-. x (_ (B vH A) -> ((B vH x) i^i (B vH A)) = B))
19	18	imp 350	. . . . . . . . . . . 12 |- ((x e. Atoms /\ -. x (_ (B vH A)) -> ((B vH x) i^i (B vH A)) = B)
20	14	sseq2i 2086	. . . . . . . . . . . . 13 |- (x (_ (A vH B) <-> x (_ (B vH A))
21	20	negbii 187	. . . . . . . . . . . 12 |- (-. x (_ (A vH B) <-> -. x (_ (B vH A))
22	19, 21	sylan2b 452	. . . . . . . . . . 11 |- ((x e. Atoms /\ -. x (_ (A vH B)) -> ((B vH x) i^i (B vH A)) = B)
23	17, 22	eqtr3d 1509	. . . . . . . . . 10 |- ((x e. Atoms /\ -. x (_ (A vH B)) -> ((x vH B) i^i (A vH B)) = B)
24		chjclt 9329	. . . . . . . . . . . . . 14 |- ((x e. CH /\ B e. CH) -> (x vH B) e. CH)
25	2, 24	mpan2 696	. . . . . . . . . . . . 13 |- (x e. CH -> (x vH B) e. CH)
26	6, 25	syl 10	. . . . . . . . . . . 12 |- (x e. Atoms -> (x vH B) e. CH)
27		chinclt 9422	. . . . . . . . . . . . 13 |- (((x vH B) e. CH /\ A e. CH) -> ((x vH B) i^i A) e. CH)
28	1, 27	mpan2 696	. . . . . . . . . . . 12 |- ((x vH B) e. CH -> ((x vH B) i^i A) e. CH)
29		chub2t 9431	. . . . . . . . . . . . 13 |- ((B e. CH /\ ((x vH B) i^i A) e. CH) -> B (_ (((x vH B) i^i A) vH B))
30	2, 29	mpan 695	. . . . . . . . . . . 12 |- (((x vH B) i^i A) e. CH -> B (_ (((x vH B) i^i A) vH B))
31	26, 28, 30	3syl 20	. . . . . . . . . . 11 |- (x e. Atoms -> B (_ (((x vH B) i^i A) vH B))
32	31	adantr 389	. . . . . . . . . 10 |- ((x e. Atoms /\ -. x (_ (A vH B)) -> B (_ (((x vH B) i^i A) vH B))
33	23, 32	eqsstrd 2095	. . . . . . . . 9 |- ((x e. Atoms /\ -. x (_ (A vH B)) -> ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B))
34	33	ex 373	. . . . . . . 8 |- (x e. Atoms -> (-. x (_ (A vH B) -> ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B)))
35	34	biantrud 726	. . . . . . 7 |- (x e. Atoms -> ((x (_ (A vH B) -> ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B)) <-> ((x (_ (A vH B) -> ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B)) /\ (-. x (_ (A vH B) -> ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B)))))
36		pm4.83 740	. . . . . . 7 |- (((x (_ (A vH B) -> ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B)) /\ (-. x (_ (A vH B) -> ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B))) <-> ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B))
37	35, 36	syl6bb 536	. . . . . 6 |- (x e. Atoms -> ((x (_ (A vH B) -> ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B)) <-> ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B)))
38	37	ralbiia 1673	. . . . 5 |- (A.x e. Atoms (x (_ (A vH B) -> ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B)) <-> A.x e. Atoms ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B))
39	1, 2	sumdmdlem2 10346	. . . . 5 |- (A.x e. Atoms ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B) -> (A +H B) = (A vH B))
40	38, 39	sylbi 199	. . . 4 |- (A.x e. Atoms (x (_ (A vH B) -> ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B)) -> (A +H B) = (A vH B))
41	1, 2	sumdmd 10347	. . . 4 |- ((A +H B) = (A vH B) <-> A MH* B)
42	40, 41	sylib 198	. . 3 |- (A.x e. Atoms (x (_ (A vH B) -> ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B)) -> A MH* B)
43	9, 42	impbi 157	. 2 |- (A MH* B <-> A.x e. Atoms (x (_ (A vH B) -> ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B)))
44	1, 2	chjcl 9380	. . . . . . . . . . . . 13 |- (A vH B) e. CH
45		chlubt 9432	. . . . . . . . . . . . 13 |- ((x e. CH /\ B e. CH /\ (A vH B) e. CH) -> ((x (_ (A vH B) /\ B (_ (A vH B)) <-> (x vH B) (_ (A vH B)))
46	2, 44, 45	mp3an23 908	. . . . . . . . . . . 12 |- (x e. CH -> ((x (_ (A vH B) /\ B (_ (A vH B)) <-> (x vH B) (_ (A vH B)))
47	2, 1	chub2 9393	. . . . . . . . . . . . 13 |- B (_ (A vH B)
48	47	biantru 724	. . . . . . . . . . . 12 |- (x (_ (A vH B) <-> (x (_ (A vH B) /\ B (_ (A vH B)))
49	46, 48	syl5bb 532	. . . . . . . . . . 11 |- (x e. CH -> (x (_ (A vH B) <-> (x vH B) (_ (A vH B)))
50		ssid 2080	. . . . . . . . . . . . 13 |- (x vH B) (_ (x vH B)
51	50	biantrur 725	. . . . . . . . . . . 12 |- ((x vH B) (_ (A vH B) <-> ((x vH B) (_ (x vH B) /\ (x vH B) (_ (A vH B)))
52		ssin 2232	. . . . . . . . . . . 12 |- (((x vH B) (_ (x vH B) /\ (x vH B) (_ (A vH B)) <-> (x vH B) (_ ((x vH B) i^i (A vH B)))
53	51, 52	bitr 173	. . . . . . . . . . 11 |- ((x vH B) (_ (A vH B) <-> (x vH B) (_ ((x vH B) i^i (A vH B)))
54	49, 53	syl6bb 536	. . . . . . . . . 10 |- (x e. CH -> (x (_ (A vH B) <-> (x vH B) (_ ((x vH B) i^i (A vH B))))
55	54	biimpa 416	. . . . . . . . 9 |- ((x e. CH /\ x (_ (A vH B)) -> (x vH B) (_ ((x vH B) i^i (A vH B)))
56		inss1 2230	. . . . . . . . 9 |- ((x vH B) i^i (A vH B)) (_ (