Theorem 5oalem4 12069

Description: Lemma for orthoarguesian law 5OA.

Hypotheses

Ref	Expression
5oalem3.1	|- A e. SH
5oalem3.2	|- B e. SH
5oalem3.3	|- C e. SH
5oalem3.4	|- D e. SH
5oalem3.5	|- F e. SH
5oalem3.6	|- G e. SH

Assertion

Ref	Expression
5oalem4	|- (((((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) /\ (f e. F /\ g e. G)) /\ ((x +h y) = (f +h g) /\ (z +h w) = (f +h g))) -> (x -h z) e. (((A +H C) i^i (B +H D)) i^i (((A +H F) i^i (B +H G)) +H ((C +H F) i^i (D +H G)))))

Proof of Theorem 5oalem4

Step	Hyp	Ref	Expression
1		eqtr3 2160	. . . 4 |- (((x +h y) = (f +h g) /\ (z +h w) = (f +h g)) -> (x +h y) = (z +h w))
2		5oalem3.1	. . . . 5 |- A e. SH
3		5oalem3.2	. . . . 5 |- B e. SH
4		5oalem3.3	. . . . 5 |- C e. SH
5		5oalem3.4	. . . . 5 |- D e. SH
6	2, 3, 4, 5	5oalem2 12067	. . . 4 |- ((((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) /\ (x +h y) = (z +h w)) -> (x -h z) e. ((A +H C) i^i (B +H D)))
7	1, 6	sylan2 600	. . 3 |- ((((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) /\ ((x +h y) = (f +h g) /\ (z +h w) = (f +h g))) -> (x -h z) e. ((A +H C) i^i (B +H D)))
8	7	adantlr 777	. 2 |- (((((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) /\ (f e. F /\ g e. G)) /\ ((x +h y) = (f +h g) /\ (z +h w) = (f +h g))) -> (x -h z) e. ((A +H C) i^i (B +H D)))
9		5oalem3.5	. . 3 |- F e. SH
10		5oalem3.6	. . 3 |- G e. SH
11	2, 3, 4, 5, 9, 10	5oalem3 12068	. 2 |- (((((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) /\ (f e. F /\ g e. G)) /\ ((x +h y) = (f +h g) /\ (z +h w) = (f +h g))) -> (x -h z) e. (((A +H F) i^i (B +H G)) +H ((C +H F) i^i (D +H G))))
12		elin 2999	. 2 |- ((x -h z) e. (((A +H C) i^i (B +H D)) i^i (((A +H F) i^i (B +H G)) +H ((C +H F) i^i (D +H G)))) <-> ((x -h z) e. ((A +H C) i^i (B +H D)) /\ (x -h z) e. (((A +H F) i^i (B +H G)) +H ((C +H F) i^i (D +H G)))))
13	8, 11, 12	sylanbrc 664	1 |- (((((x e. A /\ y e. B) /\ (z e. C /\ w e. D)) /\ (f e. F /\ g e. G)) /\ ((x +h y) = (f +h g) /\ (z +h w) = (f +h g))) -> (x -h z) e. (((A +H C) i^i (B +H D)) i^i (((A +H F) i^i (B +H G)) +H ((C +H F) i^i (D +H G)))))

Syntax hints:   -> wi 3   /\ wa 337   = wceq 1586   e. wcel 1588   i^i cin 2826  (class class class)co 4981   +h cva 11259   -h cmv 11262  SHcsh 11267   +H cph 11270

This theorem is referenced by:  5oalem5 12070

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-rep 3596  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929  ax-inf2 5964  ax-hilex 11339  ax-hfvadd 11340  ax-hvcom 11341  ax-hvass 11342  ax-hv0cl 11343  ax-hvaddid 11344  ax-hfvmul 11345  ax-hvmulid 11346  ax-hvmulass 11347  ax-hvdistr1 11348  ax-hvdistr2 11349  ax-hvmul0 11350

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-nel 2269  df-ral 2359  df-rex 2360  df-reu 2361  df-rab 2362  df-v 2540  df-sbc 2700  df-csb 2774  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-if 3181  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-int 3401  df-iun 3438  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-id 3747  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-lim 3816  df-suc 3817  df-om 4086  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-f 4143  df-f1 4144  df-fo 4145  df-f1o 4146  df-fv 4147  df-opr 4983  df-oprab 4984  df-mpt 5099  df-1st 5126  df-2nd 5127  df-iota 5219  df-rdg 5304  df-1o 5344  df-oadd 5346  df-omul 5347  df-er 5479  df-ec 5481  df-qs 5484  df-en 5588  df-dom 5589  df-sdom 5590  df-undef 5725  df-riota 5729  df-ni 6518  df-pli 6519  df-mi 6520  df-lti 6521  df-plpq 6553  df-mpq 6554  df-enq 6555  df-nq 6556  df-plq 6557  df-mq 6558  df-rq 6559  df-ltq 6560  df-1q 6561  df-np 6604  df-1p 6605  df-plp 6606  df-mp 6607  df-ltp 6608  df-plpr 6682  df-mpr 6683  df-enr 6684  df-nr 6685  df-plr 6686  df-mr 6687  df-ltr 6688  df-0r 6689  df-1r 6690  df-m1r 6691  df-c 6758  df-0 6759  df-1 6760  df-i 6761  df-r 6762  df-plus 6763  df-mul 6764  df-lt 6765  df-pnf 6846  df-mnf 6847  df-xr 6848  df-ltxr 6849  df-le 6850  df-sub 7009  df-neg 7011  df-hvsub 11310  df-hlim 11311  df-sh 11545  df-ch 11559  df-shsum 11740

Copyright terms: Public domain