Theorem irredlem3 10314

Description: Lemma for irred 10316.

Hypotheses

Ref	Expression
irred.1	|- A e. CH
irred.2	|- (x e. CH -> A C_H x)

Assertion

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

Distinct variable group:   q,p,r,x,A

Proof of Theorem irredlem3

Step	Hyp	Ref	Expression
1		irred.1	. . . . . . . . . . . 12 |- A e. CH
2	1	irredlem2 10313	. . . . . . . . . . 11 |- ((((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)
3	2	opreq2d 3982	. . . . . . . . . 10 |- ((((p e. Atoms /\ p (_ A) /\ (q e. CH /\ q (_ (_|_` A))) /\ ((r e. Atoms /\ r (_ A) /\ r (_ (p vH q))) -> (r vH ((_|_` r) i^i (p vH q))) = (r vH q))
4		pjoml2t 9549	. . . . . . . . . . . . 13 |- ((r e. CH /\ (p vH q) e. CH /\ r (_ (p vH q)) -> (r vH ((_|_` r) i^i (p vH q))) = (p vH q))
5		atelch 10266	. . . . . . . . . . . . . 14 |- (r e. Atoms -> r e. CH)
6	5	adantr 391	. . . . . . . . . . . . 13 |- ((r e. Atoms /\ r (_ A) -> r e. CH)
7		chjclt 9324	. . . . . . . . . . . . . . 15 |- ((p e. CH /\ q e. CH) -> (p vH q) e. CH)
8		atelch 10266	. . . . . . . . . . . . . . 15 |- (p e. Atoms -> p e. CH)
9	7, 8	sylan 450	. . . . . . . . . . . . . 14 |- ((p e. Atoms /\ q e. CH) -> (p vH q) e. CH)
10	9	ad2ant2r 411	. . . . . . . . . . . . 13 |- (((p e. Atoms /\ p (_ A) /\ (q e. CH /\ q (_ (_|_` A))) -> (p vH q) e. CH)
11		id 59	. . . . . . . . . . . . 13 |- (r (_ (p vH q) -> r (_ (p vH q))
12	4, 6, 10, 11	syl3an 870	. . . . . . . . . . . 12 |- (((r e. Atoms /\ r (_ A) /\ ((p e. Atoms /\ p (_ A) /\ (q e. CH /\ q (_ (_|_` A))) /\ r (_ (p vH q)) -> (r vH ((_|_` r) i^i (p vH q))) = (p vH q))
13	12	3com12 839	. . . . . . . . . . 11 |- ((((p e. Atoms /\ p (_ A) /\ (q e. CH /\ q (_ (_|_` A))) /\ (r e. Atoms /\ r (_ A) /\ r (_ (p vH q)) -> (r vH ((_|_` r) i^i (p vH q))) = (p vH q))
14	13	3expb 836	. . . . . . . . . 10 |- ((((p e. Atoms /\ p (_ A) /\ (q e. CH /\ q (_ (_|_` A))) /\ ((r e. Atoms /\ r (_ A) /\ r (_ (p vH q))) -> (r vH ((_|_` r) i^i (p vH q))) = (p vH q))
15	3, 14	eqtr3d 1512	. . . . . . . . 9 |- ((((p e. Atoms /\ p (_ A) /\ (q e. CH /\ q (_ (_|_` A))) /\ ((r e. Atoms /\ r (_ A) /\ r (_ (p vH q))) -> (r vH q) = (p vH q))
16	15	ineq2d 2220	. . . . . . . 8 |- ((((p e. Atoms /\ p (_ A) /\ (q e. CH /\ q (_ (_|_` A))) /\ ((r e. Atoms /\ r (_ A) /\ r (_ (p vH q))) -> (A i^i (r vH q)) = (A i^i (p vH q)))
17		breq2 2628	. . . . . . . . . . . . . . . 16 |- (x = r -> (A C_H x <-> A C_H r))
18		irred.2	. . . . . . . . . . . . . . . 16 |- (x e. CH -> A C_H x)
19	17, 18	vtoclga 1855	. . . . . . . . . . . . . . 15 |- (r e. CH -> A C_H r)
20		breq2 2628	. . . . . . . . . . . . . . . 16 |- (x = q -> (A C_H x <-> A C_H q))
21	20, 18	vtoclga 1855	. . . . . . . . . . . . . . 15 |- (q e. CH -> A C_H q)
22	19, 21	anim12i 333	. . . . . . . . . . . . . 14 |- ((r e. CH /\ q e. CH) -> (A C_H r /\ A C_H q))
23		fh1t 9556	. . . . . . . . . . . . . . 15 |- (((A e. CH /\ r e. CH /\ q e. CH) /\ (A C_H r /\ A C_H q)) -> (A i^i (r vH q)) = ((A i^i r) vH (A i^i q)))
24	1, 23	mp3anl1 912	. . . . . . . . . . . . . 14 |- (((r e. CH /\ q e. CH) /\ (A C_H r /\ A C_H q)) -> (A i^i (r vH q)) = ((A i^i r) vH (A i^i q)))
25	22, 24	mpdan 706	. . . . . . . . . . . . 13 |- ((r e. CH /\ q e. CH) -> (A i^i (r vH q)) = ((A i^i r) vH (A i^i q)))
26	25, 5	sylan 450	. . . . . . . . . . . 12 |- ((r e. Atoms /\ q e. CH) -> (A i^i (r vH q)) = ((A i^i r) vH (A i^i q)))
27	26	ancoms 438	. . . . . . . . . . 11 |- ((q e. CH /\ r e. Atoms) -> (A i^i (r vH q)) = ((A i^i r) vH (A i^i q)))
28	27	adantrr 397	. . . . . . . . . 10 |- ((q e. CH /\ (r e. Atoms /\ r (_ A)) -> (A i^i (r vH q)) = ((A i^i r) vH (A i^i q)))
29	28	ad2ant2r 411	. . . . . . . . 9 |- (((q e. CH /\ q (_ (_|_` A)) /\ ((r e. Atoms /\ r (_ A) /\ r (_ (p vH q))) -> (A i^i (r vH q)) = ((A i^i r) vH (A i^i q)))
30	29	adantll 394	. . . . . . . 8 |- ((((p e. Atoms /\ p (_ A) /\ (q e. CH /\ q (_ (_|_` A))) /\ ((r e. Atoms /\ r (_ A) /\ r (_ (p vH q))) -> (A i^i (r vH q)) = ((A i^i r) vH (A i^i q)))
31		breq2 2628	. . . . . . . . . . . . . 14 |- (x = p -> (A C_H x <-> A C_H p))
32	31, 18	vtoclga 1855	. . . . . . . . . . . . 13 |- (p e. CH -> A C_H p)
33	32, 21	anim12i 333	. . . . . . . . . . . 12 |- ((p e. CH /\ q e. CH) -> (A C_H p /\ A C_H q))
34		fh1t 9556	. . . . . . . . . . . . 13 |- (((A e. CH /\ p e. CH /\ q e. CH) /\ (A C_H p /\ A C_H q)) -> (A i^i (p vH q)) = ((A i^i p) vH (A i^i q)))
35	1, 34	mp3anl1 912	. . . . . . . . . . . 12 |- (((p e. CH /\ q e. CH) /\ (A C_H p /\ A C_H q)) -> (A i^i (p vH q)) = ((A i^i p) vH (A i^i q)))
36	33, 35	mpdan 706	. . . . . . . . . . 11 |- ((p e. CH /\ q e. CH) -> (A i^i (p vH q)) = ((A i^i p) vH (A i^i q)))
37	36, 8	sylan 450	. . . . . . . . . 10 |- ((p e. Atoms /\ q e. CH) -> (A i^i (p vH q)) = ((A i^i p) vH (A i^i q)))
38	37	ad2ant2r 411	. . . . . . . . 9 |- (((p e. Atoms /\ p (_ A) /\ (q e. CH /\ q (_ (_|_` A))) -> (A i^i (p vH q)) = ((A i^i p) vH (A i^i q)))
39	38	adantr 391	. . . . . . . 8 |- ((((p e. Atoms /\ p (_ A) /\ (q e. CH /\ q (_ (_|_` A))) /\ ((r e. Atoms /\ r (_ A) /\ r (_ (p vH q))) -> (A i^i (p vH q)) = ((A i^i p) vH (A i^i q)))
40	16, 30, 39	3eqtr3d 1518	. . . . . . 7 |- ((((p e. Atoms /\ p (_ A) /\ (q e. CH /\ q (_ (_|_` A))) /\ ((r e. Atoms /\ r (_ A) /\ r (_ (p vH q))) -> ((A i^i r) vH (A i^i q)) = ((A i^i p) vH (A i^i q)))
41		sseqin2 2232	. . . . . . . . . . 11 |- (r (_ A <-> (A i^i r) = r)
42	41	biimp 151	. . . . . . . . . 10 |- (r (_ A -> (A i^i r) = r)
43	42	ad2antlr 407	. . . . . . . . 9 |- (((r e. Atoms /\ r (_ A) /\ r (_ (p vH q)) -> (A i^i r) = r)
44	43	adantl 390	. . . . . . . 8 |- ((((p e. Atoms /\ p (_ A) /\ (q e. CH /\ q (_ (_|_` A))) /\ ((r e. Atoms /\ r (_ A) /\ r (_ (p vH q))) -> (A i^i r) = r)
45		chsh 9091	. . . . . . . . . . . 12 |- (q e. CH -> q e. SH)
46	1	chshi 9092	. . . . . . . . . . . . 13 |- A e. SH
47		orthin 9365	. . . . . . . . . . . . 13 |- ((q e. SH /\ A e. SH) -> (q (_ (_|_` A) -> (q i^i A) = 0H))
48	46, 47	mpan2 698	. . . . . . . . . . . 12 |- (q e. SH -> (q (_ (_|_` A) -> (q i^i A) = 0H))
49	45, 48	syl 10	. . . . . . . . . . 11 |- (q e. CH -> (q (_ (_|_` A) -> (q i^i A) = 0H))
50	49	imp 350	. . . . . . . . . 10 |- ((q e. CH /\ q (_ (_|_` A)) -> (q i^i A) = 0H)
51		incom 2211	. . . . . . . . . 10 |- (A i^i q) = (q i^i A)
52	50, 51	syl5eq 1522	. . . . . . . . 9 |- ((q e. CH /\ q (_ (_|_` A)) -> (A i^i q) = 0H)
53	52	ad2antlr 407	. . . . . . . 8 |- ((((p e. Atoms /\ p (_ A) /\ (q e. CH /\ q (_ (_|_` A))) /\ ((r e. Atoms /\ r (_ A) /\ r (_ (p vH q))) -> (A i^i q) = 0H)
54	44, 53	opreq12d 3984	. . . . . . 7 |- ((((p e. Atoms /\ p (_ A) /\ (q e. CH /\ q (_ (_|_` A))) /\ ((r e. Atoms /\ r (_ A) /\ r (_ (p vH q))) -> ((A i^i r) vH (A