Theorem sumdmdlem2 10346

Description: Lemma for sumdmd 10347.

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 9484	. . . . . . . . . . . . 13 |- (y e. H~ -> (span` {y}) e. SH)
2		sumdmdi.2	. . . . . . . . . . . . . . 15 |- B e. CH
3	2	chshi 9097	. . . . . . . . . . . . . 14 |- B e. SH
4		shsub2t 9289	. . . . . . . . . . . . . 14 |- (((span` {y}) e. SH /\ B e. SH) -> (span` {y}) (_ (B +H (span` {y})))
5	3, 4	mpan2 696	. . . . . . . . . . . . 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 9486	. . . . . . . . . . . 12 |- (y e. H~ -> y e. (span` {y}))
8	6, 7	sseldd 2068	. . . . . . . . . . 11 |- (y e. H~ -> y e. (B +H (span` {y})))
9	8	ad2antrl 406	. . . . . . . . . 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 10277	. . . . . . . . . . . . . . . . . . . . 21 |- ((y e. H~ /\ y =/= 0h) -> (span` {y}) e. Atoms)
11		df-ne 1587	. . . . . . . . . . . . . . . . . . . . 21 |- (y =/= 0h <-> -. y = 0h)
12	10, 11	sylan2br 453	. . . . . . . . . . . . . . . . . . . 20 |- ((y e. H~ /\ -. y = 0h) -> (span` {y}) e. Atoms)
13		opreq1 3968	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x = (span` {y}) -> (x vH B) = ((span` {y}) vH B))
14	13	ineq1d 2216	. . . . . . . . . . . . . . . . . . . . . 22 |- (x = (span` {y}) -> ((x vH B) i^i (A vH B)) = (((span` {y}) vH B) i^i (A vH B)))
15	13	ineq1d 2216	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x = (span` {y}) -> ((x vH B) i^i A) = (((span` {y}) vH B) i^i A))
16	15	opreq1d 3975	. . . . . . . . . . . . . . . . . . . . . 22 |- (x = (span` {y}) -> (((x vH B) i^i A) vH B) = ((((span` {y}) vH B) i^i A) vH B))
17	14, 16	sseq12d 2090	. . . . . . . . . . . . . . . . . . . . 21 |- (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 1873	. . . . . . . . . . . . . . . . . . . 20 |- ((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	. . . . . . . . . . . . . . . . . . 19 |- ((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 9592	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((B e. CH /\ y e. H~) -> (B +H (span` {y})) = (B vH (span` {y})))
21		chjcomt 9429	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((B e. CH /\ (span` {y}) e. CH) -> (B vH (span` {y})) = ((span` {y}) vH B))
22		spansncht 9483	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (y e. H~ -> (span` {y}) e. CH)
23	21, 22	sylan2 451	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((B e. CH /\ y e. H~) -> (B vH (span` {y})) = ((span` {y}) vH B))
24	20, 23	eqtrd 1507	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((B e. CH /\ y e. H~) -> (B +H (span` {y})) = ((span` {y}) vH B))
25	2, 24	mpan 695	. . . . . . . . . . . . . . . . . . . . . 22 |- (y e. H~ -> (B +H (span` {y})) = ((span` {y}) vH B))
26	25	ineq1d 2216	. . . . . . . . . . . . . . . . . . . . 21 |- (y e. H~ -> ((B +H (span` {y})) i^i (A vH B)) = (((span` {y}) vH B) i^i (A vH B)))
27	25	ineq1d 2216	. . . . . . . . . . . . . . . . . . . . . 22 |- (y e. H~ -> ((B +H (span` {y})) i^i A) = (((span` {y}) vH B) i^i A))
28	27	opreq1d 3975	. . . . . . . . . . . . . . . . . . . . 21 |- (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 2090	. . . . . . . . . . . . . . . . . . . 20 |- (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 389	. . . . . . . . . . . . . . . . . . 19 |- ((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	. . . . . . . . . . . . . . . . . 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) -> ((B +H (span` {y})) i^i (A vH B)) (_ (((B +H (span` {y})) i^i A) vH B)))
32	31	com12 11	. . . . . . . . . . . . . . . . 17 |- (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	exp3a 375	. . . . . . . . . . . . . . . 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))))
34	33	imp 350	. . . . . . . . . . . . . . 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)))
35		ssid 2080	. . . . . . . . . . . . . . . 16 |- B (_ B
36		sneq 2417	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y = 0h -> {y} = {0h})
37	36	fveq2d 3728	. . . . . . . . . . . . . . . . . . . . . 22 |- (y = 0h -> (span` {y}) = (span` {0h}))
38		spansn0 9464	. . . . . . . . . . . . . . . . . . . . . 22 |- (span` {0h}) = 0H
39	37, 38	syl6eq 1523	. . . . . . . . . . . . . . . . . . . . 21 |- (y = 0h -> (span` {y}) = 0H)
40	39	opreq2d 3976	. . . . . . . . . . . . . . . . . . . 20 |- (y = 0h -> (B +H (span` {y})) = (B +H 0H))
41	3	shs0 9372	. . . . . . . . . . . . . . . . . . . 20 |- (B +H 0H) = B
42	40, 41	syl6eq 1523	. . . . . . . . . . . . . . . . . . 19 |- (y = 0h -> (B +H (span` {y})) = B)
43	42	ineq1d 2216	. . . . . . . . . . . . . . . . . 18 |- (y = 0h -> ((B +H (span` {y})) i^i (A vH B)) = (B i^i (A vH B)))
44		inss1 2230	. . . . . . . . . . . . . . . . . . 19 |- (B i^i (A vH B)) (_ B
45		sumdmdi.1	. . . . . . . . . . . . . . . . . . . . 21 |- A e. CH
46	2, 45	chub2 9393	. . . . . . . . . . . . . . . . . . . 20 |- B (_ (A vH B)
47	35, 46	ssini 2233	. . . . . . . . . . . . . . . . . . 19 |- B (_ (B i^i (A vH B))
48	44, 47	eqssi 2078	. . . . . . . . . . . . . . . . . 18 |- (B i^i (A vH B)) = B
49	43, 48	syl6eq 1523	. . . . . . . . . . . . . . . . 17 |- (y = 0h -> ((B +H (span` {y})) i^i (A vH B)) = B)
50	42	ineq1d 2216	. . . . . . . . . . . . . . . . . . 19 |- (y = 0h -> ((B +H (span` {y})) i^i A) = (B i^i A))
51	50	opreq1d 3975	. . . . . . . . . . . . . . . . . 18 |- (y = 0h -> (((B +H (span` {y})) i^i A) vH B) = ((B i^i A) vH B))
52	2, 45	chincl 9383	. . . . . . . . . . . . . . . . . . . 20 |- (B i^i A) e. CH
53	52, 2	chjcom 9391	. . . . . . . . . . . . . . . . . . 19 |- ((B i^i A) vH B) = (B vH (B i^i A))
54	2, 45	chabs1 9441	. . . . . . . . . . . . . . . . . . 19 |- (B vH (B i^i A)) = B
55	53, 54	eqtr 1495	. . . . . . . . . . . . . . . . . 18 |- ((B i^i A) vH B) = B
56	51, 55	syl6eq 1523	. . . . . . . . . . . . . . . . 17 |- (y = 0h -> (((B +H (span` {y})) i^i A) vH B) = B)
57	49, 56	sseq12d 2090	. . . . . . . . . . . . . . . 16 |- (y = 0h -> (((B +H