Theorem comcom2 183

Description: Commutation equivalence. Kalmbach 83 p. 23. Does not use OML. (Contributed by NM, 27-Aug-1997.)

Hypothesis

Ref	Expression
comcom2.1	a C b

Assertion

Ref	Expression
comcom2	a C b⊥

Proof of Theorem comcom2

Step	Hyp	Ref	Expression
1		comcom2.1	. . . . 5 a C b
2	1	df-c2 133	. . . 4 a = ((a ∩ b) ∪ (a ∩ b⊥ ))
3		ax-a1 30	. . . . . 6 b = b⊥ ⊥
4	3	lan 77	. . . . 5 (a ∩ b) = (a ∩ b⊥ ⊥ )
5	4	ax-r5 38	. . . 4 ((a ∩ b) ∪ (a ∩ b⊥ )) = ((a ∩ b⊥ ⊥ ) ∪ (a ∩ b⊥ ))
6	2, 5	ax-r2 36	. . 3 a = ((a ∩ b⊥ ⊥ ) ∪ (a ∩ b⊥ ))
7		ax-a2 31	. . 3 ((a ∩ b⊥ ⊥ ) ∪ (a ∩ b⊥ )) = ((a ∩ b⊥ ) ∪ (a ∩ b⊥ ⊥ ))
8	6, 7	ax-r2 36	. 2 a = ((a ∩ b⊥ ) ∪ (a ∩ b⊥ ⊥ ))
9	8	df-c1 132	1 a C b⊥

Syntax hints:   C wc 3  ^⊥ wn 4   ∪ wo 6   ∩ wa 7

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

This theorem depends on definitions:  df-a 40  df-c1 132  df-c2 133

This theorem is referenced by:  wwfh2  217  wwfh3  218  wwfh4  219  comcom3  454  comcom4  455  comcom6  459  fh1  469  fh2  470  nbdi  486  oml4  487  gsth  489  gsth2  490  i3bi  496  df2i3  498  dfi3b  499  oi3ai3  503  i3lem2  505  comi31  508  com2i3  509  i3abs3  524  i3con  551  i3orlem7  558  i3orlem8  559  ud1lem1  560  ud1lem3  562  ud2lem3  565  ud3lem1a  566  ud3lem1b  567  ud3lem1c  568  ud3lem1d  569  ud3lem1  570  ud3lem2  571  ud3lem3d  575  ud3lem3  576  ud4lem1a  577  ud4lem1b  578  ud4lem1c  579  ud4lem1d  580  ud4lem1  581  ud4lem2  582  ud4lem3b  584  ud4lem3  585  ud5lem1a  586  ud5lem1b  587  ud5lem1  589  ud5lem3a  591  ud5lem3  594  u1lemaa  600  u4lemaa  603  u1lemab  610  u1lemanb  615  u3lemanb  617  u4lemoa  623  u4lemona  628  u3lemob  632  u4lemob  633  u3lemonb  637  u1lemc1  680  u4lemc1  683  u1lemc2  686  u2lemc2  687  u4lemc2  689  u5lemc2  690  u1lemc4  701  u3lemc4  703  u4lemc4  704  u5lemc4  705  u1lemle2  715  u1lembi  720  u5lembi  725  u4lem1  737  u1lem4  757  u4lem4  759  u4lem5  764  u5lem5  765  u4lem6  768  u5lem6  769  u1lem8  776  u1lem11  780  u3lem11  786  u3lem13a  789  u3lem13b  790  u3lem15  795  bi1o1a  798  test  802  test2  803  3vth5  808  3vded21  817  1oa  820  2oath1  826  neg3antlem2  865  elimcons  868  comanblem1  870  mhlem1  877  marsdenlem2  881  mlaconjolem  885  cancellem  891  e2ast2  894  govar  896  gomaex3lem1  914  gomaex3lem2  915  gomaex3lem3  916  oa23  936  lem4.6.2e1  1082  com3iia  1102