Theorem comcom 453

Description: Commutation is symmetric. Kalmbach 83 p. 22. (Contributed by NM, 27-Aug-1997.)

Hypothesis

Ref	Expression
comcom.1	a C b

Assertion

Ref	Expression
comcom	b C a

Proof of Theorem comcom

Step	Hyp	Ref	Expression
1		ax-a2 31	. . . . . . . . . 10 (a⊥ ∪ b) = (b ∪ a⊥ )
2	1	ran 78	. . . . . . . . 9 ((a⊥ ∪ b) ∩ b) = ((b ∪ a⊥ ) ∩ b)
3		ancom 74	. . . . . . . . 9 ((b ∪ a⊥ ) ∩ b) = (b ∩ (b ∪ a⊥ ))
4	2, 3	ax-r2 36	. . . . . . . 8 ((a⊥ ∪ b) ∩ b) = (b ∩ (b ∪ a⊥ ))
5		anabs 121	. . . . . . . 8 (b ∩ (b ∪ a⊥ )) = b
6	4, 5	ax-r2 36	. . . . . . 7 ((a⊥ ∪ b) ∩ b) = b
7	6	lan 77	. . . . . 6 ((a⊥ ∪ b⊥ ) ∩ ((a⊥ ∪ b) ∩ b)) = ((a⊥ ∪ b⊥ ) ∩ b)
8		comcom.1	. . . . . . . . . . . 12 a C b
9	8	df-c2 133	. . . . . . . . . . 11 a = ((a ∩ b) ∪ (a ∩ b⊥ ))
10		df-a 40	. . . . . . . . . . . 12 (a ∩ b) = (a⊥ ∪ b⊥ )⊥
11		anor1 88	. . . . . . . . . . . 12 (a ∩ b⊥ ) = (a⊥ ∪ b)⊥
12	10, 11	2or 72	. . . . . . . . . . 11 ((a ∩ b) ∪ (a ∩ b⊥ )) = ((a⊥ ∪ b⊥ )⊥ ∪ (a⊥ ∪ b)⊥ )
13	9, 12	ax-r2 36	. . . . . . . . . 10 a = ((a⊥ ∪ b⊥ )⊥ ∪ (a⊥ ∪ b)⊥ )
14	13	ax-r4 37	. . . . . . . . 9 a⊥ = ((a⊥ ∪ b⊥ )⊥ ∪ (a⊥ ∪ b)⊥ )⊥
15		df-a 40	. . . . . . . . . 10 ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b)) = ((a⊥ ∪ b⊥ )⊥ ∪ (a⊥ ∪ b)⊥ )⊥
16	15	ax-r1 35	. . . . . . . . 9 ((a⊥ ∪ b⊥ )⊥ ∪ (a⊥ ∪ b)⊥ )⊥ = ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b))
17	14, 16	ax-r2 36	. . . . . . . 8 a⊥ = ((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b))
18	17	ran 78	. . . . . . 7 (a⊥ ∩ b) = (((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b)) ∩ b)
19		anass 76	. . . . . . 7 (((a⊥ ∪ b⊥ ) ∩ (a⊥ ∪ b)) ∩ b) = ((a⊥ ∪ b⊥ ) ∩ ((a⊥ ∪ b) ∩ b))
20	18, 19	ax-r2 36	. . . . . 6 (a⊥ ∩ b) = ((a⊥ ∪ b⊥ ) ∩ ((a⊥ ∪ b) ∩ b))
21	10	con2 67	. . . . . . 7 (a ∩ b)⊥ = (a⊥ ∪ b⊥ )
22	21	ran 78	. . . . . 6 ((a ∩ b)⊥ ∩ b) = ((a⊥ ∪ b⊥ ) ∩ b)
23	7, 20, 22	3tr1 63	. . . . 5 (a⊥ ∩ b) = ((a ∩ b)⊥ ∩ b)
24	23	lor 70	. . . 4 ((a ∩ b) ∪ (a⊥ ∩ b)) = ((a ∩ b) ∪ ((a ∩ b)⊥ ∩ b))
25	24	ax-r1 35	. . 3 ((a ∩ b) ∪ ((a ∩ b)⊥ ∩ b)) = ((a ∩ b) ∪ (a⊥ ∩ b))
26		ax-a2 31	. . . . . 6 ((a ∩ b) ∪ b) = (b ∪ (a ∩ b))
27		ancom 74	. . . . . . . 8 (a ∩ b) = (b ∩ a)
28	27	lor 70	. . . . . . 7 (b ∪ (a ∩ b)) = (b ∪ (b ∩ a))
29		orabs 120	. . . . . . 7 (b ∪ (b ∩ a)) = b
30	28, 29	ax-r2 36	. . . . . 6 (b ∪ (a ∩ b)) = b
31	26, 30	ax-r2 36	. . . . 5 ((a ∩ b) ∪ b) = b
32	31	df-le1 130	. . . 4 (a ∩ b) ≤ b
33	32	oml2 451	. . 3 ((a ∩ b) ∪ ((a ∩ b)⊥ ∩ b)) = b
34		ancom 74	. . . 4 (a⊥ ∩ b) = (b ∩ a⊥ )
35	27, 34	2or 72	. . 3 ((a ∩ b) ∪ (a⊥ ∩ b)) = ((b ∩ a) ∪ (b ∩ a⊥ ))
36	25, 33, 35	3tr2 64	. 2 b = ((b ∩ a) ∪ (b ∩ a⊥ ))
37	36	df-c1 132	1 b C a

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

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-r3 439

This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is referenced by:  comcom3  454  com3ii  457  comor1  461  comorr2  463  comanr1  464  comanr2  465  fh2  470  com2or  483  nbdi  486  oml4  487  gsth  489  gsth2  490  gt1  492  i3bi  496  df2i3  498  i3lem1  504  comi31  508  lem4  511  i3abs3  524  i3con  551  ud1lem1  560  ud1lem3  562  ud2lem3  565  ud3lem1a  566  ud3lem1c  568  ud3lem3  576  ud4lem1a  577  ud4lem1b  578  ud4lem1c  579  ud4lem1  581  ud4lem3  585  ud5lem1a  586  ud5lem1  589  u4lemaa  603  u4lemana  608  u3lemab  612  u3lemanb  617  comi12  707  i1com  708  comi1  709  u4lemle2  718  u5lembi  725  u12lembi  726  u1lem1  734  u3lem1  736  u5lem1  738  u3lem2  746  u4lem2  747  u5lem2  748  u4lem4  759  u5lem5  765  u5lem6  769  u1lem8  776  u1lem11  780  u3lem13b  790  u3lem15  795  bi1o1a  798  test  802  3vcom  813  3vded21  817  3vded3  819  2oalem1  825  bi3  839  bi4  840  orbi  842  negantlem2  849  elimcons  868  comanblem1  870  mhlem  876  mhlem1  877  marsdenlem1  880  marsdenlem2  881  marsdenlem3  882  mh2  884  mlaconjolem  885  mhcor1  888  e2ast2  894  e2astlem1  895  govar  896  oau  929  oa23  936  oacom  1011  oacom3  1013  oa3moa3  1029  lem4.6.2e1  1082  lem4.6.6i1j3  1094