Theorem irredlem2 10318

Description: Lemma for irred 10321.

Hypothesis

Ref	Expression
irred.1	|- A e. CH

Assertion

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

Distinct variable group:   q,p,r,A

Proof of Theorem irredlem2

Step	Hyp	Ref	Expression
1		chjcomt 9429	. . . . . 6 |- ((p e. CH /\ q e. CH) -> (p vH q) = (q vH p))
2		atelch 10271	. . . . . 6 |- (p e. Atoms -> p e. CH)
3	1, 2	sylan 448	. . . . 5 |- ((p e. Atoms /\ q e. CH) -> (p vH q) = (q vH p))
4	3	ad2ant2r 409	. . . 4 |- (((p e. Atoms /\ p (_ A) /\ (q e. CH /\ q (_ (_|_` A))) -> (p vH q) = (q vH p))
5	4	adantr 389	. . 3 |- ((((p e. Atoms /\ p (_ A) /\ (q e. CH /\ q (_ (_|_` A))) /\ ((r e. Atoms /\ r (_ A) /\ r (_ (p vH q))) -> (p vH q) = (q vH p))
6	5	ineq2d 2217	. 2 |- ((((p e. Atoms /\ p (_ A) /\ (q e. CH /\ q (_ (_|_` A))) /\ ((r e. Atoms /\ r (_ A) /\ r (_ (p vH q))) -> ((_|_` r) i^i (p vH q)) = ((_|_` r) i^i (q vH p)))
7		fh2t 9562	. . 3 |- ((((_|_` r) e. CH /\ q e. CH /\ p e. CH) /\ (q C_H (_|_` r) /\ q C_H p)) -> ((_|_` r) i^i (q vH p)) = (((_|_` r) i^i q) vH ((_|_` r) i^i p)))
8		atelch 10271	. . . . . . . . . . 11 |- (r e. Atoms -> r e. CH)
9		chocclt 9184	. . . . . . . . . . 11 |- (r e. CH -> (_|_` r) e. CH)
10	8, 9	syl 10	. . . . . . . . . 10 |- (r e. Atoms -> (_|_` r) e. CH)
11		id 59	. . . . . . . . . 10 |- (q e. CH -> q e. CH)
12	10, 11, 2	3anim123i 821	. . . . . . . . 9 |- ((r e. Atoms /\ q e. CH /\ p e. Atoms) -> ((_|_` r) e. CH /\ q e. CH /\ p e. CH))
13	12	3com13 838	. . . . . . . 8 |- ((p e. Atoms /\ q e. CH /\ r e. Atoms) -> ((_|_` r) e. CH /\ q e. CH /\ p e. CH))
14	13	3expa 833	. . . . . . 7 |- (((p e. Atoms /\ q e. CH) /\ r e. Atoms) -> ((_|_` r) e. CH /\ q e. CH /\ p e. CH))
15	14	adantllr 397	. . . . . 6 |- ((((p e. Atoms /\ p (_ A) /\ q e. CH) /\ r e. Atoms) -> ((_|_` r) e. CH /\ q e. CH /\ p e. CH))
16	15	adantlrr 399	. . . . 5 |- ((((p e. Atoms /\ p (_ A) /\ (q e. CH /\ q (_ (_|_` A))) /\ r e. Atoms) -> ((_|_` r) e. CH /\ q e. CH /\ p e. CH))
17	16	adantrr 395	. . . 4 |- ((((p e. Atoms /\ p (_ A) /\ (q e. CH /\ q (_ (_|_` A))) /\ (r e. Atoms /\ r (_ A)) -> ((_|_` r) e. CH /\ q e. CH /\ p e. CH))
18	17	adantrr 395	. . 3 |- ((((p e. Atoms /\ p (_ A) /\ (q e. CH /\ q (_ (_|_` A))) /\ ((r e. Atoms /\ r (_ A) /\ r (_ (p vH q))) -> ((_|_` r) e. CH /\ q e. CH /\ p e. CH))
19		lecmt 9560	. . . . . 6 |- ((q e. CH /\ (_|_` r) e. CH /\ q (_ (_|_` r)) -> q C_H (_|_` r))
20		simpll 412	. . . . . 6 |- (((q e. CH /\ q (_ (_|_` A)) /\ (r e. Atoms /\ r (_ A)) -> q e. CH)
21	10	ad2antrl 406	. . . . . 6 |- (((q e. CH /\ q (_ (_|_` A)) /\ (r e. Atoms /\ r (_ A)) -> (_|_` r) e. CH)
22		sstr 2072	. . . . . . . 8 |- ((q (_ (_|_` A) /\ (_|_` A) (_ (_|_` r)) -> q (_ (_|_` r))
23		irred.1	. . . . . . . . . . 11 |- A e. CH
24		chsscon3t 9423	. . . . . . . . . . 11 |- ((r e. CH /\ A e. CH) -> (r (_ A <-> (_|_` A) (_ (_|_` r)))
25	23, 24	mpan2 696	. . . . . . . . . 10 |- (r e. CH -> (r (_ A <-> (_|_` A) (_ (_|_` r)))
26	8, 25	syl 10	. . . . . . . . 9 |- (r e. Atoms -> (r (_ A <-> (_|_` A) (_ (_|_` r)))
27	26	biimpa 416	. . . . . . . 8 |- ((r e. Atoms /\ r (_ A) -> (_|_` A) (_ (_|_` r))
28	22, 27	sylan2 451	. . . . . . 7 |- ((q (_ (_|_` A) /\ (r e. Atoms /\ r (_ A)) -> q (_ (_|_` r))
29	28	adantll 392	. . . . . 6 |- (((q e. CH /\ q (_ (_|_` A)) /\ (r e. Atoms /\ r (_ A)) -> q (_ (_|_` r))
30	19, 20, 21, 29	syl3anc 858	. . . . 5 |- (((q e. CH /\ q (_ (_|_` A)) /\ (r e. Atoms /\ r (_ A)) -> q C_H (_|_` r))
31	30	ad2ant2lr 410	. . . 4 |- ((((p e. Atoms /\ p (_ A) /\ (q e. CH /\ q (_ (_|_` A))) /\ ((r e. Atoms /\ r (_ A) /\ r (_ (p vH q))) -> q C_H (_|_` r))
32		sstr 2072	. . . . . . . . . . . . 13 |- ((q (_ (_|_` A) /\ (_|_` A) (_ (_|_` p)) -> q (_ (_|_` p))
33		chsscon3t 9423	. . . . . . . . . . . . . . 15 |- ((p e. CH /\ A e. CH) -> (p (_ A <-> (_|_` A) (_ (_|_` p)))
34	23, 33	mpan2 696	. . . . . . . . . . . . . 14 |- (p e. CH -> (p (_ A <-> (_|_` A) (_ (_|_` p)))
35	34	biimpa 416	. . . . . . . . . . . . 13 |- ((p e. CH /\ p (_ A) -> (_|_` A) (_ (_|_` p))
36	32, 35	sylan2 451	. . . . . . . . . . . 12 |- ((q (_ (_|_` A) /\ (p e. CH /\ p (_ A)) -> q (_ (_|_` p))
37	36	an1s 486	. . . . . . . . . . 11 |- ((p e. CH /\ (q (_ (_|_` A) /\ p (_ A)) -> q (_ (_|_` p))
38	37	ancom2s 487	. . . . . . . . . 10 |- ((p e. CH /\ (p (_ A /\ q (_ (_|_` A))) -> q (_ (_|_` p))
39	38	adantll 392	. . . . . . . . 9 |- (((q e. CH /\ p e. CH) /\ (p (_ A /\ q (_ (_|_` A))) -> q (_ (_|_` p))
40		lecmt 9560	. . . . . . . . . . . . 13 |- ((q e. CH /\ (_|_` p) e. CH /\ q (_ (_|_` p)) -> q C_H (_|_` p))
41		chocclt 9184	. . . . . . . . . . . . 13 |- (p e. CH -> (_|_` p) e. CH)
42	40, 41	syl3an2 860	. . . . . . . . . . . 12 |- ((q e. CH /\ p e. CH /\ q (_ (_|_` p)) -> q C_H (_|_` p))
43	42	3expia 835	. . . . . . . . . . 11 |- ((q e. CH /\ p e. CH) -> (q (_ (_|_` p) -> q C_H (_|_` p)))
44		cmcm2t 9559	. . . . . . . . . . 11 |- ((q e. CH /\ p e. CH) -> (q C_H p <-> q C_H (_|_` p)))
45	43, 44	sylibrd 204	. . . . . . . . . 10 |- ((q e. CH /\ p e. CH) -> (q (_ (_|_` p) -> q C_H p))
46	45	adantr 389	. . . . . . . . 9 |- (((q e. CH /\ p e. CH) /\ (p (_ A /\ q (_ (_|_` A))) -> (q (_ (_|_` p) -> q C_H p))
47	39, 46	mpd 26	. . . . . . . 8 |- (((q e. CH /\ p e. CH) /\ (p (_ A /\ q (_ (_|_` A))) -> q C_H p)
48	47, 2	sylanl2 461	. . . . . . 7 |- (((q e. CH /\ p e. Atoms) /\ (p (_ A /\ q (_ (_|_` A))) -> q C_H p)
49	48	ancom1s 490	. . . . . 6 |- (((p e. Atoms /\ q e. CH) /\ (p (_ A /\ q (_ (_|_` A))) -> q C_H p)
50	49	an4s 508	. . . . 5 |- (((p e. Atoms /\ p (_ A) /\ (q e. CH /\ q (_ (_|_` A))) -> q C_H p)
51	50	adantr 389	. . . 4 |- ((((p e. Atoms /\ p (_ A) /\ (q e. CH /\ q (_ (_|_` A))) /\ ((r e. Atoms /\ r (_ A) /\ r (_ (p vH q))) -> q C_H p)
52	31, 51	jca 288	. . 3 |- ((((p e. Atoms /\ p (_ A) /\ (q e. CH /\ q (_ (_|_` A))) /\ ((r e. Atoms /\ r (_ A) /\ r (_ (p vH q))) -> (q C_H (_|_` r) /\ q C_H p))
53	7, 18, 52	sylanc 471	. 2 |- ((((p e. Atoms /\ p (_ A) /\ (q e. CH /\ q (_ (_|_` A))) /\ ((r e. Atoms /\ r (_ A) /\ r (_ (p vH q))) -> ((_|_` r) i^i (q vH p)) = (((_|_` r) i^i q) vH ((_|_` r) i^i p)))
54		sseqin2 2229	. . . . . 6 |- (q (_ (_|_` r) <-> ((_|_` r) i^i q) = q)
55	29, 54	sylib 198	. . . . 5 |- (((q e. CH /\ q (_ (_|_` A)) /\ (r e. Atoms /\ r (_ A)) -> ((_|_` r) i^i q) = q)
56	55	ad2ant2lr 410	. . . 4 |- ((((p e. Atoms /\ p (_ A) /\ (q e. CH /\ q (_ (_|_` A