Theorem irredlem1 10312

Description: Lemma for irred 10316.

Hypothesis

Ref	Expression
irred.1	|- A e. CH

Assertion

Ref	Expression
irredlem1	|- (((p e. Atoms /\ (q e. CH /\ q (_ (_|_` A))) /\ ((r e. Atoms /\ r (_ A) /\ r (_ (p vH q))) -> (p i^i (_|_` r)) = 0H)

Distinct variable group:   q,p,r,A

Proof of Theorem irredlem1

Step	Hyp	Ref	Expression
1		sstr2 2074	. . . . . 6 |- (q (_ (_|_` A) -> ((_|_` A) (_ (_|_` r) -> q (_ (_|_` r)))
2		irred.1	. . . . . . . . 9 |- A e. CH
3		chsscon3t 9418	. . . . . . . . 9 |- ((r e. CH /\ A e. CH) -> (r (_ A <-> (_|_` A) (_ (_|_` r)))
4	2, 3	mpan2 698	. . . . . . . 8 |- (r e. CH -> (r (_ A <-> (_|_` A) (_ (_|_` r)))
5	4	biimpa 418	. . . . . . 7 |- ((r e. CH /\ r (_ A) -> (_|_` A) (_ (_|_` r))
6		atelch 10266	. . . . . . 7 |- (r e. Atoms -> r e. CH)
7	5, 6	sylan 450	. . . . . 6 |- ((r e. Atoms /\ r (_ A) -> (_|_` A) (_ (_|_` r))
8	1, 7	syl5 21	. . . . 5 |- (q (_ (_|_` A) -> ((r e. Atoms /\ r (_ A) -> q (_ (_|_` r)))
9		atn0 10267	. . . . . . . . . . . . . 14 |- (r e. Atoms -> r =/= 0H)
10		df-ne 1590	. . . . . . . . . . . . . 14 |- (r =/= 0H <-> -. r = 0H)
11	9, 10	sylib 198	. . . . . . . . . . . . 13 |- (r e. Atoms -> -. r = 0H)
12	11	adantr 391	. . . . . . . . . . . 12 |- ((r e. Atoms /\ q (_ (_|_` r)) -> -. r = 0H)
13	12	ad2antrr 406	. . . . . . . . . . 11 |- ((((r e. Atoms /\ q (_ (_|_` r)) /\ (p e. CH /\ q e. CH)) /\ r (_ (p vH q)) -> -. r = 0H)
14		simplr 415	. . . . . . . . . . . . . . 15 |- (((((r e. Atoms /\ q (_ (_|_` r)) /\ (p e. CH /\ q e. CH)) /\ r (_ (p vH q)) /\ p (_ (_|_` r)) -> r (_ (p vH q))
15		chlej1t 9428	. . . . . . . . . . . . . . . . . . . 20 |- (((p e. CH /\ (_|_` r) e. CH /\ q e. CH) /\ p (_ (_|_` r)) -> (p vH q) (_ ((_|_` r) vH q))
16	15	3exp1 851	. . . . . . . . . . . . . . . . . . 19 |- (p e. CH -> ((_|_` r) e. CH -> (q e. CH -> (p (_ (_|_` r) -> (p vH q) (_ ((_|_` r) vH q)))))
17		chocclt 9179	. . . . . . . . . . . . . . . . . . . 20 |- (r e. CH -> (_|_` r) e. CH)
18	6, 17	syl 10	. . . . . . . . . . . . . . . . . . 19 |- (r e. Atoms -> (_|_` r) e. CH)
19	16, 18	syl5com 52	. . . . . . . . . . . . . . . . . 18 |- (r e. Atoms -> (p e. CH -> (q e. CH -> (p (_ (_|_` r) -> (p vH q) (_ ((_|_` r) vH q)))))
20	19	imp42 369	. . . . . . . . . . . . . . . . 17 |- (((r e. Atoms /\ (p e. CH /\ q e. CH)) /\ p (_ (_|_` r)) -> (p vH q) (_ ((_|_` r) vH q))
21	20	adantllr 399	. . . . . . . . . . . . . . . 16 |- ((((r e. Atoms /\ q (_ (_|_` r)) /\ (p e. CH /\ q e. CH)) /\ p (_ (_|_` r)) -> (p vH q) (_ ((_|_` r) vH q))
22	21	adantlr 395	. . . . . . . . . . . . . . 15 |- (((((r e. Atoms /\ q (_ (_|_` r)) /\ (p e. CH /\ q e. CH)) /\ r (_ (p vH q)) /\ p (_ (_|_` r)) -> (p vH q) (_ ((_|_` r) vH q))
23	14, 22	sstrd 2077	. . . . . . . . . . . . . 14 |- (((((r e. Atoms /\ q (_ (_|_` r)) /\ (p e. CH /\ q e. CH)) /\ r (_ (p vH q)) /\ p (_ (_|_` r)) -> r (_ ((_|_` r) vH q))
24		chlejb2t 9431	. . . . . . . . . . . . . . . . . . . 20 |- ((q e. CH /\ (_|_` r) e. CH) -> (q (_ (_|_` r) <-> ((_|_` r) vH q) = (_|_` r)))
25	24	ancoms 438	. . . . . . . . . . . . . . . . . . 19 |- (((_|_` r) e. CH /\ q e. CH) -> (q (_ (_|_` r) <-> ((_|_` r) vH q) = (_|_` r)))
26	25	biimpa 418	. . . . . . . . . . . . . . . . . 18 |- ((((_|_` r) e. CH /\ q e. CH) /\ q (_ (_|_` r)) -> ((_|_` r) vH q) = (_|_` r))
27	26, 18	sylanl1 462	. . . . . . . . . . . . . . . . 17 |- (((r e. Atoms /\ q e. CH) /\ q (_ (_|_` r)) -> ((_|_` r) vH q) = (_|_` r))
28	27	an1rs 491	. . . . . . . . . . . . . . . 16 |- (((r e. Atoms /\ q (_ (_|_` r)) /\ q e. CH) -> ((_|_` r) vH q) = (_|_` r))
29	28	adantrl 396	. . . . . . . . . . . . . . 15 |- (((r e. Atoms /\ q (_ (_|_` r)) /\ (p e. CH /\ q e. CH)) -> ((_|_` r) vH q) = (_|_` r))
30	29	ad2antrr 406	. . . . . . . . . . . . . 14 |- (((((r e. Atoms /\ q (_ (_|_` r)) /\ (p e. CH /\ q e. CH)) /\ r (_ (p vH q)) /\ p (_ (_|_` r)) -> ((_|_` r) vH q) = (_|_` r))
31	23, 30	sseqtrd 2100	. . . . . . . . . . . . 13 |- (((((r e. Atoms /\ q (_ (_|_` r)) /\ (p e. CH /\ q e. CH)) /\ r (_ (p vH q)) /\ p (_ (_|_` r)) -> r (_ (_|_` r))
32	31	ex 373	. . . . . . . . . . . 12 |- ((((r e. Atoms /\ q (_ (_|_` r)) /\ (p e. CH /\ q e. CH)) /\ r (_ (p vH q)) -> (p (_ (_|_` r) -> r (_ (_|_` r)))
33		chssoct 9414	. . . . . . . . . . . . . . . 16 |- (r e. CH -> (r (_ (_|_` r) <-> r = 0H))
34	33	biimpd 153	. . . . . . . . . . . . . . 15 |- (r e. CH -> (r (_ (_|_` r) -> r = 0H))
35	6, 34	syl 10	. . . . . . . . . . . . . 14 |- (r e. Atoms -> (r (_ (_|_` r) -> r = 0H))
36	35	adantr 391	. . . . . . . . . . . . 13 |- ((r e. Atoms /\ q (_ (_|_` r)) -> (r (_ (_|_` r) -> r = 0H))
37	36	ad2antrr 406	. . . . . . . . . . . 12 |- ((((r e. Atoms /\ q (_ (_|_` r)) /\ (p e. CH /\ q e. CH)) /\ r (_ (p vH q)) -> (r (_ (_|_` r) -> r = 0H))
38	32, 37	syld 27	. . . . . . . . . . 11 |- ((((r e. Atoms /\ q (_ (_|_` r)) /\ (p e. CH /\ q e. CH)) /\ r (_ (p vH q)) -> (p (_ (_|_` r) -> r = 0H))
39	13, 38	mtod 108	. . . . . . . . . 10 |- ((((r e. Atoms /\ q (_ (_|_` r)) /\ (p e. CH /\ q e. CH)) /\ r (_ (p vH q)) -> -. p (_ (_|_` r))
40	39	ex 373	. . . . . . . . 9 |- (((r e. Atoms /\ q (_ (_|_` r)) /\ (p e. CH /\ q e. CH)) -> (r (_ (p vH q) -> -. p (_ (_|_` r)))
41		atelch 10266	. . . . . . . . 9 |- (p e. Atoms -> p e. CH)
42	40, 41	sylanr1 464	. . . . . . . 8 |- (((r e. Atoms /\ q (_ (_|_` r)) /\ (p e. Atoms /\ q e. CH)) -> (r (_ (p vH q) -> -. p (_ (_|_` r)))
43		atnssm0 10298	. . . . . . . . . . 11 |- (((_|_` r) e. CH /\ p e. Atoms) -> (-. p (_ (_|_` r) <-> ((_|_` r) i^i p) = 0H))
44		incom 2211	. . . . . . . . . . . 12 |- ((_|_` r) i^i p) = (p i^i (_|_` r))
45	44	eqeq1i 1485	. . . . . . . . . . 11 |- (((_|_` r) i^i p) = 0H <-> (p i^i (_|_` r)) = 0H)
46	43, 45	syl6bb 538	. . . . . . . . . 10 |- (((_|_` r) e. CH /\ p e. Atoms) -> (-. p (_ (_|_` r) <-> (p i^i (_|_` r)) = 0H))
47	46, 18	sylan 450	. . . . . . . . 9 |- ((r e. Atoms /\ p e. Atoms) -> (-. p (_ (_|_` r) <-> (p i^i (_|_` r)) = 0H))
48	47	ad2ant2r 411	. . . . . . . 8 |- (((r e. Atoms /\ q (_ (_|_` r)) /\ (p e. Atoms /\ q e. CH)) -> (-. p (_ (_|_` r) <-> (p i^i (_|_` r)) = 0H))
49	42, 48	sylibd 202	. . . . . . 7 |- (((r e. Atoms /\ q (_ (_|_` r)) /\ (p e. Atoms /\ q e. CH)) -> (r (_ (p vH q) -> (p i^i (_|_` r)) = 0H))
50	49	exp43 386	. . . . . 6 |- (r e. Atoms -> (q (_ (_|_` r) -> (p e. Atoms -> (q e. CH -> (r (_ (p vH q) -> (p i^i (_|_` r)) = 0H)))))
51	50	adantr 391	. . . . 5 |- ((r e. Atoms /\ r (_ A) -> (q (_ (_|_` r) -> (p e. Atoms -> (q e. CH -> (r (_ (p vH q) -> (p i^i (_|_` r)) = 0H)))))
52	8, 51	sylcom 51	. . . 4 |- (q (_ (_|_` A) -> ((r e. Atoms /\ r (_ A) -> (p e. Atoms -> (q e. CH -> (r (_ (p vH q) -> (p i^i (_|_` r)) = 0H)))))
53	52	com4t 40	. . 3 |- (p e. Atoms -> (q e. CH -> (q (_ (_|_` A) -> ((r e. Atoms /\ r (_ A) -> (r (_ (p vH q) -> (p i^i (_|_` <