Theorem mayete3 9590

Description: Mayet's equation E₃. Part of Theorem 4.1 of [Mayet3] p. 7.

Hypotheses

Ref	Expression
mayete3.1	|- A e. CH
mayete3.2	|- B e. CH
mayete3.3	|- C e. CH
mayete3.4	|- D e. CH
mayete3.5	|- F e. CH
mayete3.6	|- G e. CH
mayete3.7	|- A (_ (_|_` B)
mayete3.8	|- A (_ (_|_` C)
mayete3.9	|- B (_ (_|_` C)
mayete3.10	|- A (_ (_|_` D)
mayete3.11	|- B (_ (_|_` F)
mayete3.12	|- C (_ (_|_` G)
mayete3.13	|- R = ((A vH B) vH C)
mayete3.14	|- S = (((A vH D) i^i (B vH F)) i^i (C vH G))
mayete3.15	|- T = ((D vH F) vH G)

Assertion

Ref	Expression
mayete3	|- (R i^i S) (_ T

Proof of Theorem mayete3

Step	Hyp	Ref	Expression
1		elin 2197	. . . . . . . 8 |- (x e. (R i^i S) <-> (x e. R /\ x e. S))
2		mayete3.13	. . . . . . . . . . 11 |- R = ((A vH B) vH C)
3	2	eleq2i 1530	. . . . . . . . . 10 |- (x e. R <-> x e. ((A vH B) vH C))
4		mayete3.1	. . . . . . . . . . . . 13 |- A e. CH
5		mayete3.2	. . . . . . . . . . . . 13 |- B e. CH
6	4, 5	chjcl 9295	. . . . . . . . . . . 12 |- (A vH B) e. CH
7		mayete3.3	. . . . . . . . . . . 12 |- C e. CH
8	6, 7	chjcl 9295	. . . . . . . . . . 11 |- ((A vH B) vH C) e. CH
9	8	chel 9023	. . . . . . . . . 10 |- (x e. ((A vH B) vH C) -> x e. H~)
10	3, 9	sylbi 199	. . . . . . . . 9 |- (x e. R -> x e. H~)
11	10	adantr 389	. . . . . . . 8 |- ((x e. R /\ x e. S) -> x e. H~)
12	1, 11	sylbi 199	. . . . . . 7 |- (x e. (R i^i S) -> x e. H~)
13		ax-hvmulid 8797	. . . . . . . 8 |- (x e. H~ -> (1 .h x) = x)
14		2cn 5927	. . . . . . . . . . 11 |- 2 e. CC
15		2ne0 5937	. . . . . . . . . . 11 |- 2 =/= 0
16	14, 15	reccl 5682	. . . . . . . . . 10 |- (1 / 2) e. CC
17		ax-hvmulass 8798	. . . . . . . . . 10 |- (((1 / 2) e. CC /\ 2 e. CC /\ x e. H~) -> (((1 / 2) x. 2) .h x) = ((1 / 2) .h (2 .h x)))
18	16, 14, 17	mp3an12 903	. . . . . . . . 9 |- (x e. H~ -> (((1 / 2) x. 2) .h x) = ((1 / 2) .h (2 .h x)))
19		recid2t 5699	. . . . . . . . . . 11 |- ((2 e. CC /\ 2 =/= 0) -> ((1 / 2) x. 2) = 1)
20	14, 15, 19	mp2an 695	. . . . . . . . . 10 |- ((1 / 2) x. 2) = 1
21	20	opreq1i 3956	. . . . . . . . 9 |- (((1 / 2) x. 2) .h x) = (1 .h x)
22	18, 21	syl5eqr 1513	. . . . . . . 8 |- (x e. H~ -> (1 .h x) = ((1 / 2) .h (2 .h x)))
23	13, 22	eqtr3d 1501	. . . . . . 7 |- (x e. H~ -> x = ((1 / 2) .h (2 .h x)))
24	12, 23	syl 10	. . . . . 6 |- (x e. (R i^i S) -> x = ((1 / 2) .h (2 .h x)))
25		hv2timest 8849	. . . . . . . . . . . . 13 |- (x e. H~ -> (2 .h x) = (x +h x))
26	25	opreq1d 3960	. . . . . . . . . . . 12 |- (x e. H~ -> ((2 .h x) +h x) = ((x +h x) +h x))
27	12, 26	syl 10	. . . . . . . . . . 11 |- (x e. (R i^i S) -> ((2 .h x) +h x) = ((x +h x) +h x))
28		inss2 2221	. . . . . . . . . . . . 13 |- (R i^i S) (_ S
29	28	sseli 2055	. . . . . . . . . . . 12 |- (x e. (R i^i S) -> x e. S)
30		mayete3.14	. . . . . . . . . . . . . . 15 |- S = (((A vH D) i^i (B vH F)) i^i (C vH G))
31	30	eleq2i 1530	. . . . . . . . . . . . . 14 |- (x e. S <-> x e. (((A vH D) i^i (B vH F)) i^i (C vH G)))
32		elin 2197	. . . . . . . . . . . . . 14 |- (x e. (((A vH D) i^i (B vH F)) i^i (C vH G)) <-> (x e. ((A vH D) i^i (B vH F)) /\ x e. (C vH G)))
33	31, 32	bitr 173	. . . . . . . . . . . . 13 |- (x e. S <-> (x e. ((A vH D) i^i (B vH F)) /\ x e. (C vH G)))
34		elin 2197	. . . . . . . . . . . . . . . 16 |- (x e. ((A vH D) i^i (B vH F)) <-> (x e. (A vH D) /\ x e. (B vH F)))
35		mayete3.10	. . . . . . . . . . . . . . . . . 18 |- A (_ (_|_` D)
36		mayete3.4	. . . . . . . . . . . . . . . . . . 19 |- D e. CH
37	4, 36	pjds 9574	. . . . . . . . . . . . . . . . . 18 |- ((x e. (A vH D) /\ A (_ (_|_` D)) -> x = (((proj` A)` x) +h ((proj` D)` x)))
38	35, 37	mpan2 694	. . . . . . . . . . . . . . . . 17 |- (x e. (A vH D) -> x = (((proj` A)` x) +h ((proj` D)` x)))
39		mayete3.11	. . . . . . . . . . . . . . . . . 18 |- B (_ (_|_` F)
40		mayete3.5	. . . . . . . . . . . . . . . . . . 19 |- F e. CH
41	5, 40	pjds 9574	. . . . . . . . . . . . . . . . . 18 |- ((x e. (B vH F) /\ B (_ (_|_` F)) -> x = (((proj` B)` x) +h ((proj` F)` x)))
42	39, 41	mpan2 694	. . . . . . . . . . . . . . . . 17 |- (x e. (B vH F) -> x = (((proj` B)` x) +h ((proj` F)` x)))
43	38, 42	opreqan12d 3964	. . . . . . . . . . . . . . . 16 |- ((x e. (A vH D) /\ x e. (B vH F)) -> (x +h x) = ((((proj` A)` x) +h ((proj` D)` x)) +h (((proj` B)` x) +h ((proj` F)` x))))
44	34, 43	sylbi 199	. . . . . . . . . . . . . . 15 |- (x e. ((A vH D) i^i (B vH F)) -> (x +h x) = ((((proj` A)` x) +h ((proj` D)` x)) +h (((proj` B)` x) +h ((proj` F)` x))))
45		inss1 2220	. . . . . . . . . . . . . . . . . 18 |- ((A vH D) i^i (B vH F)) (_ (A vH D)
46	45	sseli 2055	. . . . . . . . . . . . . . . . 17 |- (x e. ((A vH D) i^i (B vH F)) -> x e. (A vH D))
47	4, 36	chjcl 9295	. . . . . . . . . . . . . . . . . 18 |- (A vH D) e. CH
48	47	chel 9023	. . . . . . . . . . . . . . . . 17 |- (x e. (A vH D) -> x e. H~)
49	46, 48	syl 10	. . . . . . . . . . . . . . . 16 |- (x e. ((A vH D) i^i (B vH F)) -> x e. H~)
50		hvadd4t 8826	. . . . . . . . . . . . . . . . 17 |- (((((proj` A)` x) e. H~ /\ ((proj` D)` x) e. H~) /\ (((proj` B)` x) e. H~ /\ ((proj` F)` x) e. H~)) -> ((((proj` A)` x) +h ((proj` D)` x)) +h (((proj` B)` x) +h ((proj` F)` x))) = ((((proj` A)` x) +h ((proj` B)` x)) +h (((proj` D)` x) +h ((proj` F)` x))))
51	4	pjhcl 9167	. . . . . . . . . . . . . . . . 17 |- (x e. H~ -> ((proj` A)` x) e. H~)
52	36	pjhcl 9167	. . . . . . . . . . . . . . . . 17 |- (x e. H~ -> ((proj` D)` x) e. H~)
53	5	pjhcl 9167	. . . . . . . . . . . . . . . . 17 |- (x e. H~ -> ((proj` B)` x) e. H~)
54	40	pjhcl 9167	. . . . . . . . . . . . . . . . 17 |- (x e. H~ -> ((proj` F)` x) e. H~)
55	50, 51, 52, 53, 54	syl2anc 472	. . . . . . . . . . . . . . . 16 |- (x e. H~ -> ((((proj` A)` x) +h ((proj` D)` x)) +h (((proj` B)` x) +h ((proj` F)` x))) = ((((proj` A)` x) +h ((proj` B)` x)) +h (((proj` D)` x) +h ((proj` F)` x))))
56	49, 55	syl 10	. . . . . . . . . . . . . . 15 |- (x e. ((A vH D) i^i (B vH F)) -> ((((proj` A)` x) +h ((proj` D)` x)) +h (((proj` B)` x) +h ((proj` F)` x))) = ((((proj` A)` x) +h ((proj` B)` x)) +h (((proj` D)` x) +h ((proj` F)` x))))
57	44, 56	eqtrd 1499	. . . . . . . . . . . . . 14 |- (x e. ((A vH D) i^i (B vH F)) -> (x +h x) = ((((proj` A)` x) +h ((proj` B)` x)) +h (((proj` D)` x) +h ((proj` F)` x))))
58		mayete3.12	. . . . . . . . . . . . . . 15 |- C (_ (_|_` G)
59		mayete3.6	. . . . . . . . . . . . . . . 16 |- G e. CH
60	7, 59	pjds 9574	. . . . . . . . . . . . . . 15 |- ((x e. (C vH G) /\ C (_ (_|_` G)) -> x = (((proj` C)` x) +h ((proj` G)` x)))
61	58, 60	mpan2 694	. . . . . . . . . . . . . 14 |- (x e. (C vH G) -> x = (((proj` C)` x) +h ((proj` G)` x)))
62	57, 61	opreqan12d 3964	. . . . . . . . . . . . 13 |- ((x e. ((A vH D) i^i (B vH F)) /\ x e. (C vH G)) -> ((x +h x) +h x) = (((((proj` A)` x) +h ((proj` B)` x)) +h (((proj` D)` x) +h ((proj` F)` x))) +h (((proj` C)` x) +h ((proj` G)` x))))
63	33, 62	sylbi 199	. . . . . . . . . . . 12 |- (x e. S -> ((x +h x) +h x) = (((((proj` A)` x) +h ((proj` B)` x)) +h (((proj` D)` x) +h ((proj` F)` x))) +h (((proj` C)` x) +h ((proj` G)` x))))
64	29, 63	syl 10	. . . . . . . . . . 11 |- (x e. (R i^i S) -> ((x +h x) +h x) = (((((proj` A)` x) +h ((proj` B)` x)) +h (((proj` D)` x) +h ((proj` F)` x))) +h (((proj` C)` x) +h ((proj` G)` x))))