Theorem sumdmdlem2 10341

Description: Lemma for sumdmd 10342.

Hypotheses

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

Assertion

Ref	Expression
sumdmdlem2	|- (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))

Distinct variable groups:   x,A   x,B

Proof of Theorem sumdmdlem2

Step	Hyp	Ref	Expression
1		spansnsht 9479	. . . . . . . . . . . . 13 |- (y e. H~ -> (span` {y}) e. SH)
2		sumdmdi.2	. . . . . . . . . . . . . . 15 |- B e. CH
3	2	chshi 9092	. . . . . . . . . . . . . 14 |- B e. SH
4		shsub2t 9284	. . . . . . . . . . . . . 14 |- (((span` {y}) e. SH /\ B e. SH) -> (span` {y}) (_ (B +H (span` {y})))
5	3, 4	mpan2 698	. . . . . . . . . . . . 13 |- ((span` {y}) e. SH -> (span` {y}) (_ (B +H (span` {y})))
6	1, 5	syl 10	. . . . . . . . . . . 12 |- (y e. H~ -> (span` {y}) (_ (B +H (span` {y})))
7		spansnid 9481	. . . . . . . . . . . 12 |- (y e. H~ -> y e. (span` {y}))
8	6, 7	sseldd 2071	. . . . . . . . . . 11 |- (y e. H~ -> y e. (B +H (span` {y})))
9	8	ad2antrl 408	. . . . . . . . . 10 |- ((A.x e. Atoms ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B) /\ (y e. H~ /\ -. y e. (A +H B))) -> y e. (B +H (span` {y})))
10		spansnat 10272	. . . . . . . . . . . . . . . . . . . 20 |- ((y e. H~ /\ y =/= 0h) -> (span` {y}) e. Atoms)
11		df-ne 1590	. . . . . . . . . . . . . . . . . . . 20 |- (y =/= 0h <-> -. y = 0h)
12	10, 11	sylan2br 455	. . . . . . . . . . . . . . . . . . 19 |- ((y e. H~ /\ -. y = 0h) -> (span` {y}) e. Atoms)
13		opreq1 3974	. . . . . . . . . . . . . . . . . . . . . 22 |- (x = (span` {y}) -> (x vH B) = ((span` {y}) vH B))
14	13	ineq1d 2219	. . . . . . . . . . . . . . . . . . . . 21 |- (x = (span` {y}) -> ((x vH B) i^i (A vH B)) = (((span` {y}) vH B) i^i (A vH B)))
15	13	ineq1d 2219	. . . . . . . . . . . . . . . . . . . . . 22 |- (x = (span` {y}) -> ((x vH B) i^i A) = (((span` {y}) vH B) i^i A))
16	15	opreq1d 3981	. . . . . . . . . . . . . . . . . . . . 21 |- (x = (span` {y}) -> (((x vH B) i^i A) vH B) = ((((span` {y}) vH B) i^i A) vH B))
17	14, 16	sseq12d 2093	. . . . . . . . . . . . . . . . . . . 20 |- (x = (span` {y}) -> (((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B) <-> (((span` {y}) vH B) i^i (A vH B)) (_ ((((span` {y}) vH B) i^i A) vH B)))
18	17	rcla4v 1876	. . . . . . . . . . . . . . . . . . 19 |- ((span` {y}) e. Atoms -> (A.x e. Atoms ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B) -> (((span` {y}) vH B) i^i (A vH B)) (_ ((((span` {y}) vH B) i^i A) vH B)))
19	12, 18	syl 10	. . . . . . . . . . . . . . . . . 18 |- ((y e. H~ /\ -. y = 0h) -> (A.x e. Atoms ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B) -> (((span` {y}) vH B) i^i (A vH B)) (_ ((((span` {y}) vH B) i^i A) vH B)))
20		spansnjt 9587	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((B e. CH /\ y e. H~) -> (B +H (span` {y})) = (B vH (span` {y})))
21		chjcomt 9424	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((B e. CH /\ (span` {y}) e. CH) -> (B vH (span` {y})) = ((span` {y}) vH B))
22		spansncht 9478	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y e. H~ -> (span` {y}) e. CH)
23	21, 22	sylan2 453	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((B e. CH /\ y e. H~) -> (B vH (span` {y})) = ((span` {y}) vH B))
24	20, 23	eqtrd 1510	. . . . . . . . . . . . . . . . . . . . . 22 |- ((B e. CH /\ y e. H~) -> (B +H (span` {y})) = ((span` {y}) vH B))
25	2, 24	mpan 697	. . . . . . . . . . . . . . . . . . . . 21 |- (y e. H~ -> (B +H (span` {y})) = ((span` {y}) vH B))
26	25	ineq1d 2219	. . . . . . . . . . . . . . . . . . . 20 |- (y e. H~ -> ((B +H (span` {y})) i^i (A vH B)) = (((span` {y}) vH B) i^i (A vH B)))
27	25	ineq1d 2219	. . . . . . . . . . . . . . . . . . . . 21 |- (y e. H~ -> ((B +H (span` {y})) i^i A) = (((span` {y}) vH B) i^i A))
28	27	opreq1d 3981	. . . . . . . . . . . . . . . . . . . 20 |- (y e. H~ -> (((B +H (span` {y})) i^i A) vH B) = ((((span` {y}) vH B) i^i A) vH B))
29	26, 28	sseq12d 2093	. . . . . . . . . . . . . . . . . . 19 |- (y e. H~ -> (((B +H (span` {y})) i^i (A vH B)) (_ (((B +H (span` {y})) i^i A) vH B) <-> (((span` {y}) vH B) i^i (A vH B)) (_ ((((span` {y}) vH B) i^i A) vH B)))
30	29	adantr 391	. . . . . . . . . . . . . . . . . 18 |- ((y e. H~ /\ -. y = 0h) -> (((B +H (span` {y})) i^i (A vH B)) (_ (((B +H (span` {y})) i^i A) vH B) <-> (((span` {y}) vH B) i^i (A vH B)) (_ ((((span` {y}) vH B) i^i A) vH B)))
31	19, 30	sylibrd 204	. . . . . . . . . . . . . . . . 17 |- ((y e. H~ /\ -. y = 0h) -> (A.x e. Atoms ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B) -> ((B +H (span` {y})) i^i (A vH B)) (_ (((B +H (span` {y})) i^i A) vH B)))
32	31	com12 11	. . . . . . . . . . . . . . . 16 |- (A.x e. Atoms ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B) -> ((y e. H~ /\ -. y = 0h) -> ((B +H (span` {y})) i^i (A vH B)) (_ (((B +H (span` {y})) i^i A) vH B)))
33	32	expdimp 377	. . . . . . . . . . . . . . 15 |- ((A.x e. Atoms ((x vH B) i^i (A vH B)) (_ (((x vH B) i^i A) vH B) /\ y e. H~) -> (-. y = 0h -> ((B +H (span` {y})) i^i (A vH B)) (_ (((B +H (span` {y})) i^i A) vH B)))
34		ssid 2083	. . . . . . . . . . . . . . . 16 |- B (_ B
35		sneq 2421	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y = 0h -> {y} = {0h})
36	35	fveq2d 3734	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = 0h -> (span` {y}) = (span` {0h}))
37		spansn0 9459	. . . . . . . . . . . . . . . . . . . . . 22 |- (span` {0h}) = 0H
38	36, 37	syl6eq 1526	. . . . . . . . . . . . . . . . . . . . 21 |- (y = 0h -> (span` {y}) = 0H)
39	38	opreq2d 3982	. . . . . . . . . . . . . . . . . . . 20 |- (y = 0h -> (B +H (span` {y})) = (B +H 0H))
40	3	shs0 9367	. . . . . . . . . . . . . . . . . . . 20 |- (B +H 0H) = B
41	39, 40	syl6eq 1526	. . . . . . . . . . . . . . . . . . 19 |- (y = 0h -> (B +H (span` {y})) = B)
42	41	ineq1d 2219	. . . . . . . . . . . . . . . . . 18 |- (y = 0h -> ((B +H (span` {y})) i^i (A vH B)) = (B i^i (A vH B)))
43		inss1 2233	. . . . . . . . . . . . . . . . . . 19 |- (B i^i (A vH B)) (_ B
44		sumdmdi.1	. . . . . . . . . . . . . . . . . . . . 21 |- A e. CH
45	2, 44	chub2 9388	. . . . . . . . . . . . . . . . . . . 20 |- B (_ (A vH B)
46	34, 45	ssini 2236	. . . . . . . . . . . . . . . . . . 19 |- B (_ (B i^i (A vH B))
47	43, 46	eqssi 2081	. . . . . . . . . . . . . . . . . 18 |- (B i^i (A vH B)) = B
48	42, 47	syl6eq 1526	. . . . . . . . . . . . . . . . 17 |- (y = 0h -> ((B +H (span` {y})) i^i (A vH B)) = B)
49	41	ineq1d 2219	. . . . . . . . . . . . . . . . . . 19 |- (y = 0h -> ((B +H (span` {y})) i^i A) = (B i^i A))
50	49	opreq1d 3981	. . . . . . . . . . . . . . . . . 18 |- (y = 0h -> (((B +H (span` {y})) i^i A) vH B) = ((B i^i A) vH B))
51	2, 44	chincl 9378	. . . . . . . . . . . . . . . . . . . 20 |- (B i^i A) e. CH
52	51, 2	chjcom 9386	. . . . . . . . . . . . . . . . . . 19 |- ((B i^i A) vH B) = (B vH (B i^i A))
53	2, 44	chabs1 9436	. . . . . . . . . . . . . . . . . . 19 |- (B vH (B i^i A)) = B
54	52, 53	eqtr 1498	. . . . . . . . . . . . . . . . . 18 |- ((B i^i A) vH B) = B
55	50, 54	syl6eq 1526	. . . . . . . . . . . . . . . . 17 |- (y = 0h -> (((B +H (span` {y})) i^i A) vH B) = B)
56	48, 55	sseq12d 2093	. . . . . . . . . . . . . . . 16 |- (y = 0h -> (((B +H (span` {y})) i^i (A vH B)) (_ (((B +H (span` {y})) i^i A) vH B) <-> B (_ B))
57	34, 56	mpbiri 194	. . . . . . . . . . . . . . 15 |- (y = 0h -> ((B +H (span` {y})) i^i (A vH B)) (_ (((B +H (span` {y})) i^i A) vH B))
58