Theorem 5oa 5551

Description: Orthoarguesian law 5OA. This 8-variable inference is called 5OA because it can be converted to a 5-variable equation (see Quantum Logic Explorer).

Hypotheses

Ref	Expression
5oa.1	|- A e. CH
5oa.2	|- B e. CH
5oa.3	|- C e. CH
5oa.4	|- D e. CH
5oa.5	|- F e. CH
5oa.6	|- G e. CH
5oa.7	|- R e. CH
5oa.8	|- S e. CH
5oa.9	|- A (_ (_|_` B)
5oa.10	|- C (_ (_|_` D)
5oa.11	|- F (_ (_|_` G)
5oa.12	|- R (_ (_|_` S)

Assertion

Ref	Expression
5oa	|- (((A vH B) i^i (C vH D)) i^i ((F vH G) i^i (R vH S))) (_ (B vH (A i^i (C vH ((((A vH C) i^i (B vH D)) i^i (((A vH R) i^i (B vH S)) vH ((C vH R) i^i (D vH S)))) i^i ((((A vH F) i^i (B vH G)) i^i (((A vH R) i^i (B vH S)) vH ((F vH R) i^i (G vH S)))) vH (((C vH F) i^i (D vH G)) i^i (((C vH R) i^i (D vH S)) vH ((F vH R) i^i (G vH S)))))))))

Proof of Theorem 5oa

Step	Hyp	Ref	Expression
1		5oa.9	. . . . . . 7 |- A (_ (_|_` B)
2		5oa.1	. . . . . . . 8 |- A e. CH
3		5oa.2	. . . . . . . 8 |- B e. CH
4	2, 3	osum 5538	. . . . . . 7 |- (A (_ (_|_` B) -> (A +H B) = (A vH B))
5	1, 4	ax-mp 6	. . . . . 6 |- (A +H B) = (A vH B)
6		5oa.10	. . . . . . 7 |- C (_ (_|_` D)
7		5oa.3	. . . . . . . 8 |- C e. CH
8		5oa.4	. . . . . . . 8 |- D e. CH
9	7, 8	osum 5538	. . . . . . 7 |- (C (_ (_|_` D) -> (C +H D) = (C vH D))
10	6, 9	ax-mp 6	. . . . . 6 |- (C +H D) = (C vH D)
11		ineq12 1640	. . . . . 6 |- (((A +H B) = (A vH B) /\ (C +H D) = (C vH D)) -> ((A +H B) i^i (C +H D)) = ((A vH B) i^i (C vH D)))
12	5, 10, 11	mp2an 520	. . . . 5 |- ((A +H B) i^i (C +H D)) = ((A vH B) i^i (C vH D))
13		5oa.11	. . . . . . 7 |- F (_ (_|_` G)
14		5oa.5	. . . . . . . 8 |- F e. CH
15		5oa.6	. . . . . . . 8 |- G e. CH
16	14, 15	osum 5538	. . . . . . 7 |- (F (_ (_|_` G) -> (F +H G) = (F vH G))
17	13, 16	ax-mp 6	. . . . . 6 |- (F +H G) = (F vH G)
18		5oa.12	. . . . . . 7 |- R (_ (_|_` S)
19		5oa.7	. . . . . . . 8 |- R e. CH
20		5oa.8	. . . . . . . 8 |- S e. CH
21	19, 20	osum 5538	. . . . . . 7 |- (R (_ (_|_` S) -> (R +H S) = (R vH S))
22	18, 21	ax-mp 6	. . . . . 6 |- (R +H S) = (R vH S)
23		ineq12 1640	. . . . . 6 |- (((F +H G) = (F vH G) /\ (R +H S) = (R vH S)) -> ((F +H G) i^i (R +H S)) = ((F vH G) i^i (R vH S)))
24	17, 22, 23	mp2an 520	. . . . 5 |- ((F +H G) i^i (R +H S)) = ((F vH G) i^i (R vH S))
25		ineq12 1640	. . . . 5 |- ((((A +H B) i^i (C +H D)) = ((A vH B) i^i (C vH D)) /\ ((F +H G) i^i (R +H S)) = ((F vH G) i^i (R vH S))) -> (((A +H B) i^i (C +H D)) i^i ((F +H G) i^i (R +H S))) = (((A vH B) i^i (C vH D)) i^i ((F vH G) i^i (R vH S))))
26	12, 24, 25	mp2an 520	. . . 4 |- (((A +H B) i^i (C +H D)) i^i ((F +H G) i^i (R +H S))) = (((A vH B) i^i (C vH D)) i^i ((F vH G) i^i (R vH S)))
27	26	cleqcomi 1105	. . 3 |- (((A vH B) i^i (C vH D)) i^i ((F vH G) i^i (R vH S))) = (((A +H B) i^i (C +H D)) i^i ((F +H G) i^i (R +H S)))
28	2	chshi 5132	. . . 4 |- A e. SH
29	3	chshi 5132	. . . 4 |- B e. SH
30	7	chshi 5132	. . . 4 |- C e. SH
31	8	chshi 5132	. . . 4 |- D e. SH
32	14	chshi 5132	. . . 4 |- F e. SH
33	15	chshi 5132	. . . 4 |- G e. SH
34	19	chshi 5132	. . . 4 |- R e. SH
35	20	chshi 5132	. . . 4 |- S e. SH
36	28, 29, 30, 31, 32, 33, 34, 35	5oalem7 5550	. . 3 |- (((A +H B) i^i (C +H D)) i^i ((F +H G) i^i (R +H S))) (_ (B +H (A i^i (C +H ((((A +H C) i^i (B +H D)) i^i (((A +H R) i^i (B +H S)) +H ((C +H R) i^i (D +H S)))) i^i ((((A +H F) i^i (B +H G)) i^i (((A +H R) i^i (B +H S)) +H ((F +H R) i^i (G +H S)))) +H (((C +H F) i^i (D +H G)) i^i (((C +H R) i^i (D +H S)) +H ((F +H R) i^i (G +H S)))))))))
37	27, 36	eqsstr 1530	. 2 |- (((A vH B) i^i (C vH D)) i^i ((F vH G) i^i (R vH S))) (_ (B +H (A i^i (C +H ((((A +H C) i^i (B +H D)) i^i (((A +H R) i^i (B +H S)) +H ((C +H R) i^i (D +H S)))) i^i ((((A +H F) i^i (B +H G)) i^i (((A +H R) i^i (B +H S)) +H ((F +H R) i^i (G +H S)))) +H (((C +H F) i^i (D +H G)) i^i (((C +H R) i^i (D +H S)) +H ((F +H R) i^i (G +H S)))))))))
38	28, 30	shscl 5282	. . . . . . . . 9 |- (A +H C) e. SH
39	29, 31	shscl 5282	. . . . . . . . 9 |- (B +H D) e. SH
40	38, 39	shincl 5332	. . . . . . . 8 |- ((A +H C) i^i (B +H D)) e. SH
41	28, 34	shscl 5282	. . . . . . . . . 10 |- (A +H R) e. SH
42	29, 35	shscl 5282	. . . . . . . . . 10 |- (B +H S) e. SH
43	41, 42	shincl 5332	. . . . . . . . 9 |- ((A +H R) i^i (B +H S)) e. SH
44	30, 34	shscl 5282	. . . . . . . . . 10 |- (C +H R) e. SH
45	31, 35	shscl 5282	. . . . . . . . . 10 |- (D +H S) e. SH
46	44, 45	shincl 5332	. . . . . . . . 9 |- ((C +H R) i^i (D +H S)) e. SH
47	43, 46	shscl 5282	. . . . . . . 8 |- (((A +H R) i^i (B +H S)) +H ((C +H R) i^i (D +H S))) e. SH
48	40, 47	shincl 5332	. . . . . . 7 |- (((A +H C) i^i (B +H D)) i^i (((A +H R) i^i (B +H S)) +H ((C +H R) i^i (D +H S)))) e. SH
49	28, 32	shscl 5282	. . . . . . . . . 10 |- (A +H F) e. SH
50	29, 33	shscl 5282	. . . . . . . . . 10 |- (B +H G) e. SH
51	49, 50	shincl 5332	. . . . . . . . 9 |- ((A +H F) i^i (B +H G)) e. SH
52	32, 34	shscl 5282	. . . . . . . . . . 11 |- (F +H R) e. SH
53	33, 35	shscl 5282	. . . . . . . . . . 11 |- (G +H S) e. SH
54	52, 53	shincl 5332	. . . . . . . . . 10 |- ((F +H R) i^i (G +H S)) e. SH
55	43, 54	shscl 5282	. . . . . . . . 9 |- (((A +H R) i^i (B +H S)) +H ((F +H R) i^i (G +H S))) e. SH
56	51, 55	shincl 5332	. . . . . . . 8 |- (((A +H F) i^i (B +H G)) i^i (((A +H R) i^i (B +H S)) +H ((F +H R) i^i (G +H S)))) e. SH
57	30, 32	shscl 5282	. . . . . . . . . 10 |- (C +H F) e. SH
58	31, 33	shscl 5282	. . . . . . . . . 10 |- (D +H G) e. SH
59	57, 58	shincl 5332	. . . . . . . . 9 |- ((C +H F) i^i (D +H G)) e. SH
60	46, 54	shscl 5282	. . . . . . . . 9 |- (((C +H R) i^i (D +H S)) +H ((F +H R) i^i (G +H S))) e. SH
61	59, 60	shincl 5332	. . . . . . . 8 |- (((C +H F) i^i (D +H G)) i^i (((C +H R) i^i (D +H S)) +H ((F +H R) i^i (G +H S)))) e. SH
62	56, 61	shscl 5282	. . . . . . 7 |- ((((A +H F) i^i (B +H G)) i^i (((A +H R) i^i (B +H S)) +H ((F +H R) i^i (G +H S)))) +H (((C +H F) i^i (D +H G)) i^i (((C +H R) i^i (D +H S)) +H ((F +H R) i^i (G +H S))))) e. SH
63	48, 62	shincl 5332	. . . . . 6 |- ((((A +H C) i^i (B +H D)) i^i (((A +H R) i^i (B +H S)) +H ((C +H R) i^i (D +H S)))) i^i ((((A +H F) i^i (B +H G)) i^i (((A +H R) i^i (B +H S)) +H ((F +H R) i^i (G +H S)))) +H (((C +H F) i^i (D +H G)) i^i (((C +H R) i^i (D +H S)) +H ((F +H R) i^i (G +H S)))))) e. SH
64	30, 63	shscl 5282	. . . . 5 |- (C +H ((((A +H C) i^i (B +H D)) i^i (((A +H R) i^i (B +H S)) +H ((C +H R) i^i (D +H S)))) i^i ((((A +H F) i^i (B +H G)) i^i (((A +H R) i^i (B +H S)) +H ((F +H R) i^i (G +H S)))) +H (((C +H F) i^i (D +H G)) i^i (((C +H R) i^i (D +H S)) +H ((F +H R) i^i (G +H S))))))) e.