Proof of Theorem mndifsplit
Step | Hyp | Ref
| Expression |
1 | | pm2.21 119 |
. . . 4
⊢ (¬
(𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓) → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = (if(𝜑, 𝐴, 0 ) + if(𝜓, 𝐴, 0 )))) |
2 | 1 | imp 444 |
. . 3
⊢ ((¬
(𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜓)) → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = (if(𝜑, 𝐴, 0 ) + if(𝜓, 𝐴, 0 ))) |
3 | 2 | 3ad2antl3 1218 |
. 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 17135 |
. . . . 5
⊢ ((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵) → (𝐴 + 0 ) = 𝐴) |
8 | 7 | 3adant3 1074 |
. . . 4
⊢ ((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) → (𝐴 + 0 ) = 𝐴) |
9 | 8 | adantr 480 |
. . 3
⊢ (((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) ∧ (𝜑 ∧ ¬ 𝜓)) → (𝐴 + 0 ) = 𝐴) |
10 | | iftrue 4042 |
. . . . 5
⊢ (𝜑 → if(𝜑, 𝐴, 0 ) = 𝐴) |
11 | | iffalse 4045 |
. . . . 5
⊢ (¬
𝜓 → if(𝜓, 𝐴, 0 ) = 0 ) |
12 | 10, 11 | oveqan12d 6568 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝜓) → (if(𝜑, 𝐴, 0 ) + if(𝜓, 𝐴, 0 )) = (𝐴 + 0 )) |
13 | 12 | adantl 481 |
. . 3
⊢ (((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) ∧ (𝜑 ∧ ¬ 𝜓)) → (if(𝜑, 𝐴, 0 ) + if(𝜓, 𝐴, 0 )) = (𝐴 + 0 )) |
14 | | iftrue 4042 |
. . . . 5
⊢ ((𝜑 ∨ 𝜓) → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = 𝐴) |
15 | 14 | orcs 408 |
. . . 4
⊢ (𝜑 → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = 𝐴) |
16 | 15 | ad2antrl 760 |
. . 3
⊢ (((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) ∧ (𝜑 ∧ ¬ 𝜓)) → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = 𝐴) |
17 | 9, 13, 16 | 3eqtr4rd 2655 |
. 2
⊢ (((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) ∧ (𝜑 ∧ ¬ 𝜓)) → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = (if(𝜑, 𝐴, 0 ) + if(𝜓, 𝐴, 0 ))) |
18 | 4, 5, 6 | mndlid 17134 |
. . . . 5
⊢ ((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵) → ( 0 + 𝐴) = 𝐴) |
19 | 18 | 3adant3 1074 |
. . . 4
⊢ ((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) → ( 0 + 𝐴) = 𝐴) |
20 | 19 | adantr 480 |
. . 3
⊢ (((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) ∧ (¬ 𝜑 ∧ 𝜓)) → ( 0 + 𝐴) = 𝐴) |
21 | | iffalse 4045 |
. . . . 5
⊢ (¬
𝜑 → if(𝜑, 𝐴, 0 ) = 0 ) |
22 | | iftrue 4042 |
. . . . 5
⊢ (𝜓 → if(𝜓, 𝐴, 0 ) = 𝐴) |
23 | 21, 22 | oveqan12d 6568 |
. . . 4
⊢ ((¬
𝜑 ∧ 𝜓) → (if(𝜑, 𝐴, 0 ) + if(𝜓, 𝐴, 0 )) = ( 0 + 𝐴)) |
24 | 23 | adantl 481 |
. . 3
⊢ (((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) ∧ (¬ 𝜑 ∧ 𝜓)) → (if(𝜑, 𝐴, 0 ) + if(𝜓, 𝐴, 0 )) = ( 0 + 𝐴)) |
25 | 14 | olcs 409 |
. . . 4
⊢ (𝜓 → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = 𝐴) |
26 | 25 | ad2antll 761 |
. . 3
⊢ (((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) ∧ (¬ 𝜑 ∧ 𝜓)) → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = 𝐴) |
27 | 20, 24, 26 | 3eqtr4rd 2655 |
. 2
⊢ (((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) ∧ (¬ 𝜑 ∧ 𝜓)) → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = (if(𝜑, 𝐴, 0 ) + if(𝜓, 𝐴, 0 ))) |
28 | | simp1 1054 |
. . . . 5
⊢ ((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) → 𝑀 ∈ Mnd) |
29 | 4, 6 | mndidcl 17131 |
. . . . . 6
⊢ (𝑀 ∈ Mnd → 0 ∈ 𝐵) |
30 | 28, 29 | syl 17 |
. . . . 5
⊢ ((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) → 0 ∈ 𝐵) |
31 | 4, 5, 6 | mndlid 17134 |
. . . . 5
⊢ ((𝑀 ∈ Mnd ∧ 0 ∈ 𝐵) → ( 0 + 0 ) = 0 ) |
32 | 28, 30, 31 | syl2anc 691 |
. . . 4
⊢ ((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) → ( 0 + 0 ) = 0 ) |
33 | 32 | adantr 480 |
. . 3
⊢ (((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) ∧ (¬ 𝜑 ∧ ¬ 𝜓)) → ( 0 + 0 ) = 0 ) |
34 | 21, 11 | oveqan12d 6568 |
. . . 4
⊢ ((¬
𝜑 ∧ ¬ 𝜓) → (if(𝜑, 𝐴, 0 ) + if(𝜓, 𝐴, 0 )) = ( 0 + 0 )) |
35 | 34 | adantl 481 |
. . 3
⊢ (((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) ∧ (¬ 𝜑 ∧ ¬ 𝜓)) → (if(𝜑, 𝐴, 0 ) + if(𝜓, 𝐴, 0 )) = ( 0 + 0 )) |
36 | | ioran 510 |
. . . . 5
⊢ (¬
(𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓)) |
37 | | iffalse 4045 |
. . . . 5
⊢ (¬
(𝜑 ∨ 𝜓) → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = 0 ) |
38 | 36, 37 | sylbir 224 |
. . . 4
⊢ ((¬
𝜑 ∧ ¬ 𝜓) → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = 0 ) |
39 | 38 | adantl 481 |
. . 3
⊢ (((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) ∧ (¬ 𝜑 ∧ ¬ 𝜓)) → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = 0 ) |
40 | 33, 35, 39 | 3eqtr4rd 2655 |
. 2
⊢ (((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) ∧ (¬ 𝜑 ∧ ¬ 𝜓)) → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = (if(𝜑, 𝐴, 0 ) + if(𝜓, 𝐴, 0 ))) |
41 | 3, 17, 27, 40 | 4casesdan 988 |
1
⊢ ((𝑀 ∈ Mnd ∧ 𝐴 ∈ 𝐵 ∧ ¬ (𝜑 ∧ 𝜓)) → if((𝜑 ∨ 𝜓), 𝐴, 0 ) = (if(𝜑, 𝐴, 0 ) + if(𝜓, 𝐴, 0 ))) |