Proof of Theorem mndifsplit
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | pm2.21 123 | . . . 4
⊢ (¬
(𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓) → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = (if(𝜑, 𝐴, 0 ) + if(𝜓, 𝐴, 0 )))) | 
| 2 | 1 | imp 406 | . . 3
⊢ ((¬
(𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜓)) → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = (if(𝜑, 𝐴, 0 ) + if(𝜓, 𝐴, 0 ))) | 
| 3 | 2 | 3ad2antl3 1187 | . 2
⊢ (((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) ∧ (𝜑 ∧ 𝜓)) → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = (if(𝜑, 𝐴, 0 ) + if(𝜓, 𝐴, 0 ))) | 
| 4 |  | mndifsplit.b | . . . . . 6
⊢ 𝐵 = (Base‘𝑀) | 
| 5 |  | mndifsplit.pg | . . . . . 6
⊢  + =
(+g‘𝑀) | 
| 6 |  | mndifsplit.0g | . . . . . 6
⊢  0 =
(0g‘𝑀) | 
| 7 | 4, 5, 6 | mndrid 18769 | . . . . 5
⊢ ((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵) → (𝐴 + 0 ) = 𝐴) | 
| 8 | 7 | 3adant3 1132 | . . . 4
⊢ ((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) → (𝐴 + 0 ) = 𝐴) | 
| 9 | 8 | adantr 480 | . . 3
⊢ (((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) ∧ (𝜑 ∧ ¬ 𝜓)) → (𝐴 + 0 ) = 𝐴) | 
| 10 |  | iftrue 4530 | . . . . 5
⊢ (𝜑 → if(𝜑, 𝐴, 0 ) = 𝐴) | 
| 11 |  | iffalse 4533 | . . . . 5
⊢ (¬
𝜓 → if(𝜓, 𝐴, 0 ) = 0 ) | 
| 12 | 10, 11 | oveqan12d 7451 | . . . 4
⊢ ((𝜑 ∧ ¬ 𝜓) → (if(𝜑, 𝐴, 0 ) + if(𝜓, 𝐴, 0 )) = (𝐴 + 0 )) | 
| 13 | 12 | adantl 481 | . . 3
⊢ (((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) ∧ (𝜑 ∧ ¬ 𝜓)) → (if(𝜑, 𝐴, 0 ) + if(𝜓, 𝐴, 0 )) = (𝐴 + 0 )) | 
| 14 |  | iftrue 4530 | . . . . 5
⊢ ((𝜑 ∨ 𝜓) → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = 𝐴) | 
| 15 | 14 | orcs 875 | . . . 4
⊢ (𝜑 → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = 𝐴) | 
| 16 | 15 | ad2antrl 728 | . . 3
⊢ (((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) ∧ (𝜑 ∧ ¬ 𝜓)) → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = 𝐴) | 
| 17 | 9, 13, 16 | 3eqtr4rd 2787 | . 2
⊢ (((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) ∧ (𝜑 ∧ ¬ 𝜓)) → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = (if(𝜑, 𝐴, 0 ) + if(𝜓, 𝐴, 0 ))) | 
| 18 | 4, 5, 6 | mndlid 18768 | . . . . 5
⊢ ((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵) → ( 0 + 𝐴) = 𝐴) | 
| 19 | 18 | 3adant3 1132 | . . . 4
⊢ ((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) → ( 0 + 𝐴) = 𝐴) | 
| 20 | 19 | adantr 480 | . . 3
⊢ (((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) ∧ (¬ 𝜑 ∧ 𝜓)) → ( 0 + 𝐴) = 𝐴) | 
| 21 |  | iffalse 4533 | . . . . 5
⊢ (¬
𝜑 → if(𝜑, 𝐴, 0 ) = 0 ) | 
| 22 |  | iftrue 4530 | . . . . 5
⊢ (𝜓 → if(𝜓, 𝐴, 0 ) = 𝐴) | 
| 23 | 21, 22 | oveqan12d 7451 | . . . 4
⊢ ((¬
𝜑 ∧ 𝜓) → (if(𝜑, 𝐴, 0 ) + if(𝜓, 𝐴, 0 )) = ( 0 + 𝐴)) | 
| 24 | 23 | adantl 481 | . . 3
⊢ (((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) ∧ (¬ 𝜑 ∧ 𝜓)) → (if(𝜑, 𝐴, 0 ) + if(𝜓, 𝐴, 0 )) = ( 0 + 𝐴)) | 
| 25 | 14 | olcs 876 | . . . 4
⊢ (𝜓 → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = 𝐴) | 
| 26 | 25 | ad2antll 729 | . . 3
⊢ (((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) ∧ (¬ 𝜑 ∧ 𝜓)) → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = 𝐴) | 
| 27 | 20, 24, 26 | 3eqtr4rd 2787 | . 2
⊢ (((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) ∧ (¬ 𝜑 ∧ 𝜓)) → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = (if(𝜑, 𝐴, 0 ) + if(𝜓, 𝐴, 0 ))) | 
| 28 |  | simp1 1136 | . . . . 5
⊢ ((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) → 𝑀 ∈ Mnd) | 
| 29 | 4, 6 | mndidcl 18763 | . . . . 5
⊢ (𝑀 ∈ Mnd → 0 ∈ 𝐵) | 
| 30 | 4, 5, 6 | mndlid 18768 | . . . . 5
⊢ ((𝑀 ∈ Mnd ∧ 0 ∈ 𝐵) → ( 0 + 0 ) = 0 ) | 
| 31 | 28, 29, 30 | syl2anc2 585 | . . . 4
⊢ ((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) → ( 0 + 0 ) = 0 ) | 
| 32 | 31 | adantr 480 | . . 3
⊢ (((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) ∧ (¬ 𝜑 ∧ ¬ 𝜓)) → ( 0 + 0 ) = 0 ) | 
| 33 | 21, 11 | oveqan12d 7451 | . . . 4
⊢ ((¬
𝜑 ∧ ¬ 𝜓) → (if(𝜑, 𝐴, 0 ) + if(𝜓, 𝐴, 0 )) = ( 0 + 0 )) | 
| 34 | 33 | adantl 481 | . . 3
⊢ (((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) ∧ (¬ 𝜑 ∧ ¬ 𝜓)) → (if(𝜑, 𝐴, 0 ) + if(𝜓, 𝐴, 0 )) = ( 0 + 0 )) | 
| 35 |  | ioran 985 | . . . . 5
⊢ (¬
(𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓)) | 
| 36 |  | iffalse 4533 | . . . . 5
⊢ (¬
(𝜑 ∨ 𝜓) → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = 0 ) | 
| 37 | 35, 36 | sylbir 235 | . . . 4
⊢ ((¬
𝜑 ∧ ¬ 𝜓) → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = 0 ) | 
| 38 | 37 | adantl 481 | . . 3
⊢ (((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) ∧ (¬ 𝜑 ∧ ¬ 𝜓)) → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = 0 ) | 
| 39 | 32, 34, 38 | 3eqtr4rd 2787 | . 2
⊢ (((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) ∧ (¬ 𝜑 ∧ ¬ 𝜓)) → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = (if(𝜑, 𝐴, 0 ) + if(𝜓, 𝐴, 0 ))) | 
| 40 | 3, 17, 27, 39 | 4casesdan 1041 | 1
⊢ ((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = (if(𝜑, 𝐴, 0 ) + if(𝜓, 𝐴, 0 ))) |