Theorem comcom5 440

Description: Commutation equivalence. Kalmbach 83 p. 23.

Hypothesis

Ref	Expression
comcom5.1	a⊥ C b⊥

Assertion

Ref	Expression
comcom5	a C b

Proof of Theorem comcom5

Step	Hyp	Ref	Expression
1		comcom5.1	. . . . 5 a⊥ C b⊥
2	1	comcom4 437	. . . 4 a⊥ ⊥ C b⊥ ⊥
3	2	df-c2 125	. . 3 a⊥ ⊥ = ((a⊥ ⊥ ∩ b⊥ ⊥ ) ∪ (a⊥ ⊥ ∩ b⊥ ⊥ ⊥ ))
4		ax-a1 29	. . 3 a = a⊥ ⊥
5		ax-a1 29	. . . . 5 b = b⊥ ⊥
6	4, 5	2an 72	. . . 4 (a ∩ b) = (a⊥ ⊥ ∩ b⊥ ⊥ )
7		ax-a1 29	. . . . 5 b⊥ = b⊥ ⊥ ⊥
8	4, 7	2an 72	. . . 4 (a ∩ b⊥ ) = (a⊥ ⊥ ∩ b⊥ ⊥ ⊥ )
9	6, 8	2or 67	. . 3 ((a ∩ b) ∪ (a ∩ b⊥ )) = ((a⊥ ⊥ ∩ b⊥ ⊥ ) ∪ (a⊥ ⊥ ∩ b⊥ ⊥ ⊥ ))
10	3, 4, 9	3tr1 60	. 2 a = ((a ∩ b) ∪ (a ∩ b⊥ ))
11	10	df-c1 124	1 a C b

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

This theorem is referenced by:  comcom6 441  comcom7 442  comdr 448  df2c1 450  com2an 466  oml4 469  gstho 473  df2i3 480  i3lem2 487  comi31 490  ud1lem1 542  ud1lem3 544  ud4lem1a 559  ud4lem1b 560  ud4lem1c 561  ud4lem1d 562  ud4lem1 563  ud5lem1a 568

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

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org