P. 265 of Theorem List - Metamath Proof Explorer

Type

Label

Description

Statement

Theorem

ex-natded5.8 26401

Theorem 5.8 of [Clemente] p. 20, translated line by line using the usual translation of natural deduction (ND) in the Metamath Proof Explorer (MPE) notation. For information about ND and Metamath, see the page on Deduction Form and Natural Deduction in Metamath Proof Explorer. The original proof, which uses Fitch style, was written as follows (the leading "..." shows an embedded ND hypothesis, beginning with the initial assumption of the ND hypothesis):

#	MPE#	ND Expression	MPE Translation	ND Rationale	MPE Rationale
1	10;11	((𝜓 ∧ 𝜒) → ¬ 𝜃)	(𝜑 → ((𝜓 ∧ 𝜒) → ¬ 𝜃))	Given	$e; adantr 479 to move it into the ND hypothesis
2	3;4	(𝜏 → 𝜃)	(𝜑 → (𝜏 → 𝜃))	Given	$e; adantr 479 to move it into the ND hypothesis
3	7;8	𝜒	(𝜑 → 𝜒)	Given	$e; adantr 479 to move it into the ND hypothesis
4	1;2	𝜏	(𝜑 → 𝜏)	Given	$e. adantr 479 to move it into the ND hypothesis
5	6	...| 𝜓	((𝜑 ∧ 𝜓) → 𝜓)	ND Hypothesis/Assumption	simpr 475. New ND hypothesis scope, each reference outside the scope must change antecedent 𝜑 to (𝜑 ∧ 𝜓).
6	9	... (𝜓 ∧ 𝜒)	((𝜑 ∧ 𝜓) → (𝜓 ∧ 𝜒))	∧I 5,3	jca 552 (∧I), 6,8 (adantr 479 to bring in scope)
7	5	... ¬ 𝜃	((𝜑 ∧ 𝜓) → ¬ 𝜃)	→E 1,6	mpd 15 (→E), 2,4
8	12	... 𝜃	((𝜑 ∧ 𝜓) → 𝜃)	→E 2,4	mpd 15 (→E), 9,11; note the contradiction with ND line 7 (MPE line 5)
9	13	¬ 𝜓	(𝜑 → ¬ 𝜓)	¬I 5,7,8	pm2.65da 597 (¬I), 5,12; proof by contradiction. MPE step 6 (ND#5) does not need a reference here, because the assumption is embedded in the antecedents

The original used Latin letters; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including 𝜑 and uses the Metamath equivalents of the natural deduction rules. To add an assumption, the antecedent is modified to include it (typically by using adantr 479; simpr 475 is useful when you want to depend directly on the new assumption). Below is the final metamath proof (which reorders some steps).

A much more efficient proof, using more of Metamath and MPE's capabilities, is shown in ex-natded5.8-2 26402.

(Contributed by Mario Carneiro, 9-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → ((𝜓 ∧ 𝜒) → ¬ 𝜃))    &   ⊢ (𝜑 → (𝜏 → 𝜃))    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜏)    ⇒   ⊢ (𝜑 → ¬ 𝜓)

Theorem

ex-natded5.8-2 26402

A more efficient proof of Theorem 5.8 of [Clemente] p. 20. For a longer line-by-line translation, see ex-natded5.8 26401. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → ((𝜓 ∧ 𝜒) → ¬ 𝜃))    &   ⊢ (𝜑 → (𝜏 → 𝜃))    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜏)    ⇒   ⊢ (𝜑 → ¬ 𝜓)

Theorem

ex-natded5.13 26403

Theorem 5.13 of [Clemente] p. 20, translated line by line using the interpretation of natural deduction in Metamath. For information about ND and Metamath, see the page on Deduction Form and Natural Deduction in Metamath Proof Explorer. A much more efficient proof, using more of Metamath and MPE's capabilities, is shown in ex-natded5.13-2 26404. The original proof, which uses Fitch style, was written as follows (the leading "..." shows an embedded ND hypothesis, beginning with the initial assumption of the ND hypothesis):

#	MPE#	ND Expression	MPE Translation	ND Rationale	MPE Rationale
1	15	(𝜓 ∨ 𝜒)	(𝜑 → (𝜓 ∨ 𝜒))	Given	$e.
2;3	2	(𝜓 → 𝜃)	(𝜑 → (𝜓 → 𝜃))	Given	$e. adantr 479 to move it into the ND hypothesis
3	9	(¬ 𝜏 → ¬ 𝜒)	(𝜑 → (¬ 𝜏 → ¬ 𝜒))	Given	$e. ad2antrr 757 to move it into the ND sub-hypothesis
4	1	...| 𝜓	((𝜑 ∧ 𝜓) → 𝜓)	ND hypothesis assumption	simpr 475
5	4	... 𝜃	((𝜑 ∧ 𝜓) → 𝜃)	→E 2,4	mpd 15 1,3
6	5	... (𝜃 ∨ 𝜏)	((𝜑 ∧ 𝜓) → (𝜃 ∨ 𝜏))	∨I 5	orcd 405 4
7	6	...| 𝜒	((𝜑 ∧ 𝜒) → 𝜒)	ND hypothesis assumption	simpr 475
8	8	... ...| ¬ 𝜏	(((𝜑 ∧ 𝜒) ∧ ¬ 𝜏) → ¬ 𝜏)	(sub) ND hypothesis assumption	simpr 475
9	11	... ... ¬ 𝜒	(((𝜑 ∧ 𝜒) ∧ ¬ 𝜏) → ¬ 𝜒)	→E 3,8	mpd 15 8,10
10	7	... ... 𝜒	(((𝜑 ∧ 𝜒) ∧ ¬ 𝜏) → 𝜒)	IT 7	adantr 479 6
11	12	... ¬ ¬ 𝜏	((𝜑 ∧ 𝜒) → ¬ ¬ 𝜏)	¬I 8,9,10	pm2.65da 597 7,11
12	13	... 𝜏	((𝜑 ∧ 𝜒) → 𝜏)	¬E 11	notnotrd 126 12
13	14	... (𝜃 ∨ 𝜏)	((𝜑 ∧ 𝜒) → (𝜃 ∨ 𝜏))	∨I 12	olcd 406 13
14	16	(𝜃 ∨ 𝜏)	(𝜑 → (𝜃 ∨ 𝜏))	∨E 1,6,13	mpjaodan 822 5,14,15

The original used Latin letters; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including 𝜑 and uses the Metamath equivalents of the natural deduction rules. To add an assumption, the antecedent is modified to include it (typically by using adantr 479; simpr 475 is useful when you want to depend directly on the new assumption). (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → (𝜓 ∨ 𝜒))    &   ⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ (𝜑 → (¬ 𝜏 → ¬ 𝜒))    ⇒   ⊢ (𝜑 → (𝜃 ∨ 𝜏))

Theorem

ex-natded5.13-2 26404

A more efficient proof of Theorem 5.13 of [Clemente] p. 20. Compare with ex-natded5.13 26403. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → (𝜓 ∨ 𝜒))    &   ⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ (𝜑 → (¬ 𝜏 → ¬ 𝜒))    ⇒   ⊢ (𝜑 → (𝜃 ∨ 𝜏))

Theorem

ex-natded9.20 26405

Theorem 9.20 of [Clemente] p. 43, translated line by line using the usual translation of natural deduction (ND) in the Metamath Proof Explorer (MPE) notation. For information about ND and Metamath, see the page on Deduction Form and Natural Deduction in Metamath Proof Explorer. The original proof, which uses Fitch style, was written as follows (the leading "..." shows an embedded ND hypothesis, beginning with the initial assumption of the ND hypothesis):

#	MPE#	ND Expression	MPE Translation	ND Rationale	MPE Rationale
1	1	(𝜓 ∧ (𝜒 ∨ 𝜃))	(𝜑 → (𝜓 ∧ (𝜒 ∨ 𝜃)))	Given	$e
2	2	𝜓	(𝜑 → 𝜓)	∧EL 1	simpld 473 1
3	11	(𝜒 ∨ 𝜃)	(𝜑 → (𝜒 ∨ 𝜃))	∧ER 1	simprd 477 1
4	4	...| 𝜒	((𝜑 ∧ 𝜒) → 𝜒)	ND hypothesis assumption	simpr 475
5	5	... (𝜓 ∧ 𝜒)	((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒))	∧I 2,4	jca 552 3,4
6	6	... ((𝜓 ∧ 𝜒) ∨ (𝜓 ∧ 𝜃))	((𝜑 ∧ 𝜒) → ((𝜓 ∧ 𝜒) ∨ (𝜓 ∧ 𝜃)))	∨IR 5	orcd 405 5
7	8	...| 𝜃	((𝜑 ∧ 𝜃) → 𝜃)	ND hypothesis assumption	simpr 475
8	9	... (𝜓 ∧ 𝜃)	((𝜑 ∧ 𝜃) → (𝜓 ∧ 𝜃))	∧I 2,7	jca 552 7,8
9	10	... ((𝜓 ∧ 𝜒) ∨ (𝜓 ∧ 𝜃))	((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜒) ∨ (𝜓 ∧ 𝜃)))	∨IL 8	olcd 406 9
10	12	((𝜓 ∧ 𝜒) ∨ (𝜓 ∧ 𝜃))	(𝜑 → ((𝜓 ∧ 𝜒) ∨ (𝜓 ∧ 𝜃)))	∨E 3,6,9	mpjaodan 822 6,10,11

The original used Latin letters; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including 𝜑 and uses the Metamath equivalents of the natural deduction rules. To add an assumption, the antecedent is modified to include it (typically by using adantr 479; simpr 475 is useful when you want to depend directly on the new assumption). Below is the final metamath proof (which reorders some steps).

A much more efficient proof is ex-natded9.20-2 26406. (Contributed by David A. Wheeler, 19-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → (𝜓 ∧ (𝜒 ∨ 𝜃)))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∨ (𝜓 ∧ 𝜃)))

Theorem

ex-natded9.20-2 26406

A more efficient proof of Theorem 9.20 of [Clemente] p. 45. Compare with ex-natded9.20 26405. (Contributed by David A. Wheeler, 19-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → (𝜓 ∧ (𝜒 ∨ 𝜃)))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∨ (𝜓 ∧ 𝜃)))

Theorem

ex-natded9.26 26407*

Theorem 9.26 of [Clemente] p. 45, translated line by line using an interpretation of natural deduction in Metamath. This proof has some additional complications due to the fact that Metamath's existential elimination rule does not change bound variables, so we need to verify that 𝑥 is bound in the conclusion. For information about ND and Metamath, see the page on Deduction Form and Natural Deduction in Metamath Proof Explorer. The original proof, which uses Fitch style, was written as follows (the leading "..." shows an embedded ND hypothesis, beginning with the initial assumption of the ND hypothesis):

#	MPE#	ND Expression	MPE Translation	ND Rationale	MPE Rationale
1	3	∃𝑥∀𝑦𝜓(𝑥, 𝑦)	(𝜑 → ∃𝑥∀𝑦𝜓)	Given	$e.
2	6	...| ∀𝑦𝜓(𝑥, 𝑦)	((𝜑 ∧ ∀𝑦𝜓) → ∀𝑦𝜓)	ND hypothesis assumption	simpr 475. Later statements will have this scope.
3	7;5,4	... 𝜓(𝑥, 𝑦)	((𝜑 ∧ ∀𝑦𝜓) → 𝜓)	∀E 2,y	spsbcd 3320 (∀E), 5,6. To use it we need a1i 11 and vex 3080. This could be immediately done with 19.21bi 2000, but we want to show the general approach for substitution.
4	12;8,9,10,11	... ∃𝑥𝜓(𝑥, 𝑦)	((𝜑 ∧ ∀𝑦𝜓) → ∃𝑥𝜓)	∃I 3,a	spesbcd 3392 (∃I), 11. To use it we need sylibr 222, which in turn requires sylib 206 and two uses of sbcid 3323. This could be more immediately done using 19.8a 1988, but we want to show the general approach for substitution.
5	13;1,2	∃𝑥𝜓(𝑥, 𝑦)	(𝜑 → ∃𝑥𝜓)	∃E 1,2,4,a	exlimdd 2121 (∃E), 1,2,3,12. We'll need supporting assertions that the variable is free (not bound), as provided in nfv 1796 and nfe1 1969 (MPE# 1,2)
6	14	∀𝑦∃𝑥𝜓(𝑥, 𝑦)	(𝜑 → ∀𝑦∃𝑥𝜓)	∀I 5	alrimiv 1808 (∀I), 13

The original used Latin letters for predicates; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including 𝜑 and uses the Metamath equivalents of the natural deduction rules. Below is the final metamath proof (which reorders some steps).

Note that in the original proof, 𝜓(𝑥, 𝑦) has explicit parameters. In Metamath, these parameters are always implicit, and the parameters upon which a wff variable can depend are recorded in the "allowed substitution hints" below.

A much more efficient proof, using more of Metamath and MPE's capabilities, is shown in ex-natded9.26-2 26408.

(Contributed by Mario Carneiro, 9-Feb-2017.) (Revised by David A. Wheeler, 18-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → ∃𝑥∀𝑦𝜓)    ⇒   ⊢ (𝜑 → ∀𝑦∃𝑥𝜓)

Theorem

ex-natded9.26-2 26408*

A more efficient proof of Theorem 9.26 of [Clemente] p. 45. Compare with ex-natded9.26 26407. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → ∃𝑥∀𝑦𝜓)    ⇒   ⊢ (𝜑 → ∀𝑦∃𝑥𝜓)

17.1.4  Definitional examples

Theorem

ex-or 26409

Example for df-or 383. Example by David A. Wheeler. (Contributed by Mario Carneiro, 9-May-2015.)

⊢ (2 = 3 ∨ 4 = 4)

Theorem

ex-an 26410

Example for df-an 384. Example by David A. Wheeler. (Contributed by Mario Carneiro, 9-May-2015.)

⊢ (2 = 2 ∧ 3 = 3)

Theorem

ex-dif 26411

Example for df-dif 3447. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.)

⊢ ({1, 3} ∖ {1, 8}) = {3}

Theorem

ex-un 26412

Example for df-un 3449. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.)

⊢ ({1, 3} ∪ {1, 8}) = {1, 3, 8}

Theorem

ex-in 26413

Example for df-in 3451. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.)

⊢ ({1, 3} ∩ {1, 8}) = {1}

Theorem

ex-uni 26414

Example for df-uni 4271. Example by David A. Wheeler. (Contributed by Mario Carneiro, 2-Jul-2016.)

⊢ ∪ {{1, 3}, {1, 8}} = {1, 3, 8}

Theorem

ex-ss 26415

Example for df-ss 3458. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.)

⊢ {1, 2} ⊆ {1, 2, 3}

Theorem

ex-pss 26416

Example for df-pss 3460. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.)

⊢ {1, 2} ⊊ {1, 2, 3}

Theorem

ex-pw 26417

Example for df-pw 4013. Example by David A. Wheeler. (Contributed by Mario Carneiro, 2-Jul-2016.)

⊢ (𝐴 = {3, 5, 7} → 𝒫 𝐴 = (({∅} ∪ {{3}, {5}, {7}}) ∪ ({{3, 5}, {3, 7}, {5, 7}} ∪ {{3, 5, 7}})))

Theorem

ex-pr 26418

Example for df-pr 4031. (Contributed by Mario Carneiro, 7-May-2015.)

⊢ (𝐴 ∈ {1, -1} → (𝐴↑2) = 1)

Theorem

ex-br 26419

Example for df-br 4482. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.)

⊢ (𝑅 = {⟨2, 6⟩, ⟨3, 9⟩} → 3𝑅9)

Theorem

ex-opab 26420*

Example for df-opab 4542. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.)

⊢ (𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (𝑥 + 1) = 𝑦)} → 3𝑅4)

Theorem

ex-eprel 26421

Example for df-eprel 4843. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.)

⊢ 5 E {1, 5}

Theorem

ex-id 26422

Example for df-id 4847. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.)

⊢ (5 I 5 ∧ ¬ 4 I 5)

Theorem

ex-po 26423

Example for df-po 4853. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.)

⊢ ( < Po ℝ ∧ ¬ ≤ Po ℝ)

Theorem

ex-xp 26424

Example for df-xp 4938. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.)

⊢ ({1, 5} × {2, 7}) = ({⟨1, 2⟩, ⟨1, 7⟩} ∪ {⟨5, 2⟩, ⟨5, 7⟩})

Theorem

ex-cnv 26425

Example for df-cnv 4940. Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015.)

⊢ ^◡{⟨2, 6⟩, ⟨3, 9⟩} = {⟨6, 2⟩, ⟨9, 3⟩}

Theorem

ex-co 26426

Example for df-co 4941. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.)

⊢ ((exp ∘ cos)‘0) = e

Theorem

ex-dm 26427

Example for df-dm 4942. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.)

⊢ (𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → dom 𝐹 = {2, 3})

Theorem

ex-rn 26428

Example for df-rn 4943. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.)

⊢ (𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → ran 𝐹 = {6, 9})

Theorem

ex-res 26429

Example for df-res 4944. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.)

⊢ ((𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} ∧ 𝐵 = {1, 2}) → (𝐹 ↾ 𝐵) = {⟨2, 6⟩})

Theorem

ex-ima 26430

Example for df-ima 4945. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.)

⊢ ((𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} ∧ 𝐵 = {1, 2}) → (𝐹 “ 𝐵) = {6})

Theorem

ex-fv 26431

Example for df-fv 5697. Example by David A. Wheeler. (Contributed by Mario Carneiro, 7-May-2015.)

⊢ (𝐹 = {⟨2, 6⟩, ⟨3, 9⟩} → (𝐹‘3) = 9)

Theorem

ex-1st 26432

Example for df-1st 6933. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.)

⊢ (1^st ‘⟨3, 4⟩) = 3

Theorem

ex-2nd 26433

Example for df-2nd 6934. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.)

⊢ (2^nd ‘⟨3, 4⟩) = 4

Theorem

1kp2ke3k 26434

Example for df-dec 11233, 1000 + 2000 = 3000.

This proof disproves (by counterexample) the assertion of Hao Wang, who stated, "There is a theorem in the primitive notation of set theory that corresponds to the arithmetic theorem 1000 + 2000 = 3000. The formula would be forbiddingly long... even if (one) knows the definitions and is asked to simplify the long formula according to them, chances are he will make errors and arrive at some incorrect result." (Hao Wang, "Theory and practice in mathematics" , In Thomas Tymoczko, editor, New Directions in the Philosophy of Mathematics, pp 129-152, Birkauser Boston, Inc., Boston, 1986. (QA8.6.N48). The quote itself is on page 140.)

This is noted in Metamath: A Computer Language for Pure Mathematics by Norman Megill (2007) section 1.1.3. Megill then states, "A number of writers have conveyed the impression that the kind of absolute rigor provided by Metamath is an impossible dream, suggesting that a complete, formal verification of a typical theorem would take millions of steps in untold volumes of books... These writers assume, however, that in order to achieve the kind of complete formal verification they desire one must break down a proof into individual primitive steps that make direct reference to the axioms. This is not necessary. There is no reason not to make use of previously proved theorems rather than proving them over and over... A hierarchy of theorems and definitions permits an exponential growth in the formula sizes and primitive proof steps to be described with only a linear growth in the number of symbols used. Of course, this is how ordinary informal mathematics is normally done anyway, but with Metamath it can be done with absolute rigor and precision."

The proof here starts with (2 + 1) = 3, commutes it, and repeatedly multiplies both sides by ten. This is certainly longer than traditional mathematical proofs, e.g., there are a number of steps explicitly shown here to show that we're allowed to do operations such as multiplication. However, while longer, the proof is clearly a manageable size - even though every step is rigorously derived all the way back to the primitive notions of set theory and logic. And while there's a risk of making errors, the many independent verifiers make it much less likely that an incorrect result will be accepted.

This proof heavily relies on the decimal constructor df-dec 11233 developed by Mario Carneiro in 2015. The underlying Metamath language has an intentionally very small set of primitives; it doesn't even have a built-in construct for numbers. Instead, the digits are defined using these primitives, and the decimal constructor is used to make it easy to express larger numbers as combinations of digits.

(Contributed by David A. Wheeler, 29-Jun-2016.) (Shortened by Mario Carneiro using the arithmetic algorithm in mmj2, 30-Jun-2016.)

⊢ (;;;1000 + ;;;2000) = ;;;3000

Theorem

ex-fl 26435

Example for df-fl 12322. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.)

⊢ ((⌊‘(3 / 2)) = 1 ∧ (⌊‘-(3 / 2)) = -2)

Theorem

ex-ceil 26436

Example for df-ceil 12323. (Contributed by AV, 4-Sep-2021.)

⊢ ((⌈‘(3 / 2)) = 2 ∧ (⌈‘-(3 / 2)) = -1)

Theorem

ex-mod 26437

Example for df-mod 12398. (Contributed by AV, 3-Sep-2021.)

⊢ ((5 mod 3) = 2 ∧ (-7 mod 2) = 1)

Theorem

ex-exp 26438

Example for df-exp 12590. (Contributed by AV, 4-Sep-2021.)

⊢ ((5↑2) = ;25 ∧ (-3↑-2) = (1 / 9))

Theorem

ex-fac 26439

Example for df-fac 12790. (Contributed by AV, 4-Sep-2021.)

⊢ (!‘5) = ;;120

Theorem

ex-bc 26440

Example for df-bc 12819. (Contributed by AV, 4-Sep-2021.)

⊢ (5C3) = ;10

Theorem

ex-hash 26441

Example for df-hash 12847. (Contributed by AV, 4-Sep-2021.)

⊢ (#‘{0, 1, 2}) = 3

Theorem

ex-sqrt 26442

Example for df-sqrt 13680. (Contributed by AV, 4-Sep-2021.)

⊢ (√‘;25) = 5

Theorem

ex-abs 26443

Example for df-abs 13681. (Contributed by AV, 4-Sep-2021.)

⊢ (abs‘-2) = 2

Theorem

ex-dvds 26444

Example for df-dvds 14689: 3 divides into 6. (Contributed by David A. Wheeler, 19-May-2015.)

⊢ 3 ∥ 6

Theorem

ex-gcd 26445

Example for df-gcd 14926. (Contributed by AV, 5-Sep-2021.)

⊢ (-6 gcd 9) = 3

Theorem

ex-lcm 26446

Example for df-lcm 15015. (Contributed by AV, 5-Sep-2021.)

⊢ (6 lcm 9) = ;18

Theorem

ex-prmo 26447

Example for df-prmo 15456: (#_p‘10) = 2 · 3 · 5 · 7. (Contributed by AV, 6-Sep-2021.)

⊢ (#_p‘;10) = ;;210

17.1.5  Other examples

Theorem

aevdemo 26448*

Proof illustrating the comment of aev2 1934. (Contributed by BJ, 30-Mar-2021.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (∀𝑥 𝑥 = 𝑦 → ((∃𝑎∀𝑏 𝑐 = 𝑑 ∨ ∃𝑒 𝑓 = 𝑔) ∧ ∀ℎ(𝑖 = 𝑗 → 𝑘 = 𝑙)))

Theorem

ex-ind-dvds 26449

Example of a proof by induction (divisibility result). (Contributed by Stanislas Polu, 9-Mar-2020.) (Revised by BJ, 24-Mar-2020.)

⊢ (𝑁 ∈ ℕ₀ → 3 ∥ ((4↑𝑁) + 2))

17.2  Humor

17.2.1  April Fool's theorem

Theorem

avril1 26450

Poisson d'Avril's Theorem. This theorem is noted for its Selbstdokumentieren property, which means, literally, "self-documenting" and recalls the principle of quidquid german dictum sit, altum viditur, often used in set theory. Starting with the seemingly simple yet profound fact that any object 𝑥 equals itself (proved by Tarski in 1965; see Lemma 6 of [Tarski] p. 68), we demonstrate that the power set of the real numbers, as a relation on the value of the imaginary unit, does not conjoin with an empty relation on the product of the additive and multiplicative identity elements, leading to this startling conclusion that has left even seasoned professional mathematicians scratching their heads. (Contributed by Prof. Loof Lirpa, 1-Apr-2005.) (Proof modification is discouraged.) (New usage is discouraged.)

A reply to skeptics can be found at mmnotes.txt, under the 1-Apr-2006 entry.

⊢ ¬ (𝐴𝒫 ℝ(i‘1) ∧ 𝐹∅(0 · 1))

Theorem

2bornot2b 26451

The law of excluded middle. Act III, Theorem 1 of Shakespeare, Hamlet, Prince of Denmark (1602). Its author leaves its proof as an exercise for the reader - "To be, or not to be: that is the question" - starting a trend that has become standard in modern-day textbooks, serving to make the frustrated reader feel inferior, or in some cases to mask the fact that the author does not know its solution. (Contributed by Prof. Loof Lirpa, 1-Apr-2006.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (2 · 𝐵 ∨ ¬ 2 · 𝐵)

Theorem

helloworld 26452

The classic "Hello world" benchmark has been translated into 314 computer programming languages - see http://www.roesler-ac.de/wolfram/hello.htm. However, for many years it eluded a proof that it is more than just a conjecture, even though a wily mathematician once claimed, "I have discovered a truly marvelous proof of this, which this margin is too narrow to contain." Using an IBM 709 mainframe, a team of mathematicians led by Prof. Loof Lirpa, at the New College of Tahiti, were finally able put it rest with a remarkably short proof only 4 lines long. (Contributed by Prof. Loof Lirpa, 1-Apr-2007.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ¬ (ℎ ∈ (𝐿𝐿0) ∧ 𝑊∅(R1𝑑))

Theorem

1p1e2apr1 26453

One plus one equals two. Using proof-shortening techniques pioneered by Mr. Mel L. O'Cat, along with the latest supercomputer technology, Prof. Loof Lirpa and colleagues were able to shorten Whitehead and Russell's 360-page proof that 1+1=2 in Principia Mathematica to this remarkable proof only two steps long, thus establishing a new world's record for this famous theorem. (Contributed by Prof. Loof Lirpa, 1-Apr-2008.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (1 + 1) = 2

Theorem

eqid1 26454

Law of identity (reflexivity of class equality). Theorem 6.4 of [Quine] p. 41.

This law is thought to have originated with Aristotle (Metaphysics, Book VII, Part 17). It is one of the three axioms of Ayn Rand's philosophy (Atlas Shrugged, Part Three, Chapter VII). While some have proposed extending Rand's axiomatization to include Compassion and Kindness, others fear that such an extension may flirt with logical inconsistency. (Contributed by Stefan Allan, 1-Apr-2009.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ 𝐴 = 𝐴

Theorem

1div0apr 26455

Division by zero is forbidden! If we try, we encounter the DO NOT ENTER sign, which in mathematics means it is foolhardy to venture any further, possibly putting the underlying fabric of reality at risk. Based on a dare by David A. Wheeler. (Contributed by Mario Carneiro, 1-Apr-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (1 / 0) = ∅

Theorem

topnfbey 26456

Nothing seems to be impossible to Prof. Lirpa. After years of intensive research, he managed to find a proof that when given a chance to reach infinity, one could indeed go beyond, thus giving formal soundness to Buzz Lightyear's motto "To infinity... and beyond!" (Contributed by Prof. Loof Lirpa, 1-Apr-2020.) (Modified by Thierry Arnoux, 2-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝐵 ∈ (0...+∞) → +∞ < 𝐵)

17.3  (Future - to be reviewed and classified)

17.3.1  Planar incidence geometry

Syntax

cplig 26457

Extend class notation with the class of all planar incidence geometries.

class Plig

Definition

df-plig 26458*

Define the class of planar incidence geometries. We use Hilbert's axioms and adapt them to planar geometry. We use ∈ for the incidence relation. We could have used a generic binary relation, but using ∈ allows us to reuse previous results. Much of what follows is directly borrowed from Aitken, Incidence-Betweenness Geometry, 2008, http://public.csusm.edu/aitken_html/m410/betweenness.08.pdf.

The class Plig is the class of planar incidence geometries, where a planar incidence geometry 𝑥 is defined as a set of lines 𝑙 satisfying three axioms. In the definition below, ∪ 𝑥 is the union of lines, that is, the plane, and 𝑎, 𝑏, 𝑐 denote points. Therefore, the axioms are: for all pairs of (distinct) points, there exists a unique line containing them; all lines contain at least two points; there exist three non-collinear points.

(Contributed by FL, 2-Aug-2009.)

⊢ Plig = {𝑥 ∣ (∀𝑎 ∈ ∪ 𝑥∀𝑏 ∈ ∪ 𝑥(𝑎 ≠ 𝑏 → ∃!𝑙 ∈ 𝑥 (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙)) ∧ ∀𝑙 ∈ 𝑥 ∃𝑎 ∈ ∪ 𝑥∃𝑏 ∈ ∪ 𝑥(𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙) ∧ ∃𝑎 ∈ ∪ 𝑥∃𝑏 ∈ ∪ 𝑥∃𝑐 ∈ ∪ 𝑥∀𝑙 ∈ 𝑥 ¬ (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙))}

Theorem

isplig 26459*

The predicate "is a planar incidence geometry". (Contributed by FL, 2-Aug-2009.)

⊢ 𝑃 = ∪ 𝐿    ⇒   ⊢ (𝐿 ∈ 𝐴 → (𝐿 ∈ Plig ↔ (∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 → ∃!𝑙 ∈ 𝐿 (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙)) ∧ ∀𝑙 ∈ 𝐿 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 (𝑎 ≠ 𝑏 ∧ 𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙) ∧ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∀𝑙 ∈ 𝐿 ¬ (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙))))

Theorem

tncp 26460*

In any planar incidence geometry, there exist three non-collinear points. (Contributed by FL, 3-Aug-2009.)

⊢ 𝑃 = ∪ 𝐿    ⇒   ⊢ (𝐿 ∈ Plig → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∀𝑙 ∈ 𝐿 ¬ (𝑎 ∈ 𝑙 ∧ 𝑏 ∈ 𝑙 ∧ 𝑐 ∈ 𝑙))

Theorem

lpni 26461*

For any line in a planar incidence geometry, there exists a point not on the line. (Contributed by Jeff Hankins, 15-Aug-2009.)

⊢ 𝑃 = ∪ 𝐺    ⇒   ⊢ ((𝐺 ∈ Plig ∧ 𝐿 ∈ 𝐺) → ∃𝑎 ∈ 𝑃 𝑎 ∉ 𝐿)

17.3.2  Algebra preliminaries

Syntax

crpm 26462

Ring primes.

class RPrime

Definition

df-rprm 26463*

Define the set of prime elements in a ring. A prime element is a nonzero non-unit that satisfies an equivalent of Euclid's lemma euclemma 15137. (Contributed by Mario Carneiro, 17-Feb-2015.)

⊢ RPrime = (𝑤 ∈ V ↦ ⦋(Base‘𝑤) / 𝑏⦌{𝑝 ∈ (𝑏 ∖ ((Unit‘𝑤) ∪ {(0_g‘𝑤)})) ∣ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 [(∥_r‘𝑤) / 𝑑](𝑝𝑑(𝑥(._r‘𝑤)𝑦) → (𝑝𝑑𝑥 ∨ 𝑝𝑑𝑦))})

17.3.3  Aliases kept to prevent broken links

A few aliases that we temporarily keep to prevent broken links. If you land on any of these, please let the originating site and/or us know that the link that made you land here should be changed.

Theorem

dummylink 26464

Alias for a1ii 1 that may be referenced in some older works, and kept here to prevent broken links.

If you landed here, please let the originating site and/or us know that the link that made you land here should be changed to a link to a1ii 1.

(Contributed by NM, 7-Feb-2006.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ 𝜑    &   ⊢ 𝜓    ⇒   ⊢ 𝜑

Theorem

id1 26465

Alias for idALT 23 that may be referenced in some older works, and kept here to prevent broken links.

If you landed here, please let the originating site and/or us know that the link that made you land here should be changed to a link to idALT 23.

(Contributed by NM, 30-Sep-1992.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → 𝜑)

PART 18  COMPLEX TOPOLOGICAL VECTOR SPACES (DEPRECATED)

The intent is for this deprecated section to be deleted once its theorems have extensible structure versions (or are not useful). You can make a list of "terminal" theorems (i.e. theorems not referenced by anything else) and for each theorem see if there exists an extensible structure version (or decide it's not useful), and if so, delete it. Then repeat this recursively. One way to search for terminal theorems is to log the output ("open log x.txt") of "show usage WHATEVER" in metamath.exe and search for "(None)".

18.1  Additional material on group theory (deprecated)

This section contains an earlier development of groups that was defined before extensible structures were introduced.

The intent is for this deprecated section to be deleted once the corresponding definitions and theorems for complex topological vector spaces, which are using them, are revised accordingly.

18.1.1  Definitions and basic properties for groups

Syntax

cgr 26466

Extend class notation with the class of all group operations.

class GrpOp

Syntax

cgi 26467

Extend class notation with a function mapping a group operation to the group's identity element.

class GId

Syntax

cgn 26468

Extend class notation with a function mapping a group operation to the inverse function for the group.

class inv

Syntax

cgs 26469

Extend class notation with a function mapping a group operation to the division (or subtraction) operation for the group.

class /_𝑔

Definition

df-grpo 26470*

Define the class of all group operations. The base set for a group can be determined from its group operation. Based on the definition in Exercise 28 of [Herstein] p. 54. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.)

⊢ GrpOp = {𝑔 ∣ ∃𝑡(𝑔:(𝑡 × 𝑡)⟶𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 ∀𝑧 ∈ 𝑡 ((𝑥𝑔𝑦)𝑔𝑧) = (𝑥𝑔(𝑦𝑔𝑧)) ∧ ∃𝑢 ∈ 𝑡 ∀𝑥 ∈ 𝑡 ((𝑢𝑔𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑡 (𝑦𝑔𝑥) = 𝑢))}

Definition

df-gid 26471*

Define a function that maps a group operation to the group's identity element. (Contributed by FL, 5-Feb-2010.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)

⊢ GId = (𝑔 ∈ V ↦ (℩𝑢 ∈ ran 𝑔∀𝑥 ∈ ran 𝑔((𝑢𝑔𝑥) = 𝑥 ∧ (𝑥𝑔𝑢) = 𝑥)))

Definition

df-ginv 26472*

Define a function that maps a group operation to the group's inverse function. (Contributed by NM, 26-Oct-2006.) (New usage is discouraged.)

⊢ inv = (𝑔 ∈ GrpOp ↦ (𝑥 ∈ ran 𝑔 ↦ (℩𝑧 ∈ ran 𝑔(𝑧𝑔𝑥) = (GId‘𝑔))))

Definition

df-gdiv 26473*

Define a function that maps a group operation to the group's division (or subtraction) operation. (Contributed by NM, 15-Feb-2008.) (New usage is discouraged.)

⊢ /_𝑔 = (𝑔 ∈ GrpOp ↦ (𝑥 ∈ ran 𝑔, 𝑦 ∈ ran 𝑔 ↦ (𝑥𝑔((inv‘𝑔)‘𝑦))))

Theorem

isgrpo 26474*

The predicate "is a group operation." Note that 𝑋 is the base set of the group. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.)

⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝐺 ∈ 𝐴 → (𝐺 ∈ GrpOp ↔ (𝐺:(𝑋 × 𝑋)⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)) ∧ ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢))))

Theorem

isgrpoi 26475*

Properties that determine a group operation. Read 𝑁 as 𝑁(𝑥). (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.)

⊢ 𝑋 ∈ V    &   ⊢ 𝐺:(𝑋 × 𝑋)⟶𝑋    &   ⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋) → ((𝑥𝐺𝑦)𝐺𝑧) = (𝑥𝐺(𝑦𝐺𝑧)))    &   ⊢ 𝑈 ∈ 𝑋    &   ⊢ (𝑥 ∈ 𝑋 → (𝑈𝐺𝑥) = 𝑥)    &   ⊢ (𝑥 ∈ 𝑋 → 𝑁 ∈ 𝑋)    &   ⊢ (𝑥 ∈ 𝑋 → (𝑁𝐺𝑥) = 𝑈)    ⇒   ⊢ 𝐺 ∈ GrpOp

Theorem

grpofo 26476

A group operation maps onto the group's underlying set. (Contributed by NM, 30-Oct-2006.) (New usage is discouraged.)

⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝐺 ∈ GrpOp → 𝐺:(𝑋 × 𝑋)–onto→𝑋)

Theorem

grpocl 26477

Closure law for a group operation. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.)

⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) ∈ 𝑋)

Theorem

grpolidinv 26478*

A group has a left identity element, and every member has a left inverse. (Contributed by NM, 2-Nov-2006.) (New usage is discouraged.)

⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝐺 ∈ GrpOp → ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ ∃𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑢))

Theorem

grpon0 26479

The base set of a group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) (New usage is discouraged.)

⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝐺 ∈ GrpOp → 𝑋 ≠ ∅)

Theorem

grpoass 26480

A group operation is associative. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.)

⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = (𝐴𝐺(𝐵𝐺𝐶)))

Theorem

grpoidinvlem1 26481

Lemma for grpoidinv 26485. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.)

⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝐺 ∈ GrpOp ∧ (𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) ∧ ((𝑌𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝐴) = 𝐴)) → (𝑈𝐺𝐴) = 𝑈)

Theorem

grpoidinvlem2 26482

Lemma for grpoidinv 26485. (Contributed by NM, 10-Oct-2006.) (New usage is discouraged.)

⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝐺 ∈ GrpOp ∧ (𝑌 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) ∧ ((𝑈𝐺𝑌) = 𝑌 ∧ (𝑌𝐺𝐴) = 𝑈)) → ((𝐴𝐺𝑌)𝐺(𝐴𝐺𝑌)) = (𝐴𝐺𝑌))

Theorem

grpoidinvlem3 26483*

Lemma for grpoidinv 26485. (Contributed by NM, 11-Oct-2006.) (New usage is discouraged.)

⊢ 𝑋 = ran 𝐺    &   ⊢ (𝜑 ↔ ∀𝑥 ∈ 𝑋 (𝑈𝐺𝑥) = 𝑥)    &   ⊢ (𝜓 ↔ ∀𝑥 ∈ 𝑋 ∃𝑧 ∈ 𝑋 (𝑧𝐺𝑥) = 𝑈)    ⇒   ⊢ ((((𝐺 ∈ GrpOp ∧ 𝑈 ∈ 𝑋) ∧ (𝜑 ∧ 𝜓)) ∧ 𝐴 ∈ 𝑋) → ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈))

Theorem

grpoidinvlem4 26484*

Lemma for grpoidinv 26485. (Contributed by NM, 14-Oct-2006.) (New usage is discouraged.)

⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈)) → (𝐴𝐺𝑈) = (𝑈𝐺𝐴))

Theorem

grpoidinv 26485*

A group has a left and right identity element, and every member has a left and right inverse. (Contributed by NM, 14-Oct-2006.) (New usage is discouraged.)

⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝐺 ∈ GrpOp → ∃𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 (((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝑥) = 𝑢 ∧ (𝑥𝐺𝑦) = 𝑢)))

Theorem

grpoideu 26486*

The left identity element of a group is unique. Lemma 2.2.1(a) of [Herstein] p. 55. (Contributed by NM, 14-Oct-2006.) (New usage is discouraged.)

⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝐺 ∈ GrpOp → ∃!𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 (𝑢𝐺𝑥) = 𝑥)

Theorem

grporndm 26487

A group's range in terms of its domain. (Contributed by NM, 6-Apr-2008.) (New usage is discouraged.)

⊢ (𝐺 ∈ GrpOp → ran 𝐺 = dom dom 𝐺)

Theorem

0ngrp 26488

The empty set is not a group. (Contributed by NM, 25-Apr-2007.) (New usage is discouraged.)

⊢ ¬ ∅ ∈ GrpOp

Theorem

gidval 26489*

The value of the identity element of a group. (Contributed by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)

⊢ 𝑋 = ran 𝐺    ⇒   ⊢ (𝐺 ∈ 𝑉 → (GId‘𝐺) = (℩𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 ((𝑢𝐺𝑥) = 𝑥 ∧ (𝑥𝐺𝑢) = 𝑥)))

Theorem

grpoidval 26490*

Lemma for grpoidcl 26491 and others. (Contributed by NM, 5-Feb-2010.) (Proof shortened by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)

⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    ⇒   ⊢ (𝐺 ∈ GrpOp → 𝑈 = (℩𝑢 ∈ 𝑋 ∀𝑥 ∈ 𝑋 (𝑢𝐺𝑥) = 𝑥))

Theorem

grpoidcl 26491

The identity element of a group belongs to the group. (Contributed by NM, 24-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)

⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    ⇒   ⊢ (𝐺 ∈ GrpOp → 𝑈 ∈ 𝑋)

Theorem

grpoidinv2 26492*

A group's properties using the explicit identity element. (Contributed by NM, 5-Feb-2010.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)

⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (((𝑈𝐺𝐴) = 𝐴 ∧ (𝐴𝐺𝑈) = 𝐴) ∧ ∃𝑦 ∈ 𝑋 ((𝑦𝐺𝐴) = 𝑈 ∧ (𝐴𝐺𝑦) = 𝑈)))

Theorem

grpolid 26493

The identity element of a group is a left identity. (Contributed by NM, 24-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)

⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝑈𝐺𝐴) = 𝐴)

Theorem

grporid 26494

The identity element of a group is a right identity. (Contributed by NM, 24-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)

⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺𝑈) = 𝐴)

Theorem

grporcan 26495

Right cancellation law for groups. (Contributed by NM, 26-Oct-2006.) (New usage is discouraged.)

⊢ 𝑋 = ran 𝐺    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐶) = (𝐵𝐺𝐶) ↔ 𝐴 = 𝐵))

Theorem

grpoinveu 26496*

The left inverse element of a group is unique. Lemma 2.2.1(b) of [Herstein] p. 55. (Contributed by NM, 27-Oct-2006.) (New usage is discouraged.)

⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → ∃!𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈)

Theorem

grpoid 26497

Two ways of saying that an element of a group is the identity element. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.)

⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝐴 = 𝑈 ↔ (𝐴𝐺𝐴) = 𝐴))

Theorem

grporn 26498

The range of a group operation. Useful for satisfying group base set hypotheses of the form 𝑋 = ran 𝐺. (Contributed by NM, 5-Nov-2006.) (New usage is discouraged.)

⊢ 𝐺 ∈ GrpOp    &   ⊢ dom 𝐺 = (𝑋 × 𝑋)    ⇒   ⊢ 𝑋 = ran 𝐺

Theorem

grpoinvfval 26499*

The inverse function of a group. (Contributed by NM, 26-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)

⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    &   ⊢ 𝑁 = (inv‘𝐺)    ⇒   ⊢ (𝐺 ∈ GrpOp → 𝑁 = (𝑥 ∈ 𝑋 ↦ (℩𝑦 ∈ 𝑋 (𝑦𝐺𝑥) = 𝑈)))

Theorem

grpoinvval 26500*

The inverse of a group element. (Contributed by NM, 26-Oct-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)

⊢ 𝑋 = ran 𝐺    &   ⊢ 𝑈 = (GId‘𝐺)    &   ⊢ 𝑁 = (inv‘𝐺)    ⇒   ⊢ ((𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋) → (𝑁‘𝐴) = (℩𝑦 ∈ 𝑋 (𝑦𝐺𝐴) = 𝑈))